Small displeasure with associated type synonyms

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

Small displeasure with associated type synonyms

Stefan Holdermans
Dear all,

I was doing a little experimentation with associated type synonyms and  
ran into a small but unforeseen annoyance. The following, contrived,  
example snippets illustrate my pain:

First, let us declare some of the simplest classes exhibiting  
associated type synonyms that I can think of,

   class C a where
     type T a
     val :: T a

together with a trivial instance for nullary products:

   instance C () where
     type T () = ()
     val       = ()

But then, let us try an instance for binary products:

   instance (C a, C b) => C (a, b) where
     type T (a, b) = (T a, T b)
     val           = (val, val)

I really thought this would work out nicely, but GHC (version 6.8.2)  
gracefully gives me

   Couldn't match expected type `T a2' against inferred type `T a'
     Expected type: T (a2, b)
     Inferred type: (T a, T a1)
   In the expression: (val, val)
   In the definition of `val': val = (val, val)

   Couldn't match expected type `T b' against inferred type `T a1'
     Expected type: T (a2, b)
     Inferred type: (T a, T a1)
   In the expression: (val, val)
   In the definition of `val': val = (val, val)

while I think I deserve better than that.

Can someone (Tom?) please explain (a) why the required unifications  
fail, (b) whether or not it is reasonable to expect the unifications  
to succeed, and (c) how I can overcome problems like these? Surely, I  
can have val take a dummy argument, but I am hoping for something a  
bit more elegant here.

I tried lexically scoped type variables, but to no avail:

   instance forall a b. (C a, C b) => C (a, b) where
     type T (a, b) = (T a, T b)
     val           = (val :: T a, val :: T b)

gives me

   Couldn't match expected type `T a2' against inferred type `T a'
   In the expression: val :: T a
   In the expression: (val :: T a, val :: T b)
   In the definition of `val': val = (val :: T a, val :: T b)

etc.

Cheers,

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

Re: Small displeasure with associated type synonyms

Hugo Pacheco
I don't know if this is exactly what you were expecting as a dummy argument, but I solve this kind of issues like this:

_L = undefined

class C a where
    type TT a
    val :: a -> TT a
   
instance C () where
    type TT () = ()
    val _ = ()

instance (C a, C b) => C (a, b) where
    type TT (a,b) = (TT a, TT b)
    val _ = (val (_L :: a),val (_L :: b))

Why normal unification (val :: TT a) does not work I can't say why, but this kind of behavior is not solely for type families.

Cheers,
hugo



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

Re: Small displeasure with associated type synonyms

Tom Schrijvers-2
In reply to this post by Stefan Holdermans
Stefan,

> I tried lexically scoped type variables, but to no avail:
>
> instance forall a b. (C a, C b) => C (a, b) where
>   type T (a, b) = (T a, T b)
>   val           = (val :: T a, val :: T b)

The problem is ambiguity. The type checker can't determine which val
function to use, i.e. which dictionary to pass to val. Assume:

   instance C Int where
     type T Int = Int
     val        = 0

   instance C Bool where
     type T Bool = Int
     val         = 1

Now, if you want some val :: Int, which one do you get? The one of C Int
of C Bool? Depending on the choice you may get a different result. We
can't have that in a deterministic functional language. Hence the error.
Adding a type signature doesn't change the matter.

Providing an additional argument, as you propose, resolves the ambiguity.

I hope this helps.

Cheers,

Tom

--
Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium

tel: +32 16 327544
e-mail: [hidden email]
url: http://www.cs.kuleuven.be/~toms/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Small displeasure with associated type synonyms

haskell-2
Tom Schrijvers wrote:

> Stefan,
>
>> I tried lexically scoped type variables, but to no avail:
>>
>> instance forall a b. (C a, C b) => C (a, b) where
>>   type T (a, b) = (T a, T b)
>>   val           = (val :: T a, val :: T b)
>
> The problem is ambiguity. The type checker can't determine which val
> function to use, i.e. which dictionary to pass to val. Assume:
>
>   instance C Int where
>     type T Int = Int
>     val        = 0
>
>   instance C Bool where
>     type T Bool = Int
>     val         = 1
>
> Now, if you want some val :: Int, which one do you get? The one of C Int
> of C Bool? Depending on the choice you may get a different result. We
> can't have that in a deterministic functional language. Hence the error.
> Adding a type signature doesn't change the matter.

