garyb · July 14, 2017 13:43
diff --git a/typelevel-datetime.purs b/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
	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