Type family signatures

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
8 messages Options
Reply | Threaded
Open this post in threaded view
|

Type family signatures

Thomas van Noort
Hello,

I have a question regarding type family signatures. Consider the
following type family:

   type family Fam a :: *

Then I define a GADT that takes such a value and wraps it:

   data GADT :: * -> * where
     GADT :: a -> Fam a -> GADT (Fam a)

and an accompanying unwrapper:

   unwrap :: GADT (Fam a) -> (a, Fam a)
   unwrap (GADT x y) = (x, y)

When Fam is declared using the first notation,

   type family Fam a :: *

GHC HEAD gives the following error message:

   Main.hs:9:21:
     Couldn't match expected type `a' against inferred type `a1'
       `a' is a rigid type variable bound by
           the type signature for `unwrap' at Main.hs:8:20
       `a1' is a rigid type variable bound by
            the constructor `GADT' at Main.hs:9:8
     In the expression: x
     In the expression: (x, y)
     In the definition of `unwrap': unwrap (GADT x y) = (x, y)

However, when Fam is declared as (moving the a to the other side of the
:: and changing it into *),

   type family Fam :: * -> *

everything is ok. So, it seems to me that GHC HEAD considers both
signatures to be really different. However, I do not quite understand
the semantic difference in my example, other than that Fam needs to be
fully satisfied in its named type arguments. Note that GHC 6.10.3 does
not accept the latter signature for Fam since it requires at least one
index for some reason, that's why I'm using GHC HEAD.

Regards,
Thomas
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type family signatures

David Menendez-2
On Fri, Aug 14, 2009 at 11:06 AM, Thomas van Noort<[hidden email]> wrote:

> Hello,
>
> I have a question regarding type family signatures. Consider the following
> type family:
>
>  type family Fam a :: *
>
> Then I define a GADT that takes such a value and wraps it:
>
>  data GADT :: * -> * where
>    GADT :: a -> Fam a -> GADT (Fam a)
>
> and an accompanying unwrapper:
>
>  unwrap :: GADT (Fam a) -> (a, Fam a)
>  unwrap (GADT x y) = (x, y)
>
> When Fam is declared using the first notation,
>
>  type family Fam a :: *
>
> GHC HEAD gives the following error message:
>
>  Main.hs:9:21:
>    Couldn't match expected type `a' against inferred type `a1'
>      `a' is a rigid type variable bound by
>          the type signature for `unwrap' at Main.hs:8:20
>      `a1' is a rigid type variable bound by
>           the constructor `GADT' at Main.hs:9:8
>    In the expression: x
>    In the expression: (x, y)
>    In the definition of `unwrap': unwrap (GADT x y) = (x, y)

This is because type families are not injective. Nothing stops you
from defining two instances such as,

type instance Fam Int = Bool
type instance Fam Char = Bool

in which case a value of type GADT Bool is ambiguous. Does it contain
an Int or a Char?

> However, when Fam is declared as (moving the a to the other side of the ::
> and changing it into *),
>
>  type family Fam :: * -> *
>
> everything is ok. So, it seems to me that GHC HEAD considers both signatures
> to be really different. However, I do not quite understand the semantic
> difference in my example, other than that Fam needs to be fully satisfied in
> its named type arguments. Note that GHC 6.10.3 does not accept the latter
> signature for Fam since it requires at least one index for some reason,
> that's why I'm using GHC HEAD.

A type family with no index is equivalent to a type synonym.

But in answer to your question, these signatures are very different.
Consider these families.

type family Foo a b :: *
type family Bar a :: * -> *

Foo is indexed by two parameters, but Bar is only indexed by one.

type instance Foo A B = X
type instance Foo A C = X
-- Foo a b ~ Foo a c does not imply b ~ c

type instance Bar A = []
-- Bar a b ~ Bar a c does imply b ~ c

Bar returns a type constructor, so it can be used anywhere a type
constructor of kind * -> * can be used.

foo :: (Functor (Foo a)) => ...   -- invalid
bar :: (Functor (Bar a)) => ...   -- valid

--
Dave Menendez <[hidden email]>
<http://www.eyrie.org/~zednenem/>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type family signatures

