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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
