Proposal: ValidateMonoLiterals - Initial bikeshed discussion

[Ryan Trinkle]

I think the idea of compile-time validation for overloaded literals is
fantastic, and doing it with nicer syntax than quasiquoting would really
improve things.  However, I'm a bit confused about specifically how the
requirement that it be monomorphic will play into this.  For example, if I
have:

x = 1

Presumably this will compile, and give a run-time error if I ever
instantiate its type to Even.  However, if I have:

x :: Even
x = 1

it will fail to compile?  Furthermore, if I have the former, and type
inference determines that its type is Even, it sounds like that will also
fail to compile, but if type inference determines that its type is forall
a. Nat a => a, then it will successfully compile and then fail at runtime.

Am I understanding this correctly?


Ryan

On Fri, Feb 6, 2015 at 8:55 AM, Erik Hesselink <hesselink at gmail.com> wrote:

> On Fri, Feb 6, 2015 at 2:49 PM, Dominique Devriese
> <dominique.devriese at cs.kuleuven.be> wrote:
> > 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
> ...
>
> Note that there is a trick to fake this with current GHC: you can
> write an equality constraint that is false, involving the type level
> string:
>
> >   type family MustBeTrue False error = (() ~ error)
>
> Erik
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20150206/ae8dc02d/attachment.html>