Dan Weston
But presumably he can use a data family instead of a type family to
restore injectivity, at the cost of adding an extra wrapped bottom value
and one more layer of value constructor?

David Menendez wrote:

> On Fri, Aug 14, 2009 at 11:06 AM, Thomas van Noort<[hidden email]> wrote:
>> Hello,
>>
>> I have a question regarding type family signatures. Consider the following
>> type family:
>>
>>  type family Fam a :: *
>>
>> Then I define a GADT that takes such a value and wraps it:
>>
>>  data GADT :: * -> * where
>>    GADT :: a -> Fam a -> GADT (Fam a)
>>
>> and an accompanying unwrapper:
>>
>>  unwrap :: GADT (Fam a) -> (a, Fam a)
>>  unwrap (GADT x y) = (x, y)
>>
>> When Fam is declared using the first notation,
>>
>>  type family Fam a :: *
>>
>> GHC HEAD gives the following error message:
>>
>>  Main.hs:9:21:
>>    Couldn't match expected type `a' against inferred type `a1'
>>      `a' is a rigid type variable bound by
>>          the type signature for `unwrap' at Main.hs:8:20
>>      `a1' is a rigid type variable bound by
>>           the constructor `GADT' at Main.hs:9:8
>>    In the expression: x
>>    In the expression: (x, y)
>>    In the definition of `unwrap': unwrap (GADT x y) = (x, y)
>
> This is because type families are not injective. Nothing stops you
> from defining two instances such as,
>
> type instance Fam Int = Bool
> type instance Fam Char = Bool
>
> in which case a value of type GADT Bool is ambiguous. Does it contain
> an Int or a Char?
>
>> However, when Fam is declared as (moving the a to the other side of the ::
>> and changing it into *),
>>
>>  type family Fam :: * -> *
>>
>> everything is ok. So, it seems to me that GHC HEAD considers both signatures
>> to be really different. However, I do not quite understand the semantic
>> difference in my example, other than that Fam needs to be fully satisfied in
>> its named type arguments. Note that GHC 6.10.3 does not accept the latter
>> signature for Fam since it requires at least one index for some reason,
>> that's why I'm using GHC HEAD.
>
> A type family with no index is equivalent to a type synonym.
>
> But in answer to your question, these signatures are very different.
> Consider these families.
>
> type family Foo a b :: *
> type family Bar a :: * -> *
>
> Foo is indexed by two parameters, but Bar is only indexed by one.
>
> type instance Foo A B = X
> type instance Foo A C = X
> -- Foo a b ~ Foo a c does not imply b ~ c
>
> type instance Bar A = []
> -- Bar a b ~ Bar a c does imply b ~ c
>
> Bar returns a type constructor, so it can be used anywhere a type
> constructor of kind * -> * can be used.
>
> foo :: (Functor (Foo a)) => ...   -- invalid
> bar :: (Functor (Bar a)) => ...   -- valid
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type family signatures

Ryan Ingram
On Fri, Aug 14, 2009 at 12:03 PM, Dan Weston<[hidden email]> wrote:
> But presumably he can use a data family instead of a type family to restore
> injectivity, at the cost of adding an extra wrapped bottom value and one
> more layer of value constructor?

Actually, you don't even necessarily pay this penalty, since you can
put newtypes into data families.

> data family Foo a
> newtype instance Foo () = UnitFoo Int

You do need to add the constructor wrap/unwrapping in code, but they
all get erased after typechecking.

  -- ryan
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type family signatures

Thomas van Noort
Somehow I didn't receive David's mail, but his explanation makes a lot
of sense. I'm still wondering how this results in a type error involving
rigid type variables.

Ryan Ingram wrote:

> On Fri, Aug 14, 2009 at 12:03 PM, Dan Weston<[hidden email]> wrote:
>> But presumably he can use a data family instead of a type family to restore
>> injectivity, at the cost of adding an extra wrapped bottom value and one
>> more layer of value constructor?
>
> Actually, you don't even necessarily pay this penalty, since you can
> put newtypes into data families.
>
>> data family Foo a
>> newtype instance Foo () = UnitFoo Int
>
> You do need to add the constructor wrap/unwrapping in code, but they
> all get erased after typechecking.
>
>   -- ryan
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type family signatures

