Skip to content

ambiguity of offset precision of Date.date #29

@eldesh

Description

@eldesh

Basis Date sais:

Offsets are taken modulo 24 hours. That is, we express t, in hours, as sgn(t)(24*d + r), where d and r are non-negative, d is integral, and r < 24.

r < 24 means that r is in hours.
And by we express t, in hours, r should be integral.

But in general, the Time.time for offset has a finer precision than seconds.

And SML/NJ 110.97 keep values finer that hour like below:

- Date.toString (Date.date { year=2000, day= 1, hour=0, minute=0, month=Date.Jan, offset=SOME (Time.fromSeconds (0)), second=0});
val it = "Sat Jan 01 00:00:00 2000" : string
- Date.toString (Date.date { year=2000, day= 1, hour=0, minute=0, month=Date.Jan, offset=SOME (Time.fromSeconds (1)), second=0});
val it = "Sat Jan 01 00:00:01 2000" : string (* +1 sec *)

I think the specification should be modified to keep seconds.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions