RE: ConstraintKinds feature suggestion and question about type family peculiarity
| 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
* 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
ConstraintKinds feature suggestion and question about type family peculiarity
Hello fellow haskellers!
I was experimenting with restricting functions operating on GADTs with phantom
types to only work on a subset of the possible phantom types. I ended up with
the following code:
{-# LANGUAGE ConstraintKinds, DataKinds, GADTs, TypeFamilies, TypeOperators #-}
import GHC.Prim (Constraint)
data Foo a where
Foo :: Foo Int
Bar :: Foo Char
Baz :: Foo Bool
type family Restrict a (as :: [*]) :: Constraint
type instance where
Restrict a (a ': as) = ()
Restrict x (a ': as) = Restrict x as
foo :: Restrict a '[Char, Bool] = Foo a - Bool
foo Bar = True
foo Baz = False
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.
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?
Cheers,
Merijn Verstraaten
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