Ryan Ingram
On Mon, Aug 17, 2009 at 12:12 AM, Thomas van Noort<[hidden email]> wrote:
> Somehow I didn't receive David's mail, but his explanation makes a lot of
> sense. I'm still wondering how this results in a type error involving rigid
> type variables.

"rigid" type means the type has been specified by the programmer somehow.

Desugaring your code a bit, we get:

GADT :: forall a b. (b ~ Fam a) => a -> b -> GADT b

Notice that this is an existential type that partially hides "a"; all
we know about "a" after unwrapping this type is that (Fam a ~ b).

unwrap :: forall a b. (b ~ Fam a) => GADT b -> (a,b)
unwrap (GADT x y) = (x,y)

So, the type signature of unwrap fixes "a" and "b" to be supplied by
the caller.  Then the pattern match on GADT needs a type variable for
the existential, so a new "a1" is invented.  These are rigid because
they cannot be further refined by the typechecker; the typechecker
cannot unify them with other types, like "a1 ~ Int", or "a1 ~ a".

An example of a non-rigid variable occurs type-checking this expression:

foo x = x + (1 :: Int)

During type-checking/inference, there is a point where the type environment is:

(+) :: forall a. Num a => a -> a -> a

b :: *, non-rigid
x :: b

c :: *, non-rigid
foo :: b -> c

Then (+) gets instantiated at Int and forces "b" and "c" to be Int.

In your case, during the typechecking of unwrap, we have:

unwrap :: forall a b. (b ~ Fam a) => GADT b -> (a,b)
    a :: *, rigid
    b :: *, rigid
    (b ~ Fam a)

    -- From the pattern match on GADT:
    a1 :: *, rigid
    x :: a1
    y :: b
    (b ~ Fam a1)

Now the typechecker wants to unify "a" and "a1", and it cannot,
because they are rigid.  If one of them was still open, we could unify
it with the other.

The type equalities give us (Fam a ~ Fam a1), but that does not give
us (a ~ a1).  If Fam was a data type or data family, we would know it
is injective and be able to derive (a ~ a1), but it is a type family,
so we are stuck.

  -- ryan
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type family signatures

Thomas van Noort
Thank your for this elaborate explanation, you made my day!

Thomas

Ryan Ingram wrote:

> On Mon, Aug 17, 2009 at 12:12 AM, Thomas van Noort<[hidden email]> wrote:
>> Somehow I didn't receive David's mail, but his explanation makes a lot of
>> sense. I'm still wondering how this results in a type error involving rigid
>> type variables.
>
> "rigid" type means the type has been specified by the programmer somehow.
>
> Desugaring your code a bit, we get:
>
> GADT :: forall a b. (b ~ Fam a) => a -> b -> GADT b
>
> Notice that this is an existential type that partially hides "a"; all
> we know about "a" after unwrapping this type is that (Fam a ~ b).
>
> unwrap :: forall a b. (b ~ Fam a) => GADT b -> (a,b)
> unwrap (GADT x y) = (x,y)
>
> So, the type signature of unwrap fixes "a" and "b" to be supplied by
> the caller.  Then the pattern match on GADT needs a type variable for
> the existential, so a new "a1" is invented.  These are rigid because
> they cannot be further refined by the typechecker; the typechecker
> cannot unify them with other types, like "a1 ~ Int", or "a1 ~ a".
>
> An example of a non-rigid variable occurs type-checking this expression:
>
> foo x = x + (1 :: Int)
>
> During type-checking/inference, there is a point where the type environment is:
>
> (+) :: forall a. Num a => a -> a -> a
>
> b :: *, non-rigid
> x :: b
>
> c :: *, non-rigid
> foo :: b -> c
>
> Then (+) gets instantiated at Int and forces "b" and "c" to be Int.
>
> In your case, during the typechecking of unwrap, we have:
>
> unwrap :: forall a b. (b ~ Fam a) => GADT b -> (a,b)
>     a :: *, rigid
>     b :: *, rigid
>     (b ~ Fam a)
>
>     -- From the pattern match on GADT:
>     a1 :: *, rigid
>     x :: a1
>     y :: b
>     (b ~ Fam a1)
>
> Now the typechecker wants to unify "a" and "a1", and it cannot,
> because they are rigid.  If one of them was still open, we could unify
> it with the other.
>
> The type equalities give us (Fam a ~ Fam a1), but that does not give
> us (a ~ a1).  If Fam was a data type or data family, we would know it
> is injective and be able to derive (a ~ a1), but it is a type family,
> so we are stuck.
>
>   -- ryan

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

