Re: [Haskell-cafe] type families and type signatures

[Martin Sulzmann]

Lennart Augustsson wrote:
On Wed, Apr 9, 2008 at 8:53 AM, Martin Sulzmann 
<[EMAIL PROTECTED] > wrote:



Lennart, you said

(It's also pretty easy to fix the problem.)


What do you mean? Easy to fix the type checker, or easy to fix the
program by inserting annotations
to guide the type checker?

Martin

 
I'm referring to the situation where the type inferred by the type 
checker is illegal for me to put into the program.
In our example we can fix this in two ways, by making foo' illegal 
even when it has no signature, or making foo' legal even when it has a 
signature.


To make it illegal:  If foo' has no type signature, infer a type for 
foo', insert this type as a signature and type check again.  If this 
fails, foo' is illegal.


To make it legal: If foo' with a type signature doesn't type check, 
try to infer a type without a signature.  If this succeeds then check 
that the type that was inferred is alpha-convertible to the original 
signature.  If it is, accept foo'; the signature doesn't add any 
information.


Either of these two option would be much preferable to the current 
(broken) situation where the inferred signature is illegal.


I understand now what you meant. See my earlier reply to Claus' email.

Regarding your request to take into account alpha-convertibility when 
checking signatures.

We know that in GHC the check

(forall a, b. Foo a b => a) <= (forall a, c. Foo a c => a)(**)

fails cause when testing the constraint/formula derived from the above 
subsumption check


 forall a, b. Foo a b implies exists c. Foo a c

GHC simply drops the exists c bit and clearly

  Foo a b does NOT imply Foo a c

We need to choose c to be equal to b. I call this process "matching" but 
it's of course

a form of alpha-conversion.
(We convince GHC to accept such signatures but encoding System F style
type application via redundant type proxy arguments)

The point I want to make is that in Chameleon I've implemented a 
subsumption check
which takes into account matching. Therefore, (**) is checkable in 
Chameleon.
BUT matching can be fairly expensive, exponential in the worst case, for 
example

consider cases such as Foo x_i x_i+1
So maybe there's good reason why GHC's subsumption check doesn't take 
into account matching.


The slightly odd thing is that GHC uses a "pessimistic" subsumption 
check (no matching) in combination

with an "optimistic" ambiguity check (see my earlier message on this topic).
I'd say it's better to be pessimistic/pessimistic and 
optimistic/optimistic, maybe this could be

a compiler switch?

Martin

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type families and type signatures

[Manuel M T Chakravarty]

Lennart Augustsson:
On Thu, Apr 10, 2008 at 4:20 AM, Manuel M T Chakravarty <[EMAIL PROTECTED] 
> wrote:

Lennart Augustsson:

On Wed, Apr 9, 2008 at 8:53 AM, Martin Sulzmann <[EMAIL PROTECTED] 
> wrote:


Lennart, you said

(It's also pretty easy to fix the problem.)

What do you mean? Easy to fix the type checker, or easy to fix the  
program by inserting annotations

to guide the type checker?

Martin

I'm referring to the situation where the type inferred by the type  
checker is illegal for me to put into the program.
In our example we can fix this in two ways, by making foo' illegal  
even when it has no signature, or making foo' legal even when it has  
a signature.


To make it illegal:  If foo' has no type signature, infer a type for  
foo', insert this type as a signature and type check again.  If this  
fails, foo' is illegal.


That would be possible, but it means we have to do this for all  
bindings in a program (also all lets bindings etc).


Of course, but I'd rather the compiler did it than I.  It's not that  
hard, btw.  If the whole module type checks, insert all signatures  
and type check again.


Sure.  I did not argue against this.  I think it would be a reasonable  
way forward.


Manuel

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type families and type signatures

[Manuel M T Chakravarty]

Lennart Augustsson:
In the current GHC there are even definitions that are perfecty  
usable, that cannot be given the type signature that that was  
inferred.


That's bad, I agree.

At work we have the warning for missing signatures enabled, and we  
turn warnings into errors.  We have to disbale this for certain  
definitions, because you cannot give them a signature.  I find that  
broken.


Definitely.  Can you give an example?

Manuel

On Thu, Apr 10, 2008 at 5:52 AM, Manuel M T Chakravarty <[EMAIL PROTECTED] 
> wrote:

Lennart Augustsson:

Let's look at this example from a higher level.

Haskell is a language which allows you to write type signatures for  
functions, and even encourages you to do it.
Sometimes you even have to do it.  Any language feature that stops  
me from writing a type signature is in my opinion broken.
TFs as implemented in currently implemented ghc stops me from  
writing type signatures.  They are thus, in my opinion, broken.


The problem of ambiguity is not at all restricted to TFs.  In fact,  
you need neither TFs nor FDs to get the exact same behaviour.  You  
don't even need MPTCs:


{-# LANGUAGE FlexibleContexts #-}
module Ambiguity where

class C a

bar :: C (a, b) => b -> b
bar = id

bar' :: C (a, b) => b -> b
bar' = bar



This gives us

/Users/chak/Code/haskell/Ambiguity.hs:10:7:
  Could not deduce (C (a, b)) from the context (C (a1, b))
arising from a use of `bar'
 at /Users/chak/Code/haskell/Ambiguity.hs:10:7-9
  Possible fix:
add (C (a, b)) to the context of the type signature for `bar''
or add an instance declaration for (C (a, b))
  In the expression: bar
  In the definition of `bar'': bar' = bar


So, we have this problem as soon as we have flexible contexts and/or  
MPTCs, independent of TFs and FDs.


Manuel


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type families and type signatures

[Manuel M T Chakravarty]

Lennart Augustsson:


On Thu, Apr 10, 2008 at 4:20 AM, Manuel M T Chakravarty <[EMAIL PROTECTED] 
> wrote:

the five signatures

 forall a. S a
 forall b. S b
 forall a b. S (a, b)
 Int
 S Int

By alpha-convertible I mean the usual thing from lambda calculus,  
they are identical modulo the names of bound variables.

So only the first two are alpha-convertible to each other.

If you involve any kind of reduction the equivalence test is no  
longer trivial.


All I'm asking for really, is to be able to paste in the type that  
was inferred as the signature, without the compiler complaining.


I think a trivial, purely syntactic test, such as the one proposed,  
would generate at least as much puzzlement as the current situation  
does.  It would mean, you could not have String in your signature if  
the inferred signature has [Char].  I don't think that this is a  
solution at all.


Manuel

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type families and type signatures

[Claus Reinke]

To make it legal: If foo' with a type signature doesn't type check,  
try to infer a type without a signature.  If this succeeds then  
check that the type that was inferred is alpha-convertible to the  
original signature.  If it is, accept foo'; the signature doesn't  
add any information.


This harder, if not impossible.  What does it mean for two signatures  
to be "alpha-convertible"? 


..[type synonym expansion vs type synonym family reduction]

So, I guess, you don't really mean alpha-convertible in its original  
syntactic sense.  We should accept the definition if the inferred and  
the given signature are in some sense "equivalent".  For this  
"equivalence" to be robust, I am sure we need to define it as follows,  
where <= is standard type subsumption:


  t1 "equivalent" t2  iff   t1 <= t2 and t2 <= t1


i would like to express my doubts about this assumption (which
relates directly to the earlier discussion about subsumption).

no matter what subsumption or what semantic equivalence we
are talking about, we expect it to *include* syntactic identity
(reflexivity of the relations):

   forall t: t <= t
   forall t: t ~ t

moving some equational theory into the "syntactic" equivalence
does not imply that syntactic has to be the full semantic 
equivalence - as the example of alpha- vs beta+alpha-

convertibility in lambda calculus demonstrates, it is convenient
to be able to ignore some representational issues when talking
about "identical" terms in the greater theory.

it would help to do the same here, and distinguish between
a syntactic and a semantic equivalence of types, where the
latter includes and extends the former:

syntactic: alpha-conversion, permutation of contexts,
   probably type synonym expansion (because they are 
   treated as syntactic macros, outside the theory)


semantic: type family reduction, ..

i'm tempted to the conclusion that the inability of the current
system to check its inferred signatures means that reflexivity
(of type subsumption/equivalence) is violated: if two types
are the same, they should be equivalent and subsume each
other. i can't see how the theory can work without this?

However, the fact that we cannot decide type subsumption 
for ambiguous types is exactly what led us to the original 
problem.  So, nothing has been won.


imho, the trick is to separate syntactic and semantic
equivalence, even if we include some "modulo theory"
in the former. both <= and ~ need to include this
syntactic equivalence. but syntactic equivalence should
remain straightforward to check - nothing should be
included in it that isn't easily checkable.

claus

ps i hope it is obvious that i'd like infered signatures to
   be checkable, not non-checkable signatures to be
   rejected?-)



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type families and type signatures

[Lennart Augustsson]

On Thu, Apr 10, 2008 at 4:20 AM, Manuel M T Chakravarty <
[EMAIL PROTECTED]> wrote:

> Lennart Augustsson:
>
> > On Wed, Apr 9, 2008 at 8:53 AM, Martin Sulzmann <
> > [EMAIL PROTECTED]> wrote:
> >
> > Lennart, you said
> >
> > (It's also pretty easy to fix the problem.)
> >
> > What do you mean? Easy to fix the type checker, or easy to fix the
> > program by inserting annotations
> > to guide the type checker?
> >
> > Martin
> >
> > I'm referring to the situation where the type inferred by the type
> > checker is illegal for me to put into the program.
> > In our example we can fix this in two ways, by making foo' illegal even
> > when it has no signature, or making foo' legal even when it has a signature.
> >
> > To make it illegal:  If foo' has no type signature, infer a type for
> > foo', insert this type as a signature and type check again.  If this fails,
> > foo' is illegal.
> >
>
> That would be possible, but it means we have to do this for all bindings
> in a program (also all lets bindings etc).
>

Of course, but I'd rather the compiler did it than I.  It's not that hard,
btw.  If the whole module type checks, insert all signatures and type check
again.

Making it legal might be cheaper, though.

-- Lennart
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type families and type signatures

[Lennart Augustsson]

I didn't say TF was the only broken feature in GHC.  But I want to see the
broken ones removed, instead of new ones added. :)

In the current GHC there are even definitions that are perfecty usable, that
cannot be given the type signature that that was inferred.

At work we have the warning for missing signatures enabled, and we turn
warnings into errors.  We have to disbale this for certain definitions,
because you cannot give them a signature.  I find that broken.

  -- Lennart

On Thu, Apr 10, 2008 at 5:52 AM, Manuel M T Chakravarty <
[EMAIL PROTECTED]> wrote:

> Lennart Augustsson:
>
> > Let's look at this example from a higher level.
> >
> > Haskell is a language which allows you to write type signatures for
> > functions, and even encourages you to do it.
> > Sometimes you even have to do it.  Any language feature that stops me
> > from writing a type signature is in my opinion broken.
> > TFs as implemented in currently implemented ghc stops me from writing
> > type signatures.  They are thus, in my opinion, broken.
> >
>
> The problem of ambiguity is not at all restricted to TFs.  In fact, you
> need neither TFs nor FDs to get the exact same behaviour.  You don't even
> need MPTCs:
>
>  {-# LANGUAGE FlexibleContexts #-}
> > module Ambiguity where
> >
> > class C a
> >
> > bar :: C (a, b) => b -> b
> > bar = id
> >
> > bar' :: C (a, b) => b -> b
> > bar' = bar
> >
> >
>
> This gives us
>
>  /Users/chak/Code/haskell/Ambiguity.hs:10:7:
> >   Could not deduce (C (a, b)) from the context (C (a1, b))
> > arising from a use of `bar'
> >  at /Users/chak/Code/haskell/Ambiguity.hs:10:7-9
> >   Possible fix:
> > add (C (a, b)) to the context of the type signature for `bar''
> > or add an instance declaration for (C (a, b))
> >   In the expression: bar
> >   In the definition of `bar'': bar' = bar
> >
>
>
> So, we have this problem as soon as we have flexible contexts and/or
> MPTCs, independent of TFs and FDs.
>
> Manuel
>
>
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type families and type signatures

[Lennart Augustsson]

On Thu, Apr 10, 2008 at 4:20 AM, Manuel M T Chakravarty <
[EMAIL PROTECTED]> wrote:

> the five signatures
>
>  forall a. S a
>  forall b. S b
>  forall a b. S (a, b)
>  Int
>  S Int
>

By alpha-convertible I mean the usual thing from lambda calculus, they are
identical modulo the names of bound variables.
So only the first two are alpha-convertible to each other.

If you involve any kind of reduction the equivalence test is no longer
trivial.

All I'm asking for really, is to be able to paste in the type that was
inferred as the signature, without the compiler complaining.

  -- Lennart
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type families and type signatures

[Manuel M T Chakravarty]

Lennart Augustsson:

Let's look at this example from a higher level.

Haskell is a language which allows you to write type signatures for  
functions, and even encourages you to do it.
Sometimes you even have to do it.  Any language feature that stops  
me from writing a type signature is in my opinion broken.
TFs as implemented in currently implemented ghc stops me from  
writing type signatures.  They are thus, in my opinion, broken.


The problem of ambiguity is not at all restricted to TFs.  In fact,  
you need neither TFs nor FDs to get the exact same behaviour.  You  
don't even need MPTCs:



{-# LANGUAGE FlexibleContexts #-}
module Ambiguity where

class C a

bar :: C (a, b) => b -> b
bar = id

bar' :: C (a, b) => b -> b
bar' = bar




This gives us


/Users/chak/Code/haskell/Ambiguity.hs:10:7:
   Could not deduce (C (a, b)) from the context (C (a1, b))
 arising from a use of `bar'
  at /Users/chak/Code/haskell/Ambiguity.hs:10:7-9
   Possible fix:
 add (C (a, b)) to the context of the type signature for `bar''
 or add an instance declaration for (C (a, b))
   In the expression: bar
   In the definition of `bar'': bar' = bar



So, we have this problem as soon as we have flexible contexts and/or  
MPTCs, independent of TFs and FDs.


Manuel

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type families and type signatures

[Manuel M T Chakravarty]

Lennart Augustsson:
On Wed, Apr 9, 2008 at 8:53 AM, Martin Sulzmann <[EMAIL PROTECTED] 
> wrote:


Lennart, you said

(It's also pretty easy to fix the problem.)

What do you mean? Easy to fix the type checker, or easy to fix the  
program by inserting annotations

to guide the type checker?

Martin

I'm referring to the situation where the type inferred by the type  
checker is illegal for me to put into the program.
In our example we can fix this in two ways, by making foo' illegal  
even when it has no signature, or making foo' legal even when it has  
a signature.


To make it illegal:  If foo' has no type signature, infer a type for  
foo', insert this type as a signature and type check again.  If this  
fails, foo' is illegal.


That would be possible, but it means we have to do this for all  
bindings in a program (also all lets bindings etc).


To make it legal: If foo' with a type signature doesn't type check,  
try to infer a type without a signature.  If this succeeds then  
check that the type that was inferred is alpha-convertible to the  
original signature.  If it is, accept foo'; the signature doesn't  
add any information.


This harder, if not impossible.  What does it mean for two signatures  
to be "alpha-convertible"?  I assume, you intend that given


  type S a = Int

the five signatures

  forall a. S a
  forall b. S b
  forall a b. S (a, b)
  Int
  S Int

are all the "alpha-convertible".  Now, given

  type family F a b
  type instance F Int c = Int

what about

  forall a. F a Int
  forall a. F Int Int
  forall a. F Int a
  forall a b. (a ~ Int) => F a b
  

So, I guess, you don't really mean alpha-convertible in its original  
syntactic sense.  We should accept the definition if the inferred and  
the given signature are in some sense "equivalent".  For this  
"equivalence" to be robust, I am sure we need to define it as follows,  
where <= is standard type subsumption:


  t1 "equivalent" t2  iff   t1 <= t2 and t2 <= t1

However, the fact that we cannot decide type subsumption for ambiguous  
types is exactly what led us to the original problem.  So, nothing has  
been won.


Summary
~~~
Trying to make those definitions that are currently only legal  
*without* a signature also legal when the inferred signature is added  
(foo' in Ganesh's example) doesn't seem workable.  However, to  
generally reject the same definitions, even if they are presented  
without a signature, seems workable.  It does require the compiler to  
compute type annotations, and then, check that it can still accept the  
annotated program.  This makes the process of type checking together  
with annotating the checked program idempotent, which is nice.


Manuel

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type families and type signatures

[Manuel M T Chakravarty]

Claus Reinke:

type family Id a
type instance Id Int = Int

foo :: Id a -> Id a
foo = id n
foo' :: Id a -> Id a
foo' = foo


type function notation is slightly misleading, as it presents
qualified polymorphic types in a form usually reserved for  
unqualified polymorphic types.


rewriting foo's type helped me to see the ambiguity that
others have pointed out:

foo :: r ~ Id a => r -> r

there's nowhere to get the 'a' from. so unless 'Id' itself is
fully polymorphic in 'a' (Id a = a, Id a = Int, ..), 'foo' can't
really be used. for each type variable, there needs to be
at least one position where it is not used as a type family
parameter.


Yes.  It is generally so that the introduction of indexed types (ie,  
all of GADTs, data type families, or synonym families) means that a  
type with a parameter is not necessarily parametric.



it might be useful to issue an ambiguity warning for such types?


The problem is that testing for ambiguity is, in general, difficult.   
Whether a context is ambiguous depends for example on the currently  
visible class instances.  As a result, a signature that is ambiguous  
in a module M, may be fine in a module N that imports M.


However, I think what should be easier is to improve the error  
messages given when a function with an ambiguous signature is used.   
For example, if the error message in the definition of foo' would have  
included a hint saying that the definition is illegal because its  
right hand side contains the use of a function with an ambiguous  
signature, then Ganesh may have had an easier time seeing what's  
happening.



ps. i find these examples and discussions helpful, if often initially
  puzzling - they help to clear up weak spots in the practice
  of type family use, understanding, and implementation, 
thereby improving all while making families more familiar!-)


Absolutely!

Manuel

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type families and type signatures

[Lennart Augustsson]

On Wed, Apr 9, 2008 at 8:53 AM, Martin Sulzmann <[EMAIL PROTECTED]>
wrote:

>
> Lennart, you said
>
> > (It's also pretty easy to fix the problem.)
> >
>
> What do you mean? Easy to fix the type checker, or easy to fix the program
> by inserting annotations
> to guide the type checker?
>
> Martin
>

I'm referring to the situation where the type inferred by the type checker
is illegal for me to put into the program.
In our example we can fix this in two ways, by making foo' illegal even when
it has no signature, or making foo' legal even when it has a signature.

To make it illegal:  If foo' has no type signature, infer a type for foo',
insert this type as a signature and type check again.  If this fails, foo'
is illegal.

To make it legal: If foo' with a type signature doesn't type check, try to
infer a type without a signature.  If this succeeds then check that the type
that was inferred is alpha-convertible to the original signature.  If it is,
accept foo'; the signature doesn't add any information.

Either of these two option would be much preferable to the current (broken)
situation where the inferred signature is illegal.

  -- Lennart
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type families and type signatures

[Martin Sulzmann]

Claus Reinke wrote:
The point is that the GHC type checker relies on automatic inference. 
Hence, there'll

always be cases where certain "reasonable" type signatures are rejected.

..
To conclude, any system with automatic inference will necessary 
reject certain type signatures/instances

in order to guarantee soundness, completeness and termination.


i think Lennart's complaint is mainly about cases where GHC does not 
accept the very type signature it infers itself. all of

which cases i'd consider bugs myself, independent of what
type system feature they are related to.

there are also the related cases of type signatures which cannot be 
expressed in the language but which might

occur behind the scenes. all of these cases i'd consider
language limitations that ought to be removed.

the latter cases also mean that type errors are reported either in a 
syntax that can not be used in programs or in a misleading external 
syntax that does not fully represent the internal type.


in this example, ghci infers a type for foo' that it rejects as a type 
signature for foo'. so, either the inferred type

is inaccurately presented, or there's a gap in the type
system, between inferred and declared types, right?



Good point(s) which I missed earlier.

Type inference (no annotations) is easy but type checking is much harder.
Type checking is not all about pure checking, we also perform some 
inference,

the Hindley/Milner unification variables which arise out of the program text
(we need to satisfy these constraints via the annotation).

To make type checking easier we should impose restrictions on inference.
We (Tom/SimonPJ/Manuel) thought about this possibility. The problem is 
that it's

hard to give an intuitive, declarative description of those restrictions.

Martin



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type families and type signatures

[Martin Sulzmann]

Claus Reinke wrote:

type family Id a

type instance Id Int = Int

foo :: Id a -> Id a
foo = id n

foo' :: Id a -> Id a
foo' = foo


type function notation is slightly misleading, as it presents
qualified polymorphic types in a form usually reserved for unqualified 
polymorphic types.


rewriting foo's type helped me to see the ambiguity that
others have pointed out:

foo :: r ~ Id a => r -> r

there's nowhere to get the 'a' from. so unless 'Id' itself is
fully polymorphic in 'a' (Id a = a, Id a = Int, ..), 'foo' can't
really be used. for each type variable, there needs to be
at least one position where it is not used as a type family
parameter.


Correct because type family constructors are injective only.

[Side note: With FDs you can enforce bijection

class Inj a b | a -> b
class Bij a b | a -> b, b -> a
]


it might be useful to issue an ambiguity warning for such types?

perhaps, with closed type families, one might be able to
reason backwards (is there a unique 'a' such that 'Id a ~ Int'?),
as with bidirectional FDs. but if you want to flatten all
'Maybe'-nests, even that direction isn't unique.


True, type checking with closed type families will rely on some form of
solving and then we're more likely to guess (the right) types.


The type checking problem for foo' boils down to verifying the formula

forall a. exists b. Id a ~ Id b


naively, i'd have expected to run into this instead/first:

(forall a. Id a -> Id a) ~ (forall b. Id b -> Id b)

which ought to be true modulo alpha conversion, without guesses,
making 'foo'' as valid/useless as 'foo' itself.

where am i going wrong?


You're notion of subsumption is too strong here.
I've been using


 (forall as. C => t) <= (forall bs. C' => t')

iff

 forall bs. (C'  implies exist bs. (C /\ t=t'))

where

(forall as. C => t) is the inferred type

(forall bs. C' => t') is the annotated type

Makes sense?


Even if we establish

(forall a. Id a -> Id a) ~ (forall b. Id b -> Id b)

we'd need to guess a ~ b
(which is of course obvious)


claus

ps. i find these examples and discussions helpful, if often initially
   puzzling - they help to clear up weak spots in the practice
   of type family use, understanding, and implementation,
thereby improving all while making families more familiar!-)

Absolutely!

Martin


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type families and type signatures

[Claus Reinke]

The point is that the GHC type checker relies on automatic inference. 
Hence, there'll

always be cases where certain "reasonable" type signatures are rejected.
.. 
To conclude, any system with automatic inference will necessary reject 
certain type signatures/instances

in order to guarantee soundness, completeness and termination.


i think Lennart's complaint is mainly about cases where GHC 
does not accept the very type signature it infers itself. all of

which cases i'd consider bugs myself, independent of what
type system feature they are related to.

there are also the related cases of type signatures which 
cannot be expressed in the language but which might

occur behind the scenes. all of these cases i'd consider
language limitations that ought to be removed.

the latter cases also mean that type errors are reported 
either in a syntax that can not be used in programs or in 
a misleading external syntax that does not fully represent 
the internal type.


in this example, ghci infers a type for foo' that it rejects 
as a type signature for foo'. so, either the inferred type

is inaccurately presented, or there's a gap in the type
system, between inferred and declared types, right?

claus


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type families and type signatures

[Claus Reinke]

type family Id a

type instance Id Int = Int

foo :: Id a -> Id a
foo = id n

foo' :: Id a -> Id a
foo' = foo


type function notation is slightly misleading, as it presents
qualified polymorphic types in a form usually reserved for 
unqualified polymorphic types.


rewriting foo's type helped me to see the ambiguity that
others have pointed out:

foo :: r ~ Id a => r -> r

there's nowhere to get the 'a' from. so unless 'Id' itself is
fully polymorphic in 'a' (Id a = a, Id a = Int, ..), 'foo' can't
really be used. for each type variable, there needs to be
at least one position where it is not used as a type family
parameter.

it might be useful to issue an ambiguity warning for 
such types?


perhaps, with closed type families, one might be able to
reason backwards (is there a unique 'a' such that 'Id a ~ Int'?),
as with bidirectional FDs. but if you want to flatten all
'Maybe'-nests, even that direction isn't unique.


The type checking problem for foo' boils down to verifying the formula

forall a. exists b. Id a ~ Id b


naively, i'd have expected to run into this instead/first:

(forall a. Id a -> Id a) ~ (forall b. Id b -> Id b)

which ought to be true modulo alpha conversion, without guesses,
making 'foo'' as valid/useless as 'foo' itself.

where am i going wrong?
claus

ps. i find these examples and discussions helpful, if often initially
   puzzling - they help to clear up weak spots in the practice
   of type family use, understanding, and implementation, 
   thereby improving all while making families more familiar!-)



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type families and type signatures

[Martin Sulzmann]

I think it's not fair to say TFs as implemented in GHC are broken.
Fine, they are situations where the current implementation is overly 
conservative.


The point is that the GHC type checker relies on automatic inference. 
Hence, there'll

always be cases where certain "reasonable" type signatures are rejected.

For example, consider the case of "undecidable" and "non-confluent" type 
class instances.


instance Foo a => Bar a-- (1)

instance Erk a => Bar [a]  -- (2)


GHC won't accept the above type class instance (note: instances are a 
kind of type signature) because


- instance (1) is potentially non-terminating (the size of the type term 
is not decreasing)
- instance (2) overlaps with (1),  hence, it can happen that during 
context reduction we choose

 the "wrong" instance.

To conclude, any system with automatic inference will necessary reject 
certain type signatures/instances

in order to guarantee soundness, completeness and termination.

Lennart, you said

(It's also pretty easy to fix the problem.)


What do you mean? Easy to fix the type checker, or easy to fix the 
program by inserting annotations

to guide the type checker?

Martin


Lennart Augustsson wrote:

Let's look at this example from a higher level.

Haskell is a language which allows you to write type signatures for 
functions, and even encourages you to do it.
Sometimes you even have to do it.  Any language feature that stops me 
from writing a type signature is in my opinion broken.
TFs as implemented in currently implemented ghc stops me from writing 
type signatures.  They are thus, in my opinion, broken.


A definition should either be illegal or it should be able to have a 
signature.  I think this is a design goal.  It wasn't true in Haskell 
98, and it's generally agreed that this was a mistake.


To summarize: I don't care if the definition is useless, I want to be 
able to give it a type signature anyway.


(It's also pretty easy to fix the problem.)

  -- Lennart

On Wed, Apr 9, 2008 at 7:20 AM, Martin Sulzmann 
<[EMAIL PROTECTED] > wrote:


Manuel said earlier that the source of the problem here is foo's
ambiguous type signature
(I'm switching back to the original, simplified example).
Type checking with ambiguous type signatures is hard because the
type checker has to guess
types and this guessing step may lead to too many (ambiguous)
choices. But this doesn't mean
that this worst case scenario always happens.

Consider your example again


type family Id a

type instance Id Int = Int

foo :: Id a -> Id a
foo = id

foo' :: Id a -> Id a
foo' = foo

The type checking problem for foo' boils down to verifying the formula

forall a. exists b. Id a ~ Id b

Of course for any a we can pick b=a to make the type equation
statement hold.
Fairly easy here but the point is that the GHC type checker
doesn't do any guessing
at all. The only option you have (at the moment, there's still
lots of room for improving
GHC's type checking process) is to provide some hints, for example
mimicking
System F style type application by introducing a type proxy
argument in combination
with lexically scoped type variables.

foo :: a -> Id a -> Id a
foo _ = id

foo' :: Id a -> Id a
foo' = foo (undefined :: a)


Martin



Ganesh Sittampalam wrote:

On Wed, 9 Apr 2008, Manuel M T Chakravarty wrote:

Sittampalam, Ganesh:


No, I meant can't it derive that equality when
matching (Id a) against (Id b)? As you say, it can't
derive (a ~ b) at that point, but (Id a ~ Id b) is
known, surely?


No, it is not know.  Why do you think it is?


Well, if the types of foo and foo' were forall a . a -> a and
forall b . b -> b, I would expect the type-checker to unify a
and b in the argument position and then discover that this
equality made the result position unify too. So why can't the
same happen but with Id a and Id b instead?

The problem is really with foo and its signature, not with
any use of foo. The function foo is (due to its type)
unusable.  Can't you change foo?


Here's a cut-down version of my real code. The type family
Apply is very important because it allows me to write class
instances for things that might be its first parameter, like
Id and Comp SqlExpr Maybe, without paying the syntactic
overhead of forcing client code to use Id/unId and
Comp/unComp. It also squishes nested Maybes which is important
to my application (since SQL doesn't have them).

castNum is the simplest example of a general problem - the
whole point is to allow clients to write code that is
overloaded over the first parameter to Apply using primitives
like 

Re: [Haskell-cafe] type families and type signatures

[Lennart Augustsson]

Let's look at this example from a higher level.

Haskell is a language which allows you to write type signatures for
functions, and even encourages you to do it.
Sometimes you even have to do it.  Any language feature that stops me from
writing a type signature is in my opinion broken.
TFs as implemented in currently implemented ghc stops me from writing type
signatures.  They are thus, in my opinion, broken.

A definition should either be illegal or it should be able to have a
signature.  I think this is a design goal.  It wasn't true in Haskell 98,
and it's generally agreed that this was a mistake.

To summarize: I don't care if the definition is useless, I want to be able
to give it a type signature anyway.

(It's also pretty easy to fix the problem.)

  -- Lennart

On Wed, Apr 9, 2008 at 7:20 AM, Martin Sulzmann <[EMAIL PROTECTED]>
wrote:

> Manuel said earlier that the source of the problem here is foo's ambiguous
> type signature
> (I'm switching back to the original, simplified example).
> Type checking with ambiguous type signatures is hard because the type
> checker has to guess
> types and this guessing step may lead to too many (ambiguous) choices. But
> this doesn't mean
> that this worst case scenario always happens.
>
> Consider your example again
>
> type family Id a
>
> type instance Id Int = Int
>
> foo :: Id a -> Id a
> foo = id
>
> foo' :: Id a -> Id a
> foo' = foo
>
> The type checking problem for foo' boils down to verifying the formula
>
> forall a. exists b. Id a ~ Id b
>
> Of course for any a we can pick b=a to make the type equation statement
> hold.
> Fairly easy here but the point is that the GHC type checker doesn't do any
> guessing
> at all. The only option you have (at the moment, there's still lots of
> room for improving
> GHC's type checking process) is to provide some hints, for example
> mimicking
> System F style type application by introducing a type proxy argument in
> combination
> with lexically scoped type variables.
>
> foo :: a -> Id a -> Id a
> foo _ = id
>
> foo' :: Id a -> Id a
> foo' = foo (undefined :: a)
>
>
> Martin
>
>
>
> Ganesh Sittampalam wrote:
>
> > On Wed, 9 Apr 2008, Manuel M T Chakravarty wrote:
> >
> >  Sittampalam, Ganesh:
> > >
> >
> >  No, I meant can't it derive that equality when matching (Id a) against
> > > > (Id b)? As you say, it can't derive (a ~ b) at that point, but (Id a ~ 
> > > > Id b)
> > > > is known, surely?
> > > >
> > >
> > > No, it is not know.  Why do you think it is?
> > >
> >
> > Well, if the types of foo and foo' were forall a . a -> a and forall b .
> > b -> b, I would expect the type-checker to unify a and b in the argument
> > position and then discover that this equality made the result position unify
> > too. So why can't the same happen but with Id a and Id b instead?
> >
> >  The problem is really with foo and its signature, not with any use of
> > > foo. The function foo is (due to its type) unusable.  Can't you change 
> > > foo?
> > >
> >
> > Here's a cut-down version of my real code. The type family Apply is very
> > important because it allows me to write class instances for things that
> > might be its first parameter, like Id and Comp SqlExpr Maybe, without paying
> > the syntactic overhead of forcing client code to use Id/unId and
> > Comp/unComp. It also squishes nested Maybes which is important to my
> > application (since SQL doesn't have them).
> >
> > castNum is the simplest example of a general problem - the whole point
> > is to allow clients to write code that is overloaded over the first
> > parameter to Apply using primitives like castNum. I'm not really sure how I
> > could get away from the ambiguity problem, given that desire.
> >
> > Cheers,
> >
> > Ganesh
> >
> > {-# LANGUAGE TypeFamilies, GADTs, UndecidableInstances,
> > NoMonomorphismRestriction #-}
> >
> > newtype Id a = Id { unId :: a }
> > newtype Comp f g x = Comp { unComp :: f (g x) }
> >
> > type family Apply (f :: * -> *) a
> >
> > type instance Apply Id a = a
> > type instance Apply (Comp f g) a = Apply f (Apply g a)
> > type instance Apply SqlExpr a = SqlExpr a
> > type instance Apply Maybe Int = Maybe Int
> > type instance Apply Maybe Double = Maybe Double
> > type instance Apply Maybe (Maybe a) = Apply Maybe a
> >
> > class DoubleToInt s where
> >   castNum :: Apply s Double -> Apply s Int
> >
> > instance DoubleToInt Id where
> >   castNum = round
> >
> > instance DoubleToInt SqlExpr where
> >   castNum = SECastNum
> >
> > data SqlExpr a where
> >  SECastNum :: SqlExpr Double -> SqlExpr Int
> >
> > castNum' :: (DoubleToInt s) => Apply s Double -> Apply s Int
> > castNum' = castNum
> >
> > ___
> > Haskell-Cafe mailing list
> > Haskell-Cafe@haskell.org
> > http://www.haskell.org/mailman/listinfo/haskell-cafe
> >
>
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
__

RE: [Haskell-cafe] type families and type signatures

[Sittampalam, Ganesh]

OK, thanks. I think I'm finally understanding :-)

Cheers,

Ganesh

-Original Message-
From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On Behalf Of Martin Sulzmann
Sent: 09 April 2008 07:21
To: Ganesh Sittampalam
Cc: Manuel M T Chakravarty; haskell-cafe@haskell.org
Subject: Re: [Haskell-cafe] type families and type signatures

Manuel said earlier that the source of the problem here is foo's ambiguous type 
signature (I'm switching back to the original, simplified example).
Type checking with ambiguous type signatures is hard because the type checker 
has to guess types and this guessing step may lead to too many (ambiguous) 
choices. 
But this doesn't mean
that this worst case scenario always happens.

Consider your example again

type family Id a

type instance Id Int = Int

foo :: Id a -> Id a
foo = id

foo' :: Id a -> Id a
foo' = foo

The type checking problem for foo' boils down to verifying the formula

forall a. exists b. Id a ~ Id b

Of course for any a we can pick b=a to make the type equation statement hold.
Fairly easy here but the point is that the GHC type checker doesn't do any 
guessing at all. The only option you have (at the moment, there's still lots of 
room for improving GHC's type checking process) is to provide some hints, for 
example mimicking System F style type application by introducing a type proxy 
argument in combination with lexically scoped type variables.

foo :: a -> Id a -> Id a
foo _ = id

foo' :: Id a -> Id a
foo' = foo (undefined :: a)


Martin


Ganesh Sittampalam wrote:
> On Wed, 9 Apr 2008, Manuel M T Chakravarty wrote:
>
>> Sittampalam, Ganesh:
>
>>> No, I meant can't it derive that equality when matching (Id a) 
>>> against (Id b)? As you say, it can't derive (a ~ b) at that point, 
>>> but (Id a ~ Id b) is known, surely?
>>
>> No, it is not know.  Why do you think it is?
>
> Well, if the types of foo and foo' were forall a . a -> a and forall b 
> . b -> b, I would expect the type-checker to unify a and b in the 
> argument position and then discover that this equality made the result 
> position unify too. So why can't the same happen but with Id a and Id 
> b instead?
>
>> The problem is really with foo and its signature, not with any use of 
>> foo. The function foo is (due to its type) unusable.  Can't you 
>> change foo?
>
> Here's a cut-down version of my real code. The type family Apply is 
> very important because it allows me to write class instances for 
> things that might be its first parameter, like Id and Comp SqlExpr 
> Maybe, without paying the syntactic overhead of forcing client code to 
> use Id/unId and Comp/unComp. It also squishes nested Maybes which is 
> important to my application (since SQL doesn't have them).
>
> castNum is the simplest example of a general problem - the whole point 
> is to allow clients to write code that is overloaded over the first 
> parameter to Apply using primitives like castNum. I'm not really sure 
> how I could get away from the ambiguity problem, given that desire.
>
> Cheers,
>
> Ganesh
>
> {-# LANGUAGE TypeFamilies, GADTs, UndecidableInstances, 
> NoMonomorphismRestriction #-}
>
> newtype Id a = Id { unId :: a }
> newtype Comp f g x = Comp { unComp :: f (g x) }
>
> type family Apply (f :: * -> *) a
>
> type instance Apply Id a = a
> type instance Apply (Comp f g) a = Apply f (Apply g a) type instance 
> Apply SqlExpr a = SqlExpr a type instance Apply Maybe Int = Maybe Int 
> type instance Apply Maybe Double = Maybe Double type instance Apply 
> Maybe (Maybe a) = Apply Maybe a
>
> class DoubleToInt s where
>castNum :: Apply s Double -> Apply s Int
>
> instance DoubleToInt Id where
>castNum = round
>
> instance DoubleToInt SqlExpr where
>castNum = SECastNum
>
> data SqlExpr a where
>   SECastNum :: SqlExpr Double -> SqlExpr Int
>
> castNum' :: (DoubleToInt s) => Apply s Double -> Apply s Int castNum' 
> = castNum
>
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

==
Please access the attached hyperlink for an important electronic communications 
disclaimer: 

http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html
==

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type families and type signatures

[Martin Sulzmann]

Manuel said earlier that the source of the problem here is foo's 
ambiguous type signature

(I'm switching back to the original, simplified example).
Type checking with ambiguous type signatures is hard because the type 
checker has to guess
types and this guessing step may lead to too many (ambiguous) choices. 
But this doesn't mean

that this worst case scenario always happens.

Consider your example again

type family Id a

type instance Id Int = Int

foo :: Id a -> Id a
foo = id

foo' :: Id a -> Id a
foo' = foo

The type checking problem for foo' boils down to verifying the formula

forall a. exists b. Id a ~ Id b

Of course for any a we can pick b=a to make the type equation statement 
hold.
Fairly easy here but the point is that the GHC type checker doesn't do 
any guessing
at all. The only option you have (at the moment, there's still lots of 
room for improving

GHC's type checking process) is to provide some hints, for example mimicking
System F style type application by introducing a type proxy argument in 
combination

with lexically scoped type variables.

foo :: a -> Id a -> Id a
foo _ = id

foo' :: Id a -> Id a
foo' = foo (undefined :: a)


Martin


Ganesh Sittampalam wrote:

On Wed, 9 Apr 2008, Manuel M T Chakravarty wrote:


Sittampalam, Ganesh:


No, I meant can't it derive that equality when matching (Id a) 
against (Id b)? As you say, it can't derive (a ~ b) at that point, 
but (Id a ~ Id b) is known, surely?


No, it is not know.  Why do you think it is?


Well, if the types of foo and foo' were forall a . a -> a and forall b 
. b -> b, I would expect the type-checker to unify a and b in the 
argument position and then discover that this equality made the result 
position unify too. So why can't the same happen but with Id a and Id 
b instead?


The problem is really with foo and its signature, not with any use of 
foo. The function foo is (due to its type) unusable.  Can't you 
change foo?


Here's a cut-down version of my real code. The type family Apply is 
very important because it allows me to write class instances for 
things that might be its first parameter, like Id and Comp SqlExpr 
Maybe, without paying the syntactic overhead of forcing client code to 
use Id/unId and Comp/unComp. It also squishes nested Maybes which is 
important to my application (since SQL doesn't have them).


castNum is the simplest example of a general problem - the whole point 
is to allow clients to write code that is overloaded over the first 
parameter to Apply using primitives like castNum. I'm not really sure 
how I could get away from the ambiguity problem, given that desire.


Cheers,

Ganesh

{-# LANGUAGE TypeFamilies, GADTs, UndecidableInstances, 
NoMonomorphismRestriction #-}


newtype Id a = Id { unId :: a }
newtype Comp f g x = Comp { unComp :: f (g x) }

type family Apply (f :: * -> *) a

type instance Apply Id a = a
type instance Apply (Comp f g) a = Apply f (Apply g a)
type instance Apply SqlExpr a = SqlExpr a
type instance Apply Maybe Int = Maybe Int
type instance Apply Maybe Double = Maybe Double
type instance Apply Maybe (Maybe a) = Apply Maybe a

class DoubleToInt s where
   castNum :: Apply s Double -> Apply s Int

instance DoubleToInt Id where
   castNum = round

instance DoubleToInt SqlExpr where
   castNum = SECastNum

data SqlExpr a where
  SECastNum :: SqlExpr Double -> SqlExpr Int

castNum' :: (DoubleToInt s) => Apply s Double -> Apply s Int
castNum' = castNum

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type families and type signatures

[Ganesh Sittampalam]

On Wed, 9 Apr 2008, Manuel M T Chakravarty wrote:


Sittampalam, Ganesh:


No, I meant can't it derive that equality when matching (Id a) against 
(Id b)? As you say, it can't derive (a ~ b) at that point, but (Id a ~ 
Id b) is known, surely?


No, it is not know.  Why do you think it is?


Well, if the types of foo and foo' were forall a . a -> a and forall b . b 
-> b, I would expect the type-checker to unify a and b in the argument 
position and then discover that this equality made the result position 
unify too. So why can't the same happen but with Id a and Id b instead?


The problem is really with foo and its signature, not with any use of foo. 
The function foo is (due to its type) unusable.  Can't you change foo?


Here's a cut-down version of my real code. The type family Apply is very 
important because it allows me to write class instances for things that 
might be its first parameter, like Id and Comp SqlExpr Maybe, without 
paying the syntactic overhead of forcing client code to use Id/unId and 
Comp/unComp. It also squishes nested Maybes which is important to my 
application (since SQL doesn't have them).


castNum is the simplest example of a general problem - the whole point is 
to allow clients to write code that is overloaded over the first parameter 
to Apply using primitives like castNum. I'm not really sure how I could 
get away from the ambiguity problem, given that desire.


Cheers,

Ganesh

{-# LANGUAGE TypeFamilies, GADTs, UndecidableInstances, 
NoMonomorphismRestriction #-}


newtype Id a = Id { unId :: a }
newtype Comp f g x = Comp { unComp :: f (g x) }

type family Apply (f :: * -> *) a

type instance Apply Id a = a
type instance Apply (Comp f g) a = Apply f (Apply g a)
type instance Apply SqlExpr a = SqlExpr a
type instance Apply Maybe Int = Maybe Int
type instance Apply Maybe Double = Maybe Double
type instance Apply Maybe (Maybe a) = Apply Maybe a

class DoubleToInt s where
   castNum :: Apply s Double -> Apply s Int

instance DoubleToInt Id where
   castNum = round

instance DoubleToInt SqlExpr where
   castNum = SECastNum

data SqlExpr a where
  SECastNum :: SqlExpr Double -> SqlExpr Int

castNum' :: (DoubleToInt s) => Apply s Double -> Apply s Int
castNum' = castNum

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type families and type signatures

[Manuel M T Chakravarty]

Sittampalam, Ganesh:

Manuel Chakravarty wrote:

Ganesh Sittampalam:

On Mon, 7 Apr 2008, Manuel M T Chakravarty wrote:


Ganesh Sittampalam:

The following program doesn't compile in latest GHC HEAD, although
it does if I remove the signature on foo'. Is this expected?


Yes, unfortunately, this is expected, although it is very
unintuitive. This is for the following reason.

Let's alpha-rename the signatures and use explicit foralls for
clarity:

foo  :: forall a. Id a -> Id a
foo' :: forall b. Id b -> Id b

GHC will try to match (Id a) against (Id b).  As Id is a type  
synonym

family, it would *not* be valid to derive (a ~ b) from this.  After
all, Id could have the same result for different argument types.
(That's not the case for your one instance, but maybe in another
module, there are additional instances for Id, where that is the
case.)


Can't it derive (Id a ~ Id b), though?


That's what it does derive as a proof obligation and finds it can't  
prove.
The error message you are seeing is GHC's way of saying, I cannot  
assert that

(Id a ~ Id b) holds.


No, I meant can't it derive that equality when matching (Id a)  
against (Id b)?
As you say, it can't derive (a ~ b) at that point, but (Id a ~ Id b)  
is known,

surely?


No, it is not know.  Why do you think it is?


Generally speaking, is there any way to give a signature to foo'?



Sorry, but in the heat of explaining what GHC does, I missed the
probably crucial point.  Your function foo is useless, as is foo'.
Not only can't you rename foo (to foo'), but you generally can't use
it.  It's signature is ambiguous.  Try evaluating (foo (1::Int)).   
The

problem is related to the infamous (show . read).


My real code is somewhat analogous to (foo :: (Id Int -> Id Int))  
(1::Int).
Isn't that unambiguous in the same way as (show.read) is if I give  
show or

read a signature?


No.  The problem with a functions that has an ambiguous signature is  
that it contains type variables that are impossible to constrain by  
applying the function.  Providing a type signature at the application  
site makes this no easier.  Why?  Consider what a type annotation  
means.  By writing e :: t, you express your intent to use e at type t,  
but you also force the compiler to check that whatever type it derives  
for e is more general than t.  It is this check for type subsumption  
that is the tricky bit when typing TFs (or FDs).  See  for more detail on why this is a hard problem.


The problem with an ambiguous signature is that the subsumption check  
always fails, because the ambiguous signature contains some type  
variables for which the type checker cannot deduce a type instance.   
(You as a human reader may be able to *guess* an instance, but HM- 
based inference does generally not guess.  It's a deterministic  
process.)


The problem is really with foo and its signature, not with any use of  
foo.  The function foo is (due to its type) unusable.  Can't you  
change foo?


Manuel



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

RE: [Haskell-cafe] type families and type signatures

[Sittampalam, Ganesh]

Manuel Chakravarty wrote:
>Ganesh Sittampalam:
>> On Mon, 7 Apr 2008, Manuel M T Chakravarty wrote:
>>
>>> Ganesh Sittampalam:
 The following program doesn't compile in latest GHC HEAD, although 
 it does if I remove the signature on foo'. Is this expected?
>>>
>>> Yes, unfortunately, this is expected, although it is very 
>>> unintuitive. This is for the following reason.
>>>
>>> Let's alpha-rename the signatures and use explicit foralls for
>>> clarity:
>>>
>>> foo  :: forall a. Id a -> Id a
>>> foo' :: forall b. Id b -> Id b
>>>
>>> GHC will try to match (Id a) against (Id b).  As Id is a type synonym 
>>> family, it would *not* be valid to derive (a ~ b) from this.  After 
>>> all, Id could have the same result for different argument types.  
>>> (That's not the case for your one instance, but maybe in another 
>>> module, there are additional instances for Id, where that is the 
>>> case.)
>>
>> Can't it derive (Id a ~ Id b), though?

> That's what it does derive as a proof obligation and finds it can't prove.
> The error message you are seeing is GHC's way of saying, I cannot assert that
> (Id a ~ Id b) holds.

No, I meant can't it derive that equality when matching (Id a) against (Id b)?
As you say, it can't derive (a ~ b) at that point, but (Id a ~ Id b) is known,
surely?

> > Generally speaking, is there any way to give a signature to foo'?

> Sorry, but in the heat of explaining what GHC does, I missed the  
> probably crucial point.  Your function foo is useless, as is foo'.   
> Not only can't you rename foo (to foo'), but you generally can't use  
> it.  It's signature is ambiguous.  Try evaluating (foo (1::Int)).  The  
> problem is related to the infamous (show . read).

My real code is somewhat analogous to (foo :: (Id Int -> Id Int)) (1::Int).
Isn't that unambiguous in the same way as (show.read) is if I give show or
read a signature?

Cheers,

Ganesh

==
Please access the attached hyperlink for an important electronic communications 
disclaimer: 

http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html
==

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type families and type signatures

[Manuel M T Chakravarty]

Ganesh Sittampalam:

On Mon, 7 Apr 2008, Manuel M T Chakravarty wrote:


Ganesh Sittampalam:
The following program doesn't compile in latest GHC HEAD, although  
it does if I remove the signature on foo'. Is this expected?


Yes, unfortunately, this is expected, although it is very  
unintuitive. This is for the following reason.


Let's alpha-rename the signatures and use explicit foralls for  
clarity:


foo  :: forall a. Id a -> Id a
foo' :: forall b. Id b -> Id b

GHC will try to match (Id a) against (Id b).  As Id is a type  
synonym family, it would *not* be valid to derive (a ~ b) from  
this.  After all, Id could have the same result for different  
argument types.  (That's not the case for your one instance, but  
maybe in another module, there are additional instances for Id,  
where that is the case.)


Can't it derive (Id a ~ Id b), though?


That's what it does derive as a proof obligation and finds it can't  
prove.  The error message you are seeing is GHC's way of saying, I  
cannot assert that (Id a ~ Id b) holds.


Now, as GHC cannot show that a and b are the same, it can also not  
show that (Id a) and (Id b) are the same.  It does look odd when  
you use the same type variable in both signatures, especially as  
Haskell allows you to leave out the quantifiers, but the 'a' in the  
signature of foo and the 'a' in the signatures of foo' are not the  
same thing; they just happen to have the same name.


Sure, but forall a . Id a ~ Id a is the same thing as forall b . Id  
b ~ Id b.




Thanks for the explanation, anyway. I'll need to have another think  
about what I'm actually trying to do (which roughly speaking is to  
specialise a general function over type families using a signature  
which I think I need for other reasons).


Generally speaking, is there any way to give a signature to foo'?


Sorry, but in the heat of explaining what GHC does, I missed the  
probably crucial point.  Your function foo is useless, as is foo'.   
Not only can't you rename foo (to foo'), but you generally can't use  
it.  It's signature is ambiguous.  Try evaluating (foo (1::Int)).  The  
problem is related to the infamous (show . read).


Manuel

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type families and type signatures

[Ganesh Sittampalam]

On Mon, 7 Apr 2008, Manuel M T Chakravarty wrote:


Ganesh Sittampalam:
The following program doesn't compile in latest GHC HEAD, although it does 
if I remove the signature on foo'. Is this expected?


Yes, unfortunately, this is expected, although it is very unintuitive. 
This is for the following reason.


Let's alpha-rename the signatures and use explicit foralls for clarity:

foo  :: forall a. Id a -> Id a
foo' :: forall b. Id b -> Id b

GHC will try to match (Id a) against (Id b).  As Id is a type synonym family, 
it would *not* be valid to derive (a ~ b) from this.  After all, Id could 
have the same result for different argument types.  (That's not the case for 
your one instance, but maybe in another module, there are additional 
instances for Id, where that is the case.)


Can't it derive (Id a ~ Id b), though?

Now, as GHC cannot show that a and b are the same, it can also not show that 
(Id a) and (Id b) are the same.  It does look odd when you use the same type 
variable in both signatures, especially as Haskell allows you to leave out 
the quantifiers, but the 'a' in the signature of foo and the 'a' in the 
signatures of foo' are not the same thing; they just happen to have the same 
name.


Sure, but forall a . Id a ~ Id a is the same thing as forall b . Id b ~ Id 
b.


Thanks for the explanation, anyway. I'll need to have another think about 
what I'm actually trying to do (which roughly speaking is to specialise a 
general function over type families using a signature which I think I need 
for other reasons).


Generally speaking, is there any way to give a signature to foo'?

Given that this is a confusing issue, I am wondering whether we could improve 
matters by giving a better error message, or an additional hint in the 
message.  Do you have any suggestion regarding what sort of message might 
have helped you?


I can't think of anything good. Perhaps printing out the (type classes + 
equalities) context would have helped me to see that it was empty and 
understand why, but probably not.


Cheers,

Ganesh
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type families and type signatures

[Ganesh Sittampalam]

On Sun, 6 Apr 2008, Thomas M. DuBuisson wrote:


Id is an operation over types yielding a type, as such it doesn't make
much sense to me to have (Id a -> Id a) but rather something like (a ->
Id a).  One could make this compile by adding the obvious instance:


type instance Id a = a


Curiously, is this a reduction from a real world use of families?  I
just can't think of how a (Fam a -> Fam a) function would be of use.


Yes, it's cut down from an example where (I think) I really need the type 
signature to specialise a general function that does do something useful. 
The generalised intstance above wouldn't be valid or sensible in that 
context.


Cheers,

Ganesh
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type families and type signatures

[Manuel M T Chakravarty]

Ganesh Sittampalam:
The following program doesn't compile in latest GHC HEAD, although  
it does if I remove the signature on foo'. Is this expected?


Yes, unfortunately, this is expected, although it is very  
unintuitive.  This is for the following reason.


Let's alpha-rename the signatures and use explicit foralls for clarity:

  foo  :: forall a. Id a -> Id a
  foo' :: forall b. Id b -> Id b

GHC will try to match (Id a) against (Id b).  As Id is a type synonym  
family, it would *not* be valid to derive (a ~ b) from this.  After  
all, Id could have the same result for different argument types.   
(That's not the case for your one instance, but maybe in another  
module, there are additional instances for Id, where that is the case.)


Now, as GHC cannot show that a and b are the same, it can also not  
show that (Id a) and (Id b) are the same.  It does look odd when you  
use the same type variable in both signatures, especially as Haskell  
allows you to leave out the quantifiers, but the 'a' in the signature  
of foo and the 'a' in the signatures of foo' are not the same thing;  
they just happen to have the same name.


BTW, here is the equivalent problem using FDs:

  class IdC a b | a -> b
  instance IdC Int Int

  bar :: IdC a b => b -> b
  bar = id

  bar' :: IdC a b => b -> b
  bar' = bar

Given that this is a confusing issue, I am wondering whether we could  
improve matters by giving a better error message, or an additional  
hint in the message.  Do you have any suggestion regarding what sort  
of message might have helped you?


Manuel


{-# LANGUAGE TypeFamilies #-}
module Test7 where

type family Id a

type instance Id Int = Int

foo :: Id a -> Id a
foo = id

foo' :: Id a -> Id a
foo' = foo
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type families and type signatures

[Thomas M. DuBuisson]

Id is an operation over types yielding a type, as such it doesn't make
much sense to me to have (Id a -> Id a) but rather something like (a ->
Id a).  One could make this compile by adding the obvious instance:

> type instance Id a = a

Curiously, is this a reduction from a real world use of families?  I
just can't think of how a (Fam a -> Fam a) function would be of use.

Cheers,
Thomas

Ganesh Sittampalam wrote:
> The following program doesn't compile in latest GHC HEAD, although it does 
> if I remove the signature on foo'. Is this expected?
> 
> Cheers,
> 
> Ganesh
> 
> {-# LANGUAGE TypeFamilies #-}
> module Test7 where
> 
> type family Id a
> 
> type instance Id Int = Int
> 
> foo :: Id a -> Id a
> foo = id
> 
> foo' :: Id a -> Id a
> foo' = foo
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe