Add constructors for Date / Time components using type-level integers

[JordanMartinez]

trafficstars

With the advent of 0.15.0 and type-level integers, we can now define Date and Time components without using unsafePartial:

hour
  :: forall i
   . Reflectable i Int
  => PI.Compare i (-1) PO.GT
  => PI.Compare i 24 PO.LT
  => Proxy i
  -> Hour
hour p = Hour $ reflectType p

minute
  :: forall i
   . Reflectable i Int
  => PI.Compare i (-1) PO.GT
  => PI.Compare i 60 PO.LT
  => Proxy i
  -> Minute
minute p = Minute $ reflectType p

second
  :: forall i
   . Reflectable i Int
  => PI.Compare i (-1) PO.GT
  => PI.Compare i 60 PO.LT
  => Proxy i
  -> Second
second p = Second $ reflectType p

millisecond
  :: forall i
   . Reflectable i Int
  => PI.Compare i (-1) PO.GT
  => PI.Compare i 1_000 PO.LT
  => Proxy i
  -> Millisecond
millisecond p = Millisecond $ reflectType p

year
  :: forall i
   . Reflectable i Int
  => PI.Compare i (-271821) PO.GT
  => PI.Compare i 275760 PO.LT
  => Proxy i
  -> Year
year p = Year $ reflectType p

month
  :: forall i
   . Reflectable i Int
  => PI.Compare i 0 PO.GT
  => PI.Compare i 13 PO.LT
  => Proxy i
  -> Month
month p = unsafePartial $ fromJust $ toEnum $ reflectType p

day
  :: forall i
   . Reflectable i Int
  => PI.Compare i 0 PO.GT
  => PI.Compare i 32 PO.LT
  => Proxy i
  -> Day
day p = Day $ reflectType p

I would like to add a similar constructor for DateTime based on exactDate, but that requires verifying at the type-level that the day is within the bounds for the month-year combination. If we wanted to lift the isLeapYear function to the type-level, it seems we'll need a Prim.Int (class Mod) type class.

[JordanMartinez]

I would like to add a similar constructor for DateTime based on exactDate, but that requires verifying at the type-level that the day is within the bounds for the month-year combination. If we wanted to lift the isLeapYear function to the type-level, it seems we'll need a Prim.Int (class Mod) type class.

I think this could be implemented as:

exactDate
  :: forall year month day maxDay upperBound
   . Reflectable year Int
  => PI.Compare year (-271821) PO.GT
  => PI.Compare year 275760 PO.LT
  => Reflectable month Int
  => PI.Compare month 0 PO.GT
  => PI.Compare month 13 PO.LT
  => Reflectable day Int
  => MaxMonthDay year month maxDay
  => PI.Add maxDay 1 upperBound
  => PI.Compare i 0 PO.GT
  => PI.Compare i upperBound PO.LT
  => Proxy year
  -> Proxy month
  -> Proxy day
  -> Date
exactDate y m d = Date (DC.year y) (DC.month m) (DC.day d)

where

class MaxMonthDay year month maxDay | year month -> maxDay

instance MaxMonthDay year 1 31
else instance (IsLeapYear year b, If b 29 28 maxDay) => MaxMonthDay year 2 maxDay
else instance MaxMonthDay year 3 31
else instance MaxMonthDay year 4 30
else instance MaxMonthDay year 5 31
else instance MaxMonthDay year 6 30
else instance MaxMonthDay year 7 31
else instance MaxMonthDay year 8 31
else instance MaxMonthDay year 9 30
else instance MaxMonthDay year 10 31
else instance MaxMonthDay year 11 30
else instance MaxMonthDay year 12 31
else instance Fail (Text "Not a valid month") => MaxMonthDay year month day