I don't see how your example explains this particular error.
I agree Int cannot be generalized to (T Int) or (T Bool).

I see Stefan's local type signature is not (val :: a) like your (val ::Int) but
(val :: T a) which is a whole different beast.  And (T a) is the type that ghc
should assign here.

The C (a,b) instance wants val :: T (a,b),  The T (a,b) is declared as "(T a, T
b)".  The annotated val returns "(T a, T b)".  One never needs the sort of Int
to (T Int) generalization.

So what is a better explanation or example to clarify why GHC cannot accept the
original code?

--
Chris

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

Re: Re: Small displeasure with associated type synonyms

Tom Schrijvers-2
> I don't see how your example explains this particular error.
> I agree Int cannot be generalized to (T Int) or (T Bool).

Generalized is not the right word here. In my example T Int, T Bool and
Int are all equivalent.

> I see Stefan's local type signature is not (val :: a) like your (val ::Int)
> but (val :: T a) which is a whole different beast.

Not all that different. As in my example the types T Int, T Bool and Int
are equivalent, whether one writes val :: Int, val :: T Int or val :: T
Bool. My point is that writing val :: T Int or val :: T Bool does not help
determining whether one should pick the val implementation of instance C
Int or C Bool.

> And (T a) is the type that ghc should assign here.

As my example tries to point out, there is not one single syntactic form
to denote a type.

Consider the val of in the first component. Because of val's signature in
the type class the type checker infers that the val expression has a type
equivalent to T a2 for some a2. The type checker also expects a type
equivalent to T a, either because of the type annotation or because of the
left hand side. So the type checker must solve the equation T a ~ T a2 for
some as yet to determine type a2 (a unification variable). This is
precisely where the ambiguity comes in. The type constructor T is not
injective. That means that the equation may hold for more than one value
of a2 (e.g. for T Int ~ T a2, a2 could be Int or Bool). Hence, the type
checker complains:

  Couldn't match expected type `T a2' against inferred type `T a'.

Maybe you don't care what type is chosen, if multiple ones are possible.
My example tried to show that this can effect the values computed by your
program. So it does matter.

For this particular example, it seems that the type checker does not have
have more than alternative for a2 in scope. However, it is not aware of
that fact. It uniformly applies the same general strategy for solving
equations in all contexts. This is a trade-off in type system complexity
vs. expressivity.

There is an opportunity for exploring another point in the design space
here.

Tom

--
Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium

tel: +32 16 327544
e-mail: [hidden email]
url: http://www.cs.kuleuven.be/~toms/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Small displeasure with associated type synonyms

haskell-2
Okay, I get the difference.

The "T a" annotation in "val :: T a)"and "val :: T a" does not help choose the
"C a" dictionary.
But the "val :: a-> T a" and "val (undefined :: a)" allows "a" to successfully
choose the "C a" dictionary.

val :: T a fixes "T a" but does not imply "C a".
(undefined :: a) fixes "a" and does imply "C a".
I now see how the functional dependency works here (which I should have tried to
do in the first place -- I should have thought more and relied on the mailing
list less).

"class C a b | a -> b" is here "class C a where type T a = b".
So only knowing "T a" or "b" does not allow "a" to be determined.

--
Chris

Tom Schrijvers wrote:

>> I don't see how your example explains this particular error.
>> I agree Int cannot be generalized to (T Int) or (T Bool).
>
> Generalized is not the right word here. In my example T Int, T Bool and
> Int are all equivalent.
>
>> I see Stefan's local type signature is not (val :: a) like your (val
>> ::Int) but (val :: T a) which is a whole different beast.
>
> Not all that different. As in my example the types T Int, T Bool and Int
> are equivalent, whether one writes val :: Int, val :: T Int or val :: T
> Bool. My point is that writing val :: T Int or val :: T Bool does not
> help determining whether one should pick the val implementation of
> instance C Int or C Bool.
>
>> And (T a) is the type that ghc should assign here.
>
> As my example tries to point out, there is not one single syntactic form
> to denote a type.
>
> Consider the val of in the first component. Because of val's signature
> in the type class the type checker infers that the val expression has a
> type equivalent to T a2 for some a2. The type checker also expects a
> type equivalent to T a, either because of the type annotation or because
> of the left hand side. So the type checker must solve the equation T a ~
> T a2 for some as yet to determine type a2 (a unification variable). This
> is precisely where the ambiguity comes in. The type constructor T is not
> injective. That means that the equation may hold for more than one value
> of a2 (e.g. for T Int ~ T a2, a2 could be Int or Bool). Hence, the type
> checker complains:
>
>     Couldn't match expected type `T a2' against inferred type `T a'.
>
> Maybe you don't care what type is chosen, if multiple ones are possible.
> My example tried to show that this can effect the values computed by
> your program. So it does matter.
>
> For this particular example, it seems that the type checker does not
> have have more than alternative for a2 in scope. However, it is not
> aware of that fact. It uniformly applies the same general strategy for
> solving equations in all contexts. This is a trade-off in type system
> complexity vs. expressivity.
>
> There is an opportunity for exploring another point in the design space
> here.
>
> Tom
>
> --
> Tom Schrijvers
>
> Department of Computer Science
> K.U. Leuven
> Celestijnenlaan 200A
> B-3001 Heverlee
> Belgium
>
> tel: +32 16 327544
> e-mail: [hidden email]
> url: http://www.cs.kuleuven.be/~toms/

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

