Parametric polymorphism is parameterization of a term by a type, permitting the term to be used in differently-typed contexts. Types of polymorphic terms contain universal quantification. For the sake of inference and ease of type-checking, mainstream functional programming languages restrict where in the type the quantifiers may appear and over what they quantify. Hindley-Milner system, or core ML, limits polymorphism to rank-1 (prenex): all quantifiers in a type must be at the front and quantify over monomorphic types. OCaml and Haskell relax the rank restriction, permitting quantifiers inside certain types such as records. Haskell also permits parameterization by arbitrary type constructors: we can define a tree data type abstracting not only over the type of leaf values but also over the type of the collection to hold node's children.
We do encounter problems that run into the limits of polymorphism in Haskell, let alone in ML. We may need to parameterize by type functions that are not constructors; we may need to quantify over not only types but also kinds. Or we think we need. Some of these demanding problems turn out solvable in Haskell or even ML. On this page we collect such examples. Most of the code is simple OCaml, demonstrating that the plain Hindley-Milner system can be surprisingly expressive.
n
; The function then takes n
other arguments and returns them as the n
-element list. It seems the function should have the type n -> ('a ->)^{n} -> 'a list
, which is of course not possible in OCaml.The solution takes three lines; the first two define the building blocks of our numerals -- zero and the successor. The third line defines the desired function p
. An indented line after each definition shows the response of the OCaml top-level, with the inferred type for each function.
let n0 = fun k -> k [];; val n0 : ('a list -> 'b) -> 'b = <fun> let s n k x = n (fun v -> k (x::v));; val s : (('a list -> 'b) -> 'c) -> ('a list -> 'b) -> 'a -> 'c = <fun> let p sel = sel (fun x -> x);; val p : (('a -> 'a) -> 'b) -> 'b = <fun>We use the function
p
as follows. (Again, an indented line underneath each statement is the response of the OCaml top-level.)p n0;; - : 'a list = [] p (s n0) 1;; - : int list = [1] p (s (s n0)) 1 2;; - : int list = [1; 2] p (s (s (s n0))) 'a' 'b' 'c';; - : char list = ['a'; 'b'; 'c']
Polyvariadic zipWith
and the tautology checker of boolean functions of arbitrary many arguments are described in the Functional Pearl
Daniel Fridlender and Mia Indrika: Do We Need Dependent Types? J. Functional Programming, 2000, v10, N4, pp. 409-415
< http://www.math.chalmers.se/~indrika/jfp.ps.gz >
The concluding section of the paper thoroughly discusses the custom numeral approach.
Polyvariadic functions and keyword arguments
The introduction section of that page describes several other simple encodings of polyvariadic functions, including a simple Forth-like interpreter.
double_generic.ml [6K]
A simple generalization: a generic `function' (or, recipe) that can be instantiated to different data types (sums, products, lists) and to the different number of arguments. In effect, we unify the generic map
with the polyvariadic zipWith
.
The problem is to select a component from two tuples. If the tuples are
homogeneous, the problem is easy: we define the function
f1
that takes a selector as the argument. To select a component, we apply
f1
either to fst
or to snd
. (An indented line below
each definition or statement shows the response of the OCaml top-level.)
let f1 sel = (sel (1,2), sel (3,4));; val f1 : (int * int -> 'a) -> 'a * 'a = <fun> f1 fst;; - : int * int = (1, 3) f1 snd;; - : int * int = (2, 4)
Heterogeneous tuples cause serious trouble, however. For example:
let f2 sel = (sel (1,'b'), sel (true,"four"));; Error: This expression has type bool * string but an expression was expected of type int * charThe first problem is indicated in the error message. In a Hindley-Milner system, function arguments must be monomorphic. Therefore, it is not possible to apply
sel
(received as the argument to f2
)
to the pairs of different types. There is another problem with f2
.
Let us try to define this function in the less restrictive System F:let f2 (sel: forall a b. (a,b) -> a) = (sel @ int @ char (1,'b'), sel @ bool @ string (true,"four"))where
@
is the type application. We can apply f2
to fst
without trouble:
f2 (Fun ta tb -> fun (x:ta,y:tb) -> x)
assuming the notation Fun
for the type abstraction. Alas,
we cannot apply f2
to snd
, which has a different polymorphic
type forall a b. (a,b) -> b
. Even System F is not expressive to write
f2
. We need an abstraction not only over types but over arbitrary
type functions of the kind * -> * -> *
.
It turns out the selection from heterogeneous tuples is expressible in a
Hindley-Milner system. If we look back at f2
, we notice that there
are only two choices for sel
. Therefore, we can compute the applications
f2 fst
and f2 snd
separately, and later choose between the two results.
We use thunks to delay the computations until chosen.
let f3 = (* f2 applied to fst *) let f2_fst () = (fst (1,'b'), fst (true,"four")) in (* f2 applied to snd *) let f2_snd () = (snd (1,'b'), snd (true,"four")) in fun sel -> sel (f2_fst, f2_snd) () val f3 : ((unit -> int * bool) * (unit -> char * string) -> unit -> 'a) -> 'a = <fun> f3 fst;; - : int * bool = (1, true) f3 snd;; - : char * string = ('b', "four")
The trick is a higher-order version of the technique commonly used in partial evaluation. It is related to `narrowing' in functional-logic programming. It is essentially the eta-rule for sums:
fun x -> C[match x with V1 -> e1 | V2 -> e2] ==> fun x -> match x with V1 -> C[e1] | V2 -> C[e2]where the context
C[]
does not bind x
.g
that takes a selector such as the tuple selectorfst :: forall a b. (a,b) -> a snd :: forall a b. (a,b) -> bas an argument and applies it to several heterogeneous tuples. For example:
g sel = (sel (1,'b'), sel (true,"four"))It is already a problem to type such a function in System F, let alone in the Hindley-Milner system. But we want more: a function that takes functions like
g
as an argument. The original problem was
posed by Vladimir Reshetnikov on the Haskell-Cafe mailing list on June
6, 2009. We describe here an elaborated version: We would like to type
check the following definition of the function fs
along with several
examples of its use.fs g = (g snd, (), g fst) t1 = fs id t2 = fs (:[]) t3 = fs (\sel -> sel (True,False)) t4 = fs (\sel -> sel (True,"False")) t5 = fs (\sel -> head $ sel ([True],"False")) t6 = fs (\sel -> (sel (1,'b'), sel (true,"four")))The examples
t1
through t3
type check in Haskell98; the others
are flagged as ill-typed. Indeed, the inferred type of
fs
is (((a, a) -> a) -> t) -> (t, (), t)
,
betraying the selection from tuples whose components have the same
type. In the example t4
the selector is applied to the patently
heterogeneous tuple. We saw earlier that the type of a function taking a tuple
selector as an argument must be parametrized by a type function of the kind
* -> * -> *
. Such polymorphism is already not representable in
System F. Now we wish to pass such a function as an argument to fs
.First we show a brute-force solution, emulating the necessary higher-rank polymorphism. Then we change the point of view and the problem becomes trivial. The complex solution introduces an extra level of interpretation:
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-} {-# LANGUAGE FunctionalDependencies, UndecidableInstances #-} data Fst = Fst data Snd = Snd fs g = (apply g Snd, (), apply g Fst)replacing the functions like
fst
and snd
with their
`encodings' fstE
and sndE
, to be interpreted by the
extensible interpreter Apply
. The base cases of the interpreter are:class Apply f x y | f x -> y where apply :: f -> x -> y instance Apply (x->y) x y where apply = ($) instance Apply Fst (x,y) x where apply _ = fst instance Apply Snd (x,y) y where apply _ = sndTo write the simple tests
t1
through t3
we add the encoding
for functions that can be passed as arguments of fs
.
Representing functions by their encoding lets us get around the
too complex polymorphism:newtype Sel a w = Sel (((a,a) -> a) -> w) t1 = fs (Sel id) t2 = fs (Sel (:[])) t3 = fs (Sel (\sel -> sel (True,False))) -- (False,(),True) instance Apply (Sel a w) Fst w where apply (Sel f) _ = f fst instance Apply (Sel a w) Snd w where apply (Sel f) _ = f sndThat encoding is too simple for
t4
. Hence we introduce a more
complex encoding, and extend our interpreter:newtype PSel obj = PSel obj instance Apply Fst obj w => Apply (PSel obj) Fst w where apply (PSel obj) _ = apply Fst obj instance Apply Snd obj w => Apply (PSel obj) Snd w where apply (PSel obj) _ = apply Snd obj t13 = fs (PSel (True,False)) t4 = fs (PSel (True,"False")) -- ("False",(),True)Alas, to express
t5
and t6
we have to complicate our encoding further
still.
Let us pause however. The number of selectors is finite and small;
for example, there are only two selectors from tuples, fst
and
snd
. This gives us an idea to represent the function g
as a `table',
`indexed' by the selector argument. This change of representation is
quite like applying the eta-rule for sums. The function fs
will receive the table: a pair of the results (g fst, g snd)
.
g' = (g_fst, g_snd) where g_fst = (fst (1,'b'), fst (True,"four")) g_snd = (snd (1,'b'), snd (True,"four")) fs g' = (snd g', (), fst g') t1 = fs (id,id) t2 = fs ((:[]),(:[])) t3 = fs (True,False) t4 = fs (True,"False") -- ("False",(),True) t5 = fs (head [True], head "False") -- ('F',(),True) t6 = fs g' -- (('b',"four"),(),(1,True))Thanks to the non-strict evaluation of Haskell, the results are not actually computed unless needed. This code type checks in Haskell98, or any Hindley-Milner system. Changing the representation made the problem trivial.
Haskell with only one typeclass
Another extensive example of Apply (called C in that code)
read :: Read a => String -> a fromInteger :: Num a => Integer -> aare the examples of parameterizing a term by a type, which is constrained to be a member of a type class, Read or Num, respectively. With rank-2 polymorphism, we can write terms that accept polymorphic functions like
read
and fromInteger
as arguments, for example:foo :: (Num c, Num d) => (forall b. Num b => a -> b) -> a -> (c, d) foo f x = (f x, f x) bar :: (Read c, Read d) => (forall b. Read b => a -> b) -> a -> (c, d) bar f x = (f x, f x) testFoo = foo fromInteger 1 :: (Int, Float) -- (1,1.0) testBar = bar read "1" :: (Int, Float) -- (1,1.0)Since higher-rank types in general cannot be inferred, we must supply signatures for the functions
foo
and bar
. Writing signatures for top-level functions is overall a good habit. If the functions foo
and bar
were local however, defined in a where
clause, we must still write their full signatures -- and that is annoying.The functions foo
and bar
illustrate parameterizing terms by polymorphic terms. Bas van Dijk has observed that foo
and bar
look quite alike. It is tempting to abstract away the difference between them, generalizing foo
and bar
to a single function baz
to be used like
testBaz1 = baz fromInteger 1 :: (Int, Float) testBaz2 = baz read "1" :: (Int, Float)The only difference between
foo
and bar
is the type class constraint: Num
for foo
and Read
for bar
. The desired term baz
must therefore be parameterized by a type class. The article develops the solution without resorting to the recently added Constraint kind, showing that first-class constraints have always been available in Haskell.It turns out that quantification over a type class is easy, after we add a layer of indirection. We introduce a type class that relates, or interprets, types as type classes. That type class acts as a look-up table from types to type class constraints. We can now use ordinary types to represent type classes. Ordinary polymorphism -- parameterization over types -- becomes in effect parameterization over type classes.
We implement the idea as follows, using these extensions:
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-} {-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}Although functional dependencies are required, overlapping or undecidable instances are not. We also get by without exotic extensions such as mutually recursive instances, required by `SYB with class.'
We define the ``look-up table'' from types to type classes as the following type class:
class Apply l a b | l b -> a where apply :: l -> a -> bThe type class is the generalization of the ordinary function application. We can even give the following instance for it (although we won't be needing it here).
instance Apply (a->b) a b where apply = ($)We now add two entries into our look-up table from types to type classes. The types
LRead
and LFromInt
below will act as look-up keys.data LRead = LRead instance Read b => Apply LRead String b where apply _ = read data LFromInt = LFromInt instance Num b => Apply LFromInt Integer b where apply _ = fromIntegerThe type
LRead
indeed relates to the type class constraint Read
while LFromInt
relates to Num
. We are done. The function baz
is simplybaz f x = (apply f x, apply f x)to be used as follows:
testBaz1 = baz LFromInt 1 :: (Int, Float) testBaz2 = baz LRead "1" :: (Int, Float)Incidentally, if it were not for the polymorphic numeric literal
1
, we could have defined Apply
with only two parameters and without the functional dependency.Although we have accomplished a seemingly high-ranking polymorphism, rank-2 types emphatically were not needed. Therefore, all types are inferred. We did not have to write the signature for baz
. It is still interesting to see what the type checker has inferred:
*Main> :t baz baz :: (Apply l a b, Apply l a b1) => l -> a -> (b, b1)The type of
baz
does show it to be a generalization of both foo
and bar
. The term is polymorphic over the type l
of keys in our look-up table of type class constraints. In effect, baz
is polymorphic over type classes -- as desired.Since a type class acts as a type predicate in Haskell, quantification over arbitrary type predicates gives us the unrestricted set comprehension. We should be able to write something like Russell paradox. Indeed we can. The following code understandably needs the UndecidableInstances extension.
data Delta = Delta instance Apply l l b => Apply Delta l b where apply _ x = apply x xThe definition of
apply
is not recursive: the method apply
for the instance Apply Delta l b
is defined in terms of a generally different apply
method, for the instance Apply l l b
. However, we may, later on, instantiate l
to be Delta
. After all, the quantification in the above instance is impredicative, over a class that includes the instance being defined. We introduceomega () = apply Delta Deltawhose inferred type
*Main> :t omega omega :: () -> bleaves no doubts about the behavior of the term:
omega ()
promises to produce a value of any type whatsoever. Of course the evaluation of omega ()
does not terminate. Since apply
is sort of a functional application, the term apply x x
above does look quite like the self-application in \x -> x x
, which is the `kernel' of fixed-point combinators. The self-application and hence fixed-point combinators are not expressible in the simply-typed lambda-calculus. Our calculus is certainly not simply typed.Apply
Class-parameterized classes, and the type-level logarithm
An illustration of parameterizing a type class by a type class.
The paper on ``Typing Dynamic Typing'' (Baars and Swierstra, ICFP 2002) demonstrated the first implementation and application of Leibniz equality witnesses in Haskell:
newtype EQU a b = EQU{subst:: forall c. c a -> c b}A term
eq :: EQU a b
witnesses the equality of the types a
and b
: in
any context c
, the type a
can be substituted with the type b
. The
context is represented by the type constructor c
. The witness gives
the constructive proof of substitutability: given a term of
the type c a
, we can always obtain a term of the type c b
. Since we
do not know anything about the context c
, such a substitution may
only happen if the two types are indeed equal. Hence the sole
non-bottom witness isrefl :: EQU a a refl = EQU idtestifying that equality is reflexive. Leibniz equality became quite popular since it lets us represent GADTs to a large extent. The power of the Leibniz equality comes from the freedom to choose the context
c
.
The following example illustrates that power, by concisely proving that
the equality is transitive. Here is the 1-line witness of the proof:tran :: EQU a u -> EQU u b -> EQU a b tran au ub = subst ub auWe treat the type
EQU a u
as (EQU a) u
, that is, as an application of
the `type constructor' (EQU a)
to the type u
. We then apply the
witness EQU u b
to replace the type u
with the type b
in the context
(EQU a)
, giving us the desired EQU a b
.Implementing type checkers and type inferencers in Haskell along the lines of typing dynamic typing requires the proof that two arrow types are equal if and only if their components are equal. In one direction,
eq_arr :: EQU a1 a2 -> EQU b1 b2 -> EQU (a1->b1) (a2->b2)witnesses that if the argument and the result types of two arrow types are equal, the arrow types themselves are equal. Fortunately, for this, commonly used direction, the proof is easy, after we define suitable type-level combinators
F1
and F2
to place the types being equated in the right
context:newtype F1 t b a = F1{unF1:: EQU t (a->b)} newtype F2 t a b = F2{unF2:: EQU t (a->b)} eq_arr a1a2 b1b2 = unF2 . subst b1b2 . F2 . unF1 . subst a1a2 . F1 $ reflIn the type
EQU (a1->b1) (a2->b2)
, the type `constructor'
(F1 (a1->b1) b2)
represents the context of the type a2
, and
the type constructor (F2 (a1->b1) a2)
is the context of
the type b2
. Leibniz equality only applies if the context of a type is
represented as a type constructor; therefore, we sometimes have to
define auxiliary newtypes to put the contexts in the required form.In the reverse direction, we have to prove that if two arrow types are equal, their components (e.g., the argument types) are equal as well. The proof will witness the injectivity of the arrow type constructor. It was thought that injectivity cannot be proven with Leibniz equality at all. For example, the paper ``Implementing Cut Elimination: A Case Study of Simulating Dependent Types in Haskell'' by Chen, Zhu and Xi, PADL'04, needed the reverse, elimination direction and found it impossible to obtain with Leibniz equality witnesses. We demonstrate that type families help.
Type families let us define ``subtractive contexts'', so that we can
view a type a
as the type (a->b)
placed into the context that
removes (->b)
. Again we use an auxiliary newtype to make the
subtractive context appear as a type constructor.
type family Fst a :: * type instance Fst (x->y) = x type instance Fst (x,y) = x -- etc. newtype FstA a b = FstA{unFstA :: EQU (Fst a) (Fst b)} eq_arr1 :: EQU (a1->b1) (a2->b2) -> EQU a1 a2 eq_arr1 eq = unFstA . subst eq $ ra where ra :: FstA (a1->b1) (a1->b1) ra = FstA refl
Jeremy Yallop has suggested a simple generalization that lets us write
generic injectivity witnesses, for arbitrary type constructors f
and f1
:
eq_f :: EQU (f a) (f1 b) -> EQU a b eq_f2 :: EQU (f a1 b1) (f1 a2 b2) -> EQU a1 a2These witnesses testify that Leibniz equality is indeed stronger than mere bijection.
Proving False with impredicativity, injectivity, and type case analysis
oleg-at-pobox.com or oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML