Example:
data IdFun = IdCon (a -> a)Here IdCon can only be applied to values which have type for all a.a->a. This means that the application "IdCon id" is type correct, whereas "IdCon negate" is wrong since negate does not have type a->a for all a.
When such a value is deconstructed (in pattern matching) it regains its universal quantification. Type correct example:
f (IdCon g) = (g 'a', g True)Notice how g is applied to arguments of different types; this is normally not possible with lambda bound variables.
A universally quantified type variable can have a context as well, e.g.
data NumOps = (Num a) => NumOps { square :: a->a, cube :: a->a }
numOps = NumOps { square = \x->x*x, cube = \x->x*x*x }
f :: (Num a) => NumOps -> a -> a
f (NumOps { square, cube }) x = cube (square x)
data T = C ?a (?a->Int)Here ?a is free (since it does not appear after T) and thus existentially quantified. When constructing values C is polymorphic as usual.
hetl = [C 4 (+1), C [1,2] length, C 3.14 toInt]This list has typing hetl::[T], but is really heterogenous since the elements have different types. When a constructor with a existentially quantified type is used in pattern matching it behaves differently. The actual type of the quantified variable is not allowed to escape outside the expression tied to the pattern matching. The following function is allowed
f c =
case c of
C v f -> f v
since it has typing f::T->Int, but not this
g c =
case c of
C x y -> x
since the actual type of x is not known.
Existentially quantified variables can also be constrained by giving
a context before a constructor. The following defines a type where the
argument to the constructor has to have a type belonging to class Show.
data TShow = (Show ?a) => T ?aThis can be used as follows:
l :: [TShow] l = [T True, T 1, T (atan 1), T [True]] s = map show land the value of s will be ["True","1","7.8539816339744828e-1","[True]"].
The automatic derivation of instance declarations does not work for types containing existentially quantified variables.
NOTE The current implementation does not allow mixing universal and existential quantification within a single constructor. As soon as one type variable starts with a `?' all free type variables are considered to be existential.
The restrictions on instance declarations are relaxed if the flag -no-pedantic. Normally instance declarations can have the form
instance K => C (T a1 ... an)where a1 ... an are type vars. With the flags they can be of the form
instance K => C (T t1 ... tn)where t1 ... tn are arbitrary type expressions. If more than one instance declaration can be used to resolve an overloading the following rule is used:
If there is a single most specific declaration (in the usual type specialisation ordering) then this is used, otherwise an ambiguity error is reported.This means that you can make declarations like
instance Eq [Char] where ...and make a special purpose fast comparison routine for strings and get this whenever strings are compared. So far this has not been used anywhere in the Prelude, but a faster version of Ratio Integer (coded in C) will probably be included in a future version.
This is a dubious feature and should not be used carelessly.
newtype T f = T (f Int)You can get a similar behaviour from hbc by specifying the -fno-bad-eval-inst flag.
type List = []is legal Haskell 1.4, but not possible in hbc. Use
type List a = [a]instead.