Kind refinement in type families with PolyKinds
andres.loeh at gmail.com
Tue Oct 30 14:49:43 CET 2012
This one looks strange to me:
>> -- Stripping a type from all its arguments
>> type family Strip (t :: *) :: k
I'd be tempted to read this as saying that
> Strip :: forall k. * -> k
So the result of Strip would actually have to be kind-polymorphic. I'm
>> type instance Strip (Maybe a) = Maybe
then doesn't trigger an error.
> If I ask GHCi for the kind of `Strip (Maybe Int)`, I get `k`, whereas I
> would expect `* -> *`.
This seems to indicate that the correct reading for Strip might be
> Strip :: exists k. * -> k
which is counter-intuitive to me, because it's different from anything
else in Haskell. Then the result of Strip would indeed by an unknown
kind "k", and it would feel wrong to be able to reveal what concrete
kind it is later.
I think kind refinement on type families only makes sense if it is
introduced by arguments of the kind family.
> I understand that this might be related to GADTs not being allowed to refine
> the following datatype fails to compile with the error "`D1' cannot be
> in its *kind* arguments":
>> data DStrip :: k -> * where
>> D1 :: DStrip Maybe
This is somewhat different. Here, the kind of DStrip is clearly
DStrip :: forall k . k -> *
So here, actual refinement of k would make sense to me, although I
could understand if it isn't currently implemented.
More information about the Glasgow-haskell-users