headers
José Pedro Magalhães | 30 Oct 2012 11:28
Picon
Gravatar

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

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Permalink | Reply |
headers
Andres Löh | 30 Oct 2012 14:49
Picon

Re: Kind refinement in type families with PolyKinds

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
Permalink | Reply |
headers
Nicolas Frisby | 30 Oct 2012 19:19
Picon
Gravatar

Re: Kind refinement in type families with PolyKinds

I share an observation/"workaround" below.

On Tue, Oct 30, 2012 at 8:49 AM, Andres Löh <andres.loeh <at> gmail.com> wrote:
> 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.
Permalink | Reply |
headers
Andres Löh | 30 Oct 2012 23:46
Picon

Re: Kind refinement in type families with PolyKinds

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
Permalink | Reply |
headers
Simon Peyton-Jones | 31 Oct 2012 17:43
Picon
Favicon
Gravatar

RE: Kind refinement in type families with PolyKinds

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 <at> haskell.org [mailto:glasgow-haskell-users-bounces <at> 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

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Permalink | Reply |

Gmane