[Haskell-cafe] Language extensions [was: Memoization]

[Andrew Coppin]

Claus Reinke wrote:
>
>> I'm thinking more about things like phantom types, rank-N 
>> polymorphism, functional dependencies, GADTs, etc etc etc that nobody 
>> actually understands.
>
> this seems to be overly polymorphic in generalising over all types of
> Haskell programmers, rather than admitting the existence of some types
> of programmers who might have different values. qualifying such
> generalisations by grouping types of programmers into classes with
> different methods would seem a more Haskellish way, don't you think?-)
>
> and although it isn't nice to typecast people, sometimes one only needs
> to know the type, not the person, and sometime one needs even less
> information, such as a property of a type or its relation to other
> types. and especially if one is interested in relationships between
> different types, it is helpful to know if one type of person in such a
> relationship always occurs in combination with one and the same other
> type. and if there are times when one might even generalise over
> generalisations (although one doesn't like to generalise over so many
> people all at once;-), there are other times when one might need to be
> rather specific about which of several possible alternative types one is
> putting together in a single construction.
>
> there, does that cover everything in that list? sorry, couldn't
> resist!-)

Hahahaha!

Thanks for a good laugh! I should print this out and *frame* it or 
something...

> in exchange, below is a quick summary (didn't we have a
> dictionary/quick-reference somewhere at haskell.org? i can't seem to 
> find it right now, but if you know where it is, and it doesn't
> already contain better explanations, feel free to add the text below - 
> but check the draft for errors first, please;)
>
> claus
>
> ------------------------------
> phantom types:
>  the types of ghost values (in other words, we are only interested in
>  the type, not in any value of that type).

Mmm... Still not seeing a great amount of use for this one.

> quantified types (forall/exist):
>  an easy way to memorize this is to think of 'forall' as a big 'and'
>  and of 'exists' as a big 'or'.
>    e :: forall a. a  -- e has type 'Int' and type 'Bool' and type ..
>    e :: exists a. a  -- e has type 'Int' or  type 'Bool' or  type ..

That doesn't entirely make sense. (What am I on about? That doesn't make 
*any* sense...)

> rank-N polymorphism:
>  in rank-1 polymorphism, type variables can only stand for monomorphic
>  types (so, '($) :: (a->b) -> a -> b' can only apply monomorphic
>  functions to their arguments, and polymorphic functions are not
>  first-class citizens, as they cannot be passed as parameters without
>  their types being instantiated). in rank-N (N>1) polymorphism,
>  type-variables can stand for rank-(N-1) polymorphic types (in other
>  words, polymorphic functions can now be passed as parameters, and used
>  polymorphically in the body of another function).
>
>    f :: (forall a. [a]->Int) -> ([c],[d]) -> (Int,Int)
>    f g (c,d) = (g c,g d)
>
>    f length ([1..4],[True,False])

It's actually news to me that you can't do this already... (!)

> functional dependencies:
>  when using multi-parameter type classes, we specify relations between
>  types (taken from the cartesian product of type class parameters).
>
>  without additional measures, that tends to lead to ambiguities (some
>  of the type class parameters can not be deduced unambiguously from the
>  context, so no specific type class instance can be selected).
>
>  functional dependencies are one such measure to reduce ambiguities,
>  allowing us to specify that some subset A of type-class parameters
>  functionally determines another subset B (so if we know the types of
>  the parameters in subset A, there is only a single choice for the
>  types of the parameters in subset B).

Functional dependancies kind of make sense. Personally I like the idea 
of associated types better, but never mind.

> gadts:
>  what really makes them different is that
>  the explicit type signatures for the data constructors can give more
>  specific return types for the data constructs, and such more specific
>  types can be propagated through pattern matching

Finally, a definition of GADTs that actually makes some kind of sense...

(I find it highly unlikely I'll ever need these, but at least I have 
some idea now what they're supposed to do.)