From time to time we run into the limits of polymorphism in Haskell, let alone in ML. We may need to parameterize by arbitrary type functions rather than mere 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 even in 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
followed by n other arguments, returning them as the
n-element list. It may seem that 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
for our number representation: 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
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, this 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 * char
The 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
enough 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, after all,
expressible in a Hindley-Milner system. Looking 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.Generating Code with Polymorphic let:
A Ballad of Value Restriction, Copying and Sharing
Yet another illustration of the connection, in Sec 2.1 of the paper
g that takes a selector such as the tuple selector
fst :: forall a b. (a,b) -> a
snd :: forall a b. (a,b) -> b
as an argument and applies it to several heterogeneous tuples. For
example:
g sel = (sel (1,'b'), sel (true,"four"))(We have switched to Haskell, because the higher-order version of the problem was posed on Haskell-Cafe.)
It is already a challenge to give a type to 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: 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 parameterized 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 _ = snd
To 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 snd
That 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 the 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.Apply
Haskell with only one typeclass
Another extensive example of Apply (called C in that code)
a and b are equal, then so are c a and c b where c is
an arbitrary type constructor. The proof is constructive, giving us
the substitution function that converts any term of the type c a to
the corresponding term of the type c b. The inverse direction is
called injectivity: from the equality of c a and c b obtain the
equality of a and b. For example, injectivity tells us that if two
list types [a] and [b] are equal then the types of their elements
are equal as well. Obtaining the constructive proof of injectivity
using Leibniz equality, without any compiler magic, has been
considered impossible. We now demonstrate how to do that. The key is
the realization that a type-constructor polymorphism extends to the
polymorphism over arbitrary type functions. Leibniz injectivity is
also the example of type functions seemingly more expressive than
type-class functional dependencies.
``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}
The 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 is
refl :: EQU a a
refl = EQU id
testifying 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 au
We 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 $ refl
In 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 a2
These witnesses testify that Leibniz equality is indeed stronger than
mere bijection.Proving False with impredicativity, injectivity, and type case analysis
It all started with the question asked by Spiros Eliopoulos on the caml-mailing list on On 19 October 2015, describing a simple example distilled from the problem encountered in his work on js_of_ocaml. He wanted to define a polymorphic container class with a `map'-like method -- something like the following:
class ['a] container (x:'a) =
object
val v = x
method map : 'b. ('a -> 'b) -> 'b container =
fun f -> new container (f v)
end
To be able to access fields and (private) methods of container
objects, map should be a method. It should return a new instance of
the container, with a potentially different element type, depending on
the type of the transformation function f. Alas, OCaml rejects the
definition, with a rather cryptic message that ``The universal type
variable 'b cannot be generalized: it escapes its scope.'' Can such a
container class be implemented?
A similar class with the less-polymorphic (and less useful) map method
class ['a] containerM (x:'a) =
object
val v = x
method mapM : ('a -> 'a) -> 'a containerM =
fun f -> new containerM (f v)
end
is however accepted. To understand why, it is worth writing the
['a] containerM object type in full, expanding all abbreviations:
type 'a contM = <map : ('a->'a) -> <map : ('a->'a) -> <... > > >
This is an equi-recursive type, as object types are in OCaml,
represented as the infinite tree. Crucially, it is a regular
tree: the set of its distinct subtrees is finite (to be precise, the distinct
subtrees are: 'a, 'a->'a, map: ('a->'a) -> 'a contM, and 'a contM).
In contrast, the object type of the original ['a] container has
an infinite number of distinct subtrees: one for each instantiation of
the type variable 'b. For the sake of type checking, object
(and polymorphic variant) types in OCaml must be regular.
In more detail, the regularity requirement was explained in the
message by Jeremy Yallop, posted in response to Spiros Eliopoulos.
Thus, strictly speaking, the desired polymorphic container class with the polymorphic map method cannot be defined. That is where Category Theory comes in -- at least, that is how it how it came to my mind and lead to the solution.
Let us consider a closely related problem: defining a polymorphic map function over a collection that is not really polymorphic, like Bigarrays in OCaml (we show one-dimensional arrays for simplicity):
open Stdlib.Bigarray
type ('a,'elt) arr = ('a, 'elt, c_layout) Array1.t
Although it looks like the type variable 'a
can be instantiated to any type, in
reality big arrays may contain only integer and floating-point
numbers. Thus the unrestricted polymorphic map-like function
amap: ('a -> 'b) -> ('a,'elt) arr -> ('b,'elt) arr
is not possible. Luckily, left Kan extension (along the identity)
tells us how to overcome the restriction: rather than actually
performing the mapping, just collect its arguments and declare the
operation done.
Here is the realization of the idea:
type 'b karr = KanArr : ('a,'elt) arr * ('a -> 'b) -> 'b karr
The data type 'b karr collects the arguments
of a mapping operation: the array arr and
the transformation function f.
The parameters 'a and 'elt are existentially quantified. Any
(one-dimensional) big array ('a,'elt) arr
can be converted to 'a karr, as illustrated below:
let ar1 : (int,int_elt) arr = Array1.of_array Int c_layout [|1;2;3;4;5|]
val ar1 : (int, int_elt) arr = <abstr>
let kar1 = KanArr (ar1,fun x->x);;
val kar1 : int karr = KanArr (<abstr>, <fun>)
(The indented lines below the definitions show the responses of the
OCaml top-level.) The data type 'a karr permits the
fully polymorphic map without any restrictions:
let kmap : ('a -> 'b) -> 'a karr -> 'b karr = fun f (KanArr (ar,g)) ->
KanArr (ar, fun x -> f (g x))
to be used as
let kar2 = kmap string_of_int kar1;;
val kar2 : string karr = KanArr (<abstr>, <fun>)
This is just a pretense: although kmap string_of_int creates string karr it certainly does not create (string,int) arr; the latter is
just impossible. It may not matter however: if all we want in the end
is, say, to reduce the arr, we can do the left folding just as well
on karr instead:
let kfold : ('b -> 'a -> 'b) -> 'b -> 'a karr -> 'b = fun f z (KanArr (ar,g)) ->
let sum = ref z in
for i=0 to Array1.dim ar -1 do
sum := f !sum (g ar.{i})
done;
!sum
kfold (^) "" kar2;;
- : string = "12345"
The lesson carries over to the original container problem. The map method does not have to actually create a new container instance. It could pretend: that is, merely collect all data needed to create the instance. Here is the whole solution:
type 'a cont_proxy = P of 'a
class ['a] container (x:'a) =
object
val v = x
method map' : 'b. ('a -> 'b) -> 'b cont_proxy =
fun f -> P (f v)
method get : 'a = v
end
We added the accessor get for the sake of examples.
The data type cont_proxy is defined
to hold the arguments to the container constructor (on our case, a
single value). The method map' does not actually construct anything; it
merely returns the data needed for the construction.
As a method, map' has access to fields and (private) methods
of container objects. When all data needed to build a container
instance is at hand, constructing the instance is trivial, and can be
done by an external function:
let map : ('a -> 'b) -> ('a container -> 'b container) = fun f c ->
match c#map' f with P x -> new container x
Here are the tests (the responses of the OCaml top-level are shown
under each test, indented).
let c = new container 3;;
val c : int container = <obj>
let _ = c#get;;
- : int = 3
let c' = map string_of_int c;;
val c' : string container = <obj>
let _ = c'#get;;
- : string = "3"
As Jacques Garrigue said on the mailing list:
``The externalizing solution has been known since the beginning of
OCaml, but it is nice to know that it has such a cute name.''
read :: Read a => String -> a
fromInteger :: Num a => Integer -> a
are 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 foo and bar. Writing signatures
for top-level functions is overall a good habit. If 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 the single baz to be used as:
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 baz must therefore be parameterized by a type class.
This 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 -> b
The 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 _ = fromInteger
The type LRead indeed relates to the type class constraint
Read while LFromInt relates to Num.
We are done. The function baz is simply
baz 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.
We have thus attained a seemingly high-ranking polymorphism,
using only rank-1 types, which are all inferrable.
We do 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 x
The 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 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 very
instance being defined. We introduce
omega () = apply Delta Deltawhose inferred type
*Main> :t omega
omega :: () -> b
leaves 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