2015-02-06 14:20 GMT+01:00 Adam Gundry <a...@well-typed.com>:
> 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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
