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

[Claus Reinke]

> 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