haskell-cafe@haskell.org
[Top] [All Lists]

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

Subject: Re: [Haskell-cafe] Language extensions [was: Memoization]
From: Andrew Coppin
Date: Tue, 29 May 2007 21:28:07 +0100
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.)

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

<Prev in Thread] Current Thread [Next in Thread>