Re: Small displeasure with associated type synonyms

Stefan Holdermans
In reply to this post by Tom Schrijvers-2
Tom,

Thanks for your quick answer.

> The problem is ambiguity. The type checker can't determine which val  
> function to use, i.e. which dictionary to pass to val.


I see. Still, maybe a type-error message in terms of good old  
"unresolved top-level overloading" would be a bit more useful  
here... ;-)

Cheers,

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

Re: Re: Small displeasure with associated type synonyms

Manuel M T Chakravarty
Stefan Holdermans:
>> The problem is ambiguity. The type checker can't determine which  
>> val function to use, i.e. which dictionary to pass to val.
>
> I see. Still, maybe a type-error message in terms of good old  
> "unresolved top-level overloading" would be a bit more useful  
> here... ;-)

I agree the error message is appalling.  Could you put this as a bug  
in the bug tracker?

Thanks,
Manuel

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

Re: Re: Small displeasure with associated type synonyms

David Menendez-2
In reply to this post by haskell-2
On Thu, Mar 6, 2008 at 3:57 PM, ChrisK <[hidden email]> wrote:

> Okay, I get the difference.
>
>  The "T a" annotation in "val :: T a)"and "val :: T a" does not help choose the
>  "C a" dictionary.
>  But the "val :: a-> T a" and "val (undefined :: a)" allows "a" to successfully
>  choose the "C a" dictionary.
>
>  val :: T a fixes "T a" but does not imply "C a".
>  (undefined :: a) fixes "a" and does imply "C a".
>  I now see how the functional dependency works here (which I should have tried to
>  do in the first place -- I should have thought more and relied on the mailing
>  list less).
>
>  "class C a b | a -> b" is here "class C a where type T a = b".
>  So only knowing "T a" or "b" does not allow "a" to be determined.

Am I correct in thinking this would have worked if it were an
associated type instead of an associated type synonym?

ie,

class C a where
    data T a
    val :: T a

--
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: Re: Small displeasure with associated type synonyms

Tom Schrijvers-2
> Am I correct in thinking this would have worked if it were an
> associated type instead of an associated type synonym?
>
> ie,
>
> class C a where
>    data T a
>    val :: T a

Yes, you are. Associate data type constructors (as well as ordinary
algebraic data constructors) are injective. So we have:

  forall a b . T a = T b <=> a = b

Cheers,

Tom

--
Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium

tel: +32 16 327544
e-mail: [hidden email]
url: http://www.cs.kuleuven.be/~toms/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Small displeasure with associated type synonyms

David Roundy-2
On Fri, Mar 07, 2008 at 08:07:57AM +0100, Tom Schrijvers wrote:

> >Am I correct in thinking this would have worked if it were an
> >associated type instead of an associated type synonym?
> >
> >ie,
> >
> >class C a where
> >   data T a
> >   val :: T a
>
> Yes, you are. Associate data type constructors (as well as ordinary
> algebraic data constructors) are injective. So we have:

Yay, that's what I though! (but was hesitant to suggest anything, since
I've never actually used associated anything...)  It's nice to hear that I
do understand some of this stuff.  :)
--
David Roundy
Department of Physics
Oregon State University
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe