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!-) 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). typical uses are tagging another value with a separate, more precise type (so that we can talk either about the value's own type, or about the type tag associated with it), or enabling type-level meta-programming via type classes. so, if we have data O = O data S a = S a data T a phantom = T a we can distinguish between (T True :: T Bool O) and (T True :: T Bool (S O)) - even though they have the same value, they differ in the phantom component of their types. if you think of 'O' as 'Object' and 'S O' as some subclass of 'O' (in the oop sense), this allows us to see the same value as an instance of different (oop-style) classes, which has been used for foreign function interfaces to oop languages. monomorphism: a monomorphic type is a type without type variables (such as '[Char]') polymorphism: a polymorphic type is a generalisation of a monomorphic type (in other words, we have replaced some concrete subterms of a type with type variables; as in '[a]'). polymorphic types involve implicit or explicit all-quantification over their type variables (in other words, a polymorphic type stands *for all* monomorphic types that can be obtained by substituting types for type variables; so 'forall a.[a]' stands for '[Char]' and '[Bool]', among others) 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 .. qualified types: type classes allow us to constrain type variables in quantified types to instances of specified classes. so, rather than assuming that equality can be defined on all types, or using type-specific symbols for equality at different types, we can define a single overloaded equality function defined over all types which provide an equality test ('(==) :: forall a. Eq a => a -> a -> Bool'). 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]) 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). another use is in container types, such as '[(Char,Bool)]', when we want to refer both to the full type and to some of the contained types. we cannot always use type constructor classes, because we cannot easily compose type constructors: class C container element where c :: container element -> element instance C ([].(,Bool)) Char -- !! invented syntax here.. where c ((c,b):_) = b we can use multi-parameter type classes, with a functional dependency that specifies that if we know the full type, the element type will be uniquely determined: class D full element | full -> element where d :: full -> element instance D [(Char,Bool)] Bool where d ((c,b):_) = b note that without the functional dependency here, instance selection would be determined by the return type of 'd', not by the argument type. and we'd always have to sprinkle type signatures throughout our code to make sure that the return type is neither ambiguous nor different from the type we want. gadts: some people like them just for their syntax, as they allow data constructors to be specified with their full type signatures, just like any other function. some people like them for having existential type syntax 'built-in'. but 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 (in other words, matching on a specific construct allows us to operate on a specific type, rather than the general type "sum of all alternative constructs"). those construct-specific types can often be phantom types (and many uses of gadts can be encoded in non-generalised algebraic data types, using existential quantification and phantom types). as one example, we can try to encode the emptyness of lists in their types, so that functions like 'listLength' still work on both empty and non-empty lists, but functions like 'listHead' can only be applied to non-empty lists (this example is too simplistic, as you'll find out if you try to define 'listTail';-). data TTrue = TTrue data TFalse = TFalse data List a nonEmpty where Nil :: List a TFalse Cons :: a -> List a ne -> List a TTrue listLength :: List a ne -> Int listLength Nil = 0 listLength (Cons h t) = 1+listLength t listHead :: List a TTrue -> a listHead (Cons h t) = h *Main> let n = Nil *Main> let l = Cons 1 (Cons 2 Nil) *Main> :t n n :: List a TFalse *Main> :t l l :: List Integer TTrue *Main> listLength n 0 *Main> listLength l 2 *Main> listHead n <interactive>:1:9: Couldn't match expected type `TTrue' against inferred type `TFalse' Expected type: List a TTrue Inferred type: List a TFalse In the first argument of `listHead', namely `n' In the expression: listHead n *Main> listHead l 1