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
* Merijn Verstraaten
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
| 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
participants (3)
-
Merijn Verstraaten -
Roman Cheplyaka -
Simon Peyton-Jones