[Haskell-cafe] Re: Typed Lambda-Expressions withOUT GADTs
Keean Schupke
k.schupke at imperial.ac.uk
Tue Jan 4 06:16:58 EST 2005
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.
More information about the Haskell-Cafe
mailing list