Type-level date/time formatter sketch

typelevel-datetime.purs

module Main where

import Prelude

import Control.Monad.Eff (Eff)
import Control.Monad.Eff.Console (CONSOLE, log)
import Data.Symbol (class IsSymbol, SProxy(..), reflectSymbol)

-- First we define a HList with custom kinds, so that we can restrict it to
-- format stuff
foreign import kind FormatAtom
foreign import kind FormatList

foreign import data FCons ∷ FormatAtom → FormatList → FormatList
foreign import data FNil ∷ FormatList

infixr 6 type FCons as :

-- Then we define the possible components of a format
foreign import data Hour24 ∷ FormatAtom
foreign import data Hour12 ∷ FormatAtom
foreign import data Minute ∷ FormatAtom
foreign import data Second ∷ FormatAtom
foreign import data Meridiem ∷ FormatAtom
foreign import data Text ∷ Symbol → FormatAtom

---

-- Now we need to define a bunch of states for the "hour type" of our format
foreign import kind HourType
foreign import data NoHour ∷ HourType -- initial state
foreign import data HourType24 ∷ HourType -- 24-hour time is present
foreign import data HourType12 ∷ HourType -- 12-hour time with meridiem is present
foreign import data Hour12Only ∷ HourType -- 12-hour time without meridiem is present
foreign import data MeridiemOnly ∷ HourType -- meridiem without 12-hour time is present

-- Now we need to define which of the above "hour types" result in a valid
-- format
class ValidHourType (ht ∷ HourType)
instance vht1 ∷ ValidHourType HourType12
instance vht2 ∷ ValidHourType HourType24
instance vht3 ∷ ValidHourType NoHour

--

-- Now we need to write a type-level function that computes the HourType of a
-- format. Fundeps are essentially just that - type-level functions.
class ValidateHours (fmt ∷ FormatList) (i ∷ HourType) (o ∷ HourType) | fmt i → o

-- The nil case means we've reached the end of the format, so we want to pass
-- through whatever input HourType we have at that step as the final output
instance vh0 ∷ ValidateHours FNil t t

-- When we see an `Hour24`, if no hour type has been set yet, continue along
-- the rest of the format with the state set to `HourType24`
instance vh2 ∷ ValidateHours rest HourType24 o ⇒ ValidateHours (Hour24 : rest) NoHour o

-- When we see a `Meridiem` or `Hour12` and no hour type has been set yet,
-- continue along the rest of the format with the approriate `-Only` type for
-- the `HourType`
instance vh3 ∷ ValidateHours rest Hour12Only o ⇒ ValidateHours (Hour12 : rest) NoHour o
instance vh4 ∷ ValidateHours rest MeridiemOnly o ⇒ ValidateHours (Meridiem : rest) NoHour o

-- When we see a `Meridiem` or `Hour12` and the input was the appropriate
-- `Hour12Only` or `MerideimOnly`, finally set type type to the "confirmed"
-- `Hour12Type`
instance vh5 ∷ ValidateHours rest HourType12 o ⇒ ValidateHours (Meridiem : rest) Hour12Only o
instance vh6 ∷ ValidateHours rest HourType12 o ⇒ ValidateHours (Hour12 : rest) MeridiemOnly o

-- All other cases are trivial - they pass through whatever input & output they got
instance vh1 ∷ ValidateHours rest i o ⇒ ValidateHours (Text s : rest) i o
instance vh7 ∷ ValidateHours rest i o ⇒ ValidateHours (Minute : rest) i o
instance vh8 ∷ ValidateHours rest i o ⇒ ValidateHours (Second : rest) i o

--

-- This class is used to simplify the type arguments involved for the individual
-- type-level functions, and can accumulate different tests. It will only ever
-- have one instance, which is there to check everything is good.
--
-- Here our instance calls the `ValidateHours` "function", starting with the
-- `NoHour` default state (it needs something passing through otherwise you get
-- errors about an undetermined type variable), and then it checks that our
-- computed `HourType` is valid.
--
-- We can do the same process for anything else we want to validate (like
-- day+week), split it into a function that computes a state, and then have a
-- class that only has instances for allowable states.
class ValidDate (a ∷ FormatList)
instance vd ∷ (ValidateHours a NoHour o, ValidHourType o) ⇒ ValidDate a

---

-- We need a new proxy type to accomodate our custom kind, so we can use it at
-- the value level for printing, etc.
data FProxy (a ∷ FormatList) = FProxy

-- This class folds a string from a `FormatList` to produce our desired output.
-- We would want to hide this class internally, as it does not enforce the
-- constraint that the date is valid - we can only do that at the top level of
-- a format, and this class deals with all of the tails of the format.
class PrintFormatI (fmt ∷ FormatList) where
  printFormatI ∷ FProxy fmt → String → String

instance rdi0 ∷ PrintFormatI FNil where
  printFormatI _ acc = acc

instance rdi1 ∷ (IsSymbol s, PrintFormatI rest) ⇒ PrintFormatI (Text s : rest) where
  printFormatI _ acc = printFormatI (FProxy ∷ FProxy rest) (acc <> reflectSymbol (SProxy ∷ SProxy s))

instance rdi2 ∷ PrintFormatI rest ⇒ PrintFormatI (Hour24 : rest) where
  printFormatI _ acc = printFormatI (FProxy ∷ FProxy rest) (acc <> "HH")

instance rdi3 ∷ PrintFormatI rest ⇒ PrintFormatI (Hour12 : rest) where
  printFormatI _ acc = printFormatI (FProxy ∷ FProxy rest) (acc <> "hh")

instance rdi4 ∷ PrintFormatI rest ⇒ PrintFormatI (Minute : rest) where
  printFormatI _ acc = printFormatI (FProxy ∷ FProxy rest) (acc <> "MM")

instance rdi5 ∷ PrintFormatI rest ⇒ PrintFormatI (Second : rest) where
  printFormatI _ acc = printFormatI (FProxy ∷ FProxy rest) (acc <> "ss")

instance rdi6 ∷ PrintFormatI rest ⇒ PrintFormatI (Meridiem : rest) where
  printFormatI _ acc = printFormatI (FProxy ∷ FProxy rest) (acc <> "a")

-- This class is the public version of the above. The single instance enforces
-- our validity constraint, and also removes the accumulator argument from the
-- `printFormatI` function.
class PrintFormat (fmt ∷ FormatList) where
  printFormat ∷ FProxy fmt → String

instance pf ∷ (ValidDate a, PrintFormatI a) ⇒ PrintFormat a where
  printFormat prx = printFormatI prx ""

---

-- One type level format definition:
type MyFormat = Hour12 : Text ":" : Minute : Text ":" : Second : Text " " : Meridiem : FNil

-- One reflected format:
myFormat ∷ String
myFormat = printFormat (FProxy ∷ FProxy MyFormat)

-- Try removing `Meridiem` from the above and see how it no-longer typechecks.
--
-- The error for that is pretty great, since it tells you exactly what is wrong.
-- The error for missing "pattern matches" isn't so great - try having two
-- `Hour12`s. We can add every permutation of arguments, and use `Fail`
-- constraints to explain invalid combinations, but it's just a bit tedious.
-- Might be worthwhile in the long run though.

main ∷ Eff (console ∷ CONSOLE) Unit
main = do
  log $ show myFormat