Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
JordanMartinez opened this issue May 17, 2022 · 1 comment

Comments

@JordanMartinez
Copy link
Contributor

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
Copy link
Contributor Author

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant