Re: Data.Time questions

On Mon, May 12, 2008 at 5:15 AM, Ashley Yakeley <ashley <at> semantic.org> wrote:
>> I did already create a new type for TT. However, what you are saying
>> makes sense too (I've been wondering about the 'AbsoluteTime' name).
>> I'm not sure that how to best handle parsing and formatting of TT
>> without another type though... I'll give it some thought.
>
>> Hmm, I realize I might also have to reconsider my 'ParseTime' instance
>> for 'AbsoluteTime' before I submit that patch...
>
> I see the problem now. TT and TAI are the same up to isomorphism, but they
> both can be written in YMD HMS format, with a 32.184s difference. So how to
> parse?
>
> So far I note the interesting property that any given String logically
> corresponds to at most one type:
>
>  "2008-05-01": Day
>  "05:45": TimeOfDay
>  "UTC-7": TimeZone
>  "2008-05-01 05:45": LocalTime
>  "2008-05-01 05:45 UTC-7": ZonedTime
>
> I'm not sure if that really matters, especially as one would need a new
> union type make use of it, but we could do an "instance ParseTime
> AbsoluteTime" if we insist on virtual time-zone strings:
>
>  "2008-01-01 00:00:00 TAI": AbsoluteTime
>  "2008-01-01 00:00:32.184 TT": AbsoluteTime
>  "2007-12-31 23:59:41 GPS": AbsoluteTime
>
> I'm not sure what to do about FormatTime, though.

We could perhaps use a phantom type:

 data AbsTime a = MkAbsTime {unAbsTime :: DiffTime} deriving (Eq,Ord)

 data TAI = TAI
 data TT = TT
 ...

 type TAITime = AbsTime TAI
 ...

This would allow using different instances for e.g. 'Show' while
avoiding duplicating other code.

> Another approach is to consider the TAI, TT, GPS time-scales as a parallel
> system of "zones". So we currently have
>
>  data ZonedTime = ZonedTime LocalTime TimeZone
>  utcToZonedTime :: TimeZone -> UTCTime -> ZonedTime
>  zonedTimeToUTC :: ZonedTime -> UTCTime
>
> We could add something like
>
>  data ScaledTime = ScaledTime LocalTime TimeScale
>  absoluteToScaledTime :: TimeScale -> AbsoluteTime -> ScaledTime
>  scaledTimeToAbsolute :: ScaledTime -> AbsoluteTime
>
> This would then give us
>
>  "2008-01-01 00:00:00 TAI": ScaledTime
>  "2008-01-01 00:00:32.184 TT": ScaledTime
>  "2007-12-31 23:59:41 GPS": ScaledTime

Note that for e.g. TCG the length of a second is "Scaled" w.r.t a TT
seconds by dTT/dTCG = 1 − LG. Do you propose such information be
included in the TimeScale?

> This would belong in the "specialist" module Data.Time.Clock.TAI, which
> isn't included in Data.Time, so it shouldn't bother ordinary users of time.

With the ideas above it seems we are straying further and further from
the brute-force implementation I was originally envisioning for TT.
I'll try to explore the design space... let me know if you have any
more ideas or insights.

Thanks,
Bjorn