Time Library Date Normalisation and Arithmetic
brianlsmith at gmail.com
Sun Jul 10 13:40:36 EDT 2005
I have some ideas about how to make the API simpler and easier to learn.
Please see my comments below.
On 7/9/05, Ashley Yakeley <ashley at semantic.org> wrote:
> I'm thinking of something along these lines:
> class (Eq a,Ord a) => Normalisable a where
> isNormal :: a -> Bool
> normaliseTruncate :: a -> a
> normaliseRollover :: a -> a
> The normalise functions would work like this:
> 2005/14/32 -> 2005/12/32 -> 2005/12/31
> 2005/-2/-4 -> 2005/01/-4 -> 2005/01/01
Usually people want normalization to happen automatically when doing date
arithmetic and I/O. What is the use case for having a representation for
invalid dates? I think it should not even be possible to have a date
2005/12/32 or 2005/01/-4. Why not make GregorianDay, ISOWeek, YearDay
abstract, and then provide explicit construction functions that normalize
and/or check validity automatically?
> Calendar Arithmetic
> This is one way of providing arithmetic for such things as Gregorian
> data TimeUnit d = TimeUnit
> addTimeUnitTruncate :: Integer -> d -> d
> addTimeUnitRollover :: Integer -> d -> d
> diffTimeUnitFloor :: d -> d -> Integer
days :: (DayEncoding d) => TimeUnit d
> gregorianMonths :: (DayEncoding d) => TimeUnit d
> gregorianYears :: (DayEncoding d) => TimeUnit d
Fisrly, why provide gregorianMonths and gregorianYears functions that work
for all day encodings? I think it is enough to have then defined only for
GregorianDay. If I am working with Julian days, I probably don't care about
what month it is in. And if I DO care, then I probably also want the year
and day too. So, I would just convert the julian day to a gregorian day.
Secondly, does date arithmetic really need to be this complicated? I have
managed with the following two date arithmetic functions for quite a while:
> --| 'addMonthsTruncated x d' adds 'x' months to date 'd'. The resultant
> --| truncated to the last day of the month if necessary. For example,
> --| addMonthsTruncated 1 (GregorianDay 2001 1 31) results in
> --| (GregorianDay 2001 2 28).
> --| (This function does arithmetic identically to the Oracle Add_Months
> --| function, the Microsoft .NET Calendar.AddMonths method, and the
> --| Java GregorianCalendar.add method (using Calendar.MONTH)
> addMonthsTruncated :: Int -> GregorianDay -> GregorianDay
> --| 'addDays x d' adds x days to 'd'.
> --| examples:
> --| addDays 1 (GregorianDay 2001 1 31) ==> GregorianDay 2001 2 1
> --| addDays -1 (GregorianDay 2001 1 1) ==> GregorianDay 2000 12 31
> addDays :: Int -> GregorianDay -> GregorianDay
You can define year and week arithmetic in terms of day and month
> addYears n = addMonths (12*n)
> addWeeks n = addDays (7*n)
So for instance, to add three months to a date d, you do this:
> d' = addTimeUnitTruncate gregorianMonths 3 d
I think that 'addMonthsTruncated 3' is a lot clearer.
Below is an untested interface (and some untested implementations) specific
to the Gregorian calendar that codifies some of my suggestions.
> module System.Calendar.Gregorian
> ( Date -- abstract
> , DateTime -- synonym
> --* Constructing a Date
> , fromYMD
> , normalizedFromYMD
> --* Deconstruction and arithmetic
> , Gregorian
> --* Misc
> , lastDayOfMonth
> import System.Time(DayEncoding,DayAndTime)
In the Gregorian calendar, a Date is represented by a year,
a month, and a day. The Date type given here always holds
a valid, normalized date. For example, it is not possible
for Date to contain "2005/06/31" because June only has 30 days.
> data Date = Date Integer Int Int
> type DateTime = DayAndTime Date
* Constructing a Date
There are 12 months, 1=January...12=December. Each month has a
variable number of days, starting with 1. Dates with positive
years are A.D., and dates with negative years are B.C. TODO:
what about year 0?
| Returns Nothing if the year, month, and day of month given do not
| represent a valid date. The following law holds:
| fromJust (fromYMD (ymd d)) == d
| isJust (fromYMD 1979 12 9) == True
| isJust (fromYMD -1 1 1) == True -- 1 BC
| isJust (fromYMD 2004 2 29) == True -- leap year
| isNothing (fromYMD 1979 2 29) == True -- not a leap year
| isNothing (fromYMD 0 1 1) == True -- TODO: year 0?
| isNothing (fromYMD 1900 13 2) == True -- no 13th month
| isNothing (fromYMD 1900 0 5) == True -- Months start at 1
> fromYMD :: Integer -> Int -> Int -> Maybe Date
> fromYMD _ _ _ = undefined -- TODO:
| Like fromYMD, but the given year, month, and day are
| normalized to become a valid date. This function is
| equivalent to (fromJust . fromYMD) when the given year, month,
| and day are already valid.
| normalizedFromYMD 1979 12 9 = fromJust (fromYMD 1979 12 9)
| normalizedFromYMD -1 1 1 = fromJust (fromYMD -1 1 1)
| normalizedFromYMD 2004 2 29 = fromJust (fromYMD 2004 2 29)
| normalizedFromYMD 0 1 1 = TODO: ????
| normalizedFromYMD 1979 2 29 = fromJust (fromYMD 1979 3 1)
| normalizedFromYMD 1900 13 2 = fromJust (fromYMD 1901 1 2)
| normalizedFromYMD 1900 0 5 = fromJust (fromYMD 1899 12 5)
| normalizedFromYMD 1 1 -1 = fromJust (fromYMD -1 13 31)
> normalizedFromYMD :: Integer -> Int -> Int -> Date
> normalizedFromYMD y m d
> -- TODO: I didn't test this code. In particular, I don't know
> -- how it works for the B.C./A.D. line
> | y == 0 = TODO:
> | otherwise =
> let withYear = Date y 1 1
> withMonth = addMonths m withYear
> withDay = addDays d withMonth
> in withDay
Deconstruction and arithmetic on Gregorian dates are defined
for Date, DateTime, and Zoned DateTime.
> class Gregorian d
| 'addMonthsTruncated x d' adds 'x' months to date 'd'.
| The resultant date is truncated to the last day of the month
| if necessary.
| (ymd $ addMonthsTruncated 1 (fromYMD 2001 1 31)) == (2001,2,28)
| This function does arithmetic identically to the Oracle Add_Months
| function, the Microsoft .NET Calendar.AddMonths method, and the
| Java GregorianCalendar.add method (using Calendar.MONTH).
> addMonthsTruncated :: Integer -> d -> d
| 'addDays x d' adds x days to 'd'.
| (ymd $ addDays 1 (fromYMD 2001 1 31)) == (2001, 2, 1)
| (ymd $ addDays -1 (fromYMD 2001 1 1)) == (2000,12,31)
> addDays :: Integer -> d -> d
| Extracts the (year,month,day) from the date.
| getMonth d = m where (_,m,_) = ymd d
| getEra d = if y >= 1 then "AD" else "BC" where (y,_,_) = ymd d
| isNewYearsDay = (m,d) == (1,1) where (_,m,d) = ymd d
> ymd :; d -> (Integer,Int,Int)
> instance Gregorian Date
> addMonthsTruncated _ _ = undefined -- TODO:
> addDays _ _ = undefined -- TODO:
> ymd (Date y m d) = (y,m,d)
> instance (Gregorian d) => Gregorian (DayAndTime d)
> addMonthsTruncated n (DayAndTime d t)
> = DayAndTime (addMonthsTruncated d) t
> addDays n (DayAndTime d t) = DayAndTime (addDays d) t
> ymd (DayAndTime d _) = ymd d
> instance Gregorian (Zoned DateTime)
> addMonthsTruncated _ (Zoned _) = undefined -- TODO: DST!!!
> addDays _ (Zoned _) = undefined -- TODO: DST!!!
> ymd (Zoned (DayAndTime d _)) = ymd d
| 'lastDayOfMonth d' Finds the last day of the month that d is in.
| (ymd $ lastDayOfMonth (fromYMD 2003 2 12)) == (2002, 2,28)
| (ymd $ lastDayOfMonth (fromYMD 2004 2 12)) == (2004, 2,29)
| (ymd $ lastDayOfMonth (fromYMD 1999,12, 9)) == (1999,12,31)
> lastDayOfMonth :: Date -> Date
> lastDayOfMonth (Date _ _ _) = undefined -- TODO:
Gregorian dates can be converted to and from Julian Dates.
> instance DayEncoding Date
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Libraries