Proposal: ValidateMonoLiterals - Initial bikeshed discussion

[Dominique Devriese]

2015-02-06 14:20 GMT+01:00 Adam Gundry <adam at 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