RE: Type family signatures

Simon Peyton Jones
In reply to this post by Ryan Ingram
David is right that the program should be rejected.  To be concrete, as he suggests, suppose
  type instance Fam Int = Bool
  type instance Fam Char = Bool

Now suppose that 'unwrap' did typecheck. Then we could write:
  x :: Fam Int
  x = GADT 3 True

  y :: (Char, Bool)
  y = unwrap x

Voila!  We started with an Int (3), and managed to return it as the first component of a pair of type (Char,Bool).  


Ryan's explanation of the type checking process is accurate, but I agree that the error message is horrible.  Dimitrios and I are working on a better version of the type checker that will say something more helpful, like
        Cannot deduce (a ~ a1) from (Fam a ~ Fam a1)
which is a lot more useful.

Nice example, thank you.

Simon

| -----Original Message-----
| From: [hidden email] [mailto:[hidden email]] On
| Behalf Of Ryan Ingram
| Sent: 18 August 2009 21:56
| To: Thomas van Noort
| Cc: Haskell Cafe
| Subject: Re: [Haskell-cafe] Type family signatures
|
| On Mon, Aug 17, 2009 at 12:12 AM, Thomas van Noort<[hidden email]> wrote:
| > Somehow I didn't receive David's mail, but his explanation makes a lot of
| > sense. I'm still wondering how this results in a type error involving rigid
| > type variables.
|
| "rigid" type means the type has been specified by the programmer somehow.
|
| Desugaring your code a bit, we get:
|
| GADT :: forall a b. (b ~ Fam a) => a -> b -> GADT b
|
| Notice that this is an existential type that partially hides "a"; all
| we know about "a" after unwrapping this type is that (Fam a ~ b).
|
| unwrap :: forall a b. (b ~ Fam a) => GADT b -> (a,b)
| unwrap (GADT x y) = (x,y)
|
| So, the type signature of unwrap fixes "a" and "b" to be supplied by
| the caller.  Then the pattern match on GADT needs a type variable for
| the existential, so a new "a1" is invented.  These are rigid because
| they cannot be further refined by the typechecker; the typechecker
| cannot unify them with other types, like "a1 ~ Int", or "a1 ~ a".
|
| An example of a non-rigid variable occurs type-checking this expression:
|
| foo x = x + (1 :: Int)
|
| During type-checking/inference, there is a point where the type environment is:
|
| (+) :: forall a. Num a => a -> a -> a
|
| b :: *, non-rigid
| x :: b
|
| c :: *, non-rigid
| foo :: b -> c
|
| Then (+) gets instantiated at Int and forces "b" and "c" to be Int.
|
| In your case, during the typechecking of unwrap, we have:
|
| unwrap :: forall a b. (b ~ Fam a) => GADT b -> (a,b)
|     a :: *, rigid
|     b :: *, rigid
|     (b ~ Fam a)
|
|     -- From the pattern match on GADT:
|     a1 :: *, rigid
|     x :: a1
|     y :: b
|     (b ~ Fam a1)
|
| Now the typechecker wants to unify "a" and "a1", and it cannot,
| because they are rigid.  If one of them was still open, we could unify
| it with the other.
|
| The type equalities give us (Fam a ~ Fam a1), but that does not give
| us (a ~ a1).  If Fam was a data type or data family, we would know it
| is injective and be able to derive (a ~ a1), but it is a type family,
| so we are stuck.
|
|   -- ryan
| _______________________________________________
| Haskell-Cafe mailing list
| [hidden email]
| http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe