2015-02-06 14:20 GMT+01:00 Adam Gundry
It seems to me that what you would describe would work, and the avoidance of TH is a merit, but the downside is the complexity of implementing even relatively simple validation at the type level (as opposed to just reusing a term-level function). For Merijn's Even example I guess one could do something like this in current GHC:
type family IsEven (n :: Nat) :: Bool where IsEven 0 = True IsEven 1 = False IsEven n = n - 2
instance (KnownNat n, IsEven n ~ True) => HasIntegerLiteral Even n where literal = Even (natVal (Proxy :: Proxy n))
but anything interesting to do with strings (e.g. checking that ByteStrings are ASCII) is rather out of reach at present.
Agreed. For the idea to scale, good support for type-level programming with Integers/Strings/... is essential. Something else that would be useful is an unsatisfiable primitive constraint constructor `UnsatisfiableConstraint :: String -> Constraint` that can be used to generate custom error messages. Then one could write something like type family MustBeTrue (t :: Bool) (error :: String) :: Constraint type family MustBeTrue True _ = () type family MustBeTrue False error = UnsatisfiableConstraint error type family MustBeEven (n :: Nat) :: Constraint type family MustBeEven n = MustBeTrue (IsEven n) ("Error in Even literal :'" ++ show n ++ "' is not even!") instance (KnownNat n, MustBeEven n) => HasIntegerLiteral Even n where ... Regards, Dominique