Kind refinement in type families with PolyKinds
Hi all, I'm wondering why the following does not work: {-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeOperators #-}
module Bug where
-- Type equality data a :=: b where Refl :: a :=: a
-- Applying a type to a list of arguments type family Apply (t :: k) (ts :: [*]) :: * type instance Apply t '[] = t type instance Apply (f :: * -> *) (t ': ts) = f t
-- Stripping a type from all its arguments type family Strip (t :: *) :: k type instance Strip (Maybe a) = Maybe
-- Reapplying a stripped type is the identity x :: Apply (Strip (Maybe a)) (a ': '[]) :=: Maybe a x = Refl
If I ask GHCi for the kind of `Strip (Maybe Int)`, I get `k`, whereas I would expect `* -> *`. That explains why the `Apply` type family is not reduced further. I understand that this might be related to GADTs not being allowed to refine kinds; the following datatype fails to compile with the error "`D1' cannot be GADT-like in its *kind* arguments": data DStrip :: k -> * where
D1 :: DStrip Maybe
But then, shouldn't the type instance for `Strip` above trigger the same error? Thanks, Pedro
Hi. 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 surprised that
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 kinds; the following datatype fails to compile with the error "`D1' cannot be GADT-like 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. Cheers, Andres
I share an observation/"workaround" below.
On Tue, Oct 30, 2012 at 8:49 AM, Andres Löh
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 surprised that
type instance Strip (Maybe a) = Maybe
then doesn't trigger an error.
In my experience, such kind arguments are treated like family indices, not parameters. If you add a kind annotation, as below,
x :: Apply (Strip (Maybe a) :: * -> *) (a ': '[]) :=: Maybe a x = Refl
then it type checks. I'm not sure if that scales to your general objective, though. Again, this is based on experience, not inspecting GHC or its theory.
Hi. I had said earlier that:
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 surprised that
type instance Strip (Maybe a) = Maybe
then doesn't trigger an error.
In my experience, such kind arguments are treated like family indices, not parameters.
Oh, I see. Thanks. This actually makes sense, but not have guessed it. So then the behaviour of GHC seems correct. For example, this typechecks:
type family Strip (t :: *) :: k type instance Strip (Maybe a) = Either type instance Strip (Maybe a) = Maybe type instance Strip (Maybe a) = Int
test :: (Strip (Maybe Int) Bool Char, Strip (Maybe Int) (), Strip (Maybe Char)) test = (Left True, Just (), 5)
The problem with
x :: Apply (Strip (Maybe a) :: * -> *) (a ': '[]) :=: Maybe a x = Refl
is indeed that without the type annotation, there's no way for GHC to infer the (implicit) kind parameter, because you're passing it to something which is also kind polymorphic. Cheers, Andres
I think the issue is this. We have Strip :: forall k. * -> k When you say type instance Strip (Maybe a) = Maybe GHC infers the kind arguments (as with all hidden argument) to get type instance Strip (*->*) (Maybe a) = Maybe It would be fine to have another type instance like this type instance Strip (Maybe a) = Int which would turn into type instance Strip * (Maybe a) = Maybe In all cases, an occurrence of (Strip <kind> <type>) will match one of the "type instances" only if, well, it matches, including the kind. Does that answer the question. I would love someone to write some user guidance notes about this kind of thing, perhaps as a new sub-page of http://www.haskell.org/haskellwiki/GHC/Type_system Simon From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users-bounces@haskell.org] On Behalf Of José Pedro Magalhães Sent: 30 October 2012 10:29 To: GHC users Subject: Kind refinement in type families with PolyKinds Hi all, I'm wondering why the following does not work: {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeOperators #-} module Bug where -- Type equality data a :=: b where Refl :: a :=: a -- Applying a type to a list of arguments type family Apply (t :: k) (ts :: [*]) :: * type instance Apply t '[] = t type instance Apply (f :: * -> *) (t ': ts) = f t -- Stripping a type from all its arguments type family Strip (t :: *) :: k type instance Strip (Maybe a) = Maybe -- Reapplying a stripped type is the identity x :: Apply (Strip (Maybe a)) (a ': '[]) :=: Maybe a x = Refl If I ask GHCi for the kind of `Strip (Maybe Int)`, I get `k`, whereas I would expect `* -> *`. That explains why the `Apply` type family is not reduced further. I understand that this might be related to GADTs not being allowed to refine kinds; the following datatype fails to compile with the error "`D1' cannot be GADT-like in its *kind* arguments": data DStrip :: k -> * where D1 :: DStrip Maybe But then, shouldn't the type instance for `Strip` above trigger the same error? Thanks, Pedro
participants (4)
-
Andres Löh -
José Pedro Magalhães -
Nicolas Frisby -
Simon Peyton-Jones