[Haskell-cafe] Re: Typed Lambda-Expressions withOUT GADTs

[Keean Schupke]

Conor McBride wrote:

>
> Yeah, that's nice. Scoped type variables are really handy for this sort
> of thing. You've got rid of the annotation on application (hey, what are
> typecheckers for?) but it's not so easy to lose it on the lambda: you
> need that for the fundep. To have a good story here, we need to show
> either how to get rid of the fundep or how to ensure we always have one.
>
Well, you cannot get rid of it, as otherwise the result types would need to
be explicitly given (and if you saw the type of 'test3' you know that is 
impractical
as the type was several screens-full)

However I don't understand what you meed by 'ensuring you always have 
one'...
As far as I understand it we are lifting a value level operation (a type 
with
several constructors) to the type level (a class containing several 
types) in this
case each 'class' models a function. A generalised function has a type:

    f :: a -> b

When lifted to a class this becomes:

    class F a b | a -> b ...

So the fundep is implicit in the function we are lifting... And just 
like function
pattern guards need to have a unique contructor (head) to differentiate 
them, we
require a unique type (head) to select an instance under a fundep...

Infact it seems to me a fundep is much more general than a function, you 
cannot
write a function to do:

    class F a b | b -> a where
       f :: a -> b
    instance F (Z a) (A a)
    instance F (Y a) (B a)

where the return type determines the type of the parameter...

    Keean.