RE: ConstraintKinds feature suggestion and question about type family peculiarity

2013-06-17 Thread Simon Peyton-Jones
| This seems to works marvellously, but in writing it I ran into 2
| annoyances.
| 
| 1) The type errors produced by trying to use a function on a disallowed
| phantom type are rather unclear.
| 
| Could not deduce (Restrict Int ('[] *)) arising from a use of ‛foo
| 
| Which got me thinking, it would be really nice to have a vacuous
| Constraint that takes an error string as argument, i.e. a constraint
| that never holds and returns it's error string as type error. This would
| let you produce far nicer type errors when (ab)using ConstraintKinds and
| TypeFamilies by, for example, adding an extra Restrict instance
| Restrict x '[] = Vacuous Applying restricted function to disallowed
| type (or something to that effect), producing that message as error
| rather than the Could not deduce (Restrict Int ('[] *) which is a
| rather unhelpful error if you're not the person that wrote this code and
| are just using a function with such a Restrict constraint.

This is part of a more general question about how to generate better type error 
messages.  The Helium folk did some good work on this.  There's a very 
interesting PhD to be had here.

| 2) for some reason the type families syntax always requires a full
| argument list, which I find rather ugly. I would much prefer to use
| KindSignatures and write type family Restrict :: * - [*] -
| Constraint, but GHC does not allow this. Is there a specific reason for
| not allowing this syntax?

We need to fix the arity of a type family, because type families must always 
be fully applied.  If you write
type family F a :: * - *
then F *must* always be applied to one argument, and in a 'type instance' you 
can dispatch on one argument
type instance F Int = []
type instance F Bool = Maybe
If you instead write
type family F a b :: *
then you must always apply F to two arguments, and in a 'type instance' you can 
dispatch on two arguments.
type instance F Int Bool = Char

It is *unsatisfactory* that we get the clue about arity from the syntactic form 
of the 'type family' declaration. But it's a convenient hack; less clunky than, 
say
type family F [arity = 1] :: * - * - *  

Simon


___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


Re: ConstraintKinds feature suggestion and question about type family peculiarity

2013-06-16 Thread Roman Cheplyaka
* Merijn Verstraaten mer...@inconsistent.nl [2013-06-15 22:05:52+0100]
 2) for some reason the type families syntax always requires a full
argument list, which I find rather ugly. I would much prefer to use
KindSignatures and write type family Restrict :: * - [*] -
Constraint, but GHC does not allow this. Is there a specific
reason for not allowing this syntax?

I believe this is done to simplify (or even enable) type inference.

This is similar to the situation with type synonyms.

  type M1 = Maybe

is different from

  type M2 a = Maybe a

in that M1 has kind * - *, while M2 is not a type constructor and
doesn't have a kind — but when applied to a type of kind * it expands
to a type of kind *.

The same with the type families. You can define type families that
return e.g. [*] - *, but then you cannot pattern match on the [*]
type argument. If you could, that would be equivalent to type-level
lambdas, and that would make type inference hard or impossible.

Roman

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users