previous  next  contents  top

Advanced Polymorphism in Simpler-Typed Languages

 

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.


 

Warm-up: polyvariadic functions

As a warm-up, we show the trivial OCaml code for the problem that may at first blush appear unsolvable within the Hindley-Milner system. The problem is to write a function that first takes the numeral 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']
Version
The current version is September 2008.
References
The problem is a variation of functional unparsing. It is solved using the general approach well explained in
Olivier Danvy: Functional Unparsing. J. Functional Programming, 1998, v8, N6, pp. 621-625

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.

 

Polymorphic selection

Selection from heterogeneous structures such as nested tuples seems to require parameterization of a term by a type function that is not a type constructor. We have run into such selection problems on several occasions; last time, when designing typed printf and scanf sharing the same formatting specification. The problem turns out solvable with mere Hindley-Milner polymorphism, after we exploit the deep connection between polymorphism and inlining.

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"));;
       This expression has type bool * string but is 
       here used with type int * char
The first problem is indicated in the error message. In the 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 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 sufficient to write f2. It seems we need abstraction not over types but over arbitrary type functions of the kind * -> * -> *.

It turns out selection from heterogeneous tuples is expressible in the Hindley-Milner system.

     let f3 sel = sel ((fun () -> (fst (1,'b'), fst (true,"four"))),
                       (fun () -> (snd (1,'b'), snd (true,"four"))));;
       val f3 : ((unit -> int * bool) * (unit -> char * string) -> 'a) -> 'a = <fun>
     
     f3 (fun (a,b) -> a ());;
       - : int * bool = (1, true)
     
     f3 (fun (a,b) -> b ());;
       - : char * string = ('b', "four")
We compute the possible selections, by essentially inlining the selectors fst and snd. We use thunks to delay the selection computation until we need its result.
Version
The current version is July 18, 2008.
References
Interpreting types as abstract values
The second part of these lecture notes expounds the deep relation between parametric polymorphism and `inlining'.

 

Higher-order polymorphic selection

This is the higher-order version of selection from heterogeneous structures. Above we have seen how to define a function f3 receiving a heterogeneous tuple selector such as fst or snd as its argument. We now turn to passing the functions like f3 as arguments to other functions. 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"))
The examples t1 through t3 type check in Haskell98; t4 and t5 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 above 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.

We first demonstrate a complex solution that sort of works. We then change the point of view, and the problem becomes elementary. 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)
we replace the functions like fst and snd with their `encodings' Fst and Snd, 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 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 side-step the issue of too complex a 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. We define 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 we have to complicate our encoding further still.

Let us pause however. We have only two selectors, fst and snd. Therefore, the caller of fs, rather than passing a function g accepting a selector, can pass the results of the application of g to fst and to snd. Now fs will receive a pair of the results (g fst, g snd). Thanks to non-strict evaluation of Haskell, the results are not actually computed unless needed. We arrive at the following solution:

     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)
This code type checks in Haskell98, or any Hindley-Milner system.
Version
The current version is 1.2, October 2009.
References
Type-class overloaded functions: second-order typeclass programming with backtracking
More extensive example of using the interpreter Apply

Haskell with only one typeclass
Another extensive example of Apply (called C in that code)



Last updated November 1, 2009

This site's top page is http://pobox.com/~oleg/ftp/

oleg-at-pobox.com or oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!

Converted from HSXML by HSXML->HTML