Type Inference for Polytypic Functions

Johan Jeuring and Patrik Jansson

Chalmers University of Technology and University of Göteborg

S-412 96 Göteborg, Sweden

         e-mail : {johanj,patrikj}@cs.chalmers.se

Abstract

A polytypic function is a function that is defined by induction on the structure of user-defined datatypes. Examples of polytypic functions are the functions map and length, which can be defined on lists and on different kinds of trees. Larger examples are Yacc, term rewriting systems, program transformation systems, theorem provers, proof editors, etc. We develop a type system that facilitates writing polytypic functions. The type inference algorithm is sound and complete, and very similar to the Hindley/Milner type inference algorithm. Furthermore, we extend Core-ML with a polytypic construct, which allows users to define polytypic functions. The polytypic construct is a generalisation of Haskell’s deriving construct, since a programmer can now extend the set of functions that can be derived.

1 Introduction

1.1 Polytypic functions

Haskell’s [8] type system infers types for both parametric polymorphic functions and ad-hoc polymorphic functions. For example, the parametric polymorphic function length, which returns the length of a list with values of any type, receives the type [a] -> Int, and the ad-hoc polymorphic operator (+) receives the type Float -> Float -> Float whenever it is used on floating point numbers, and Int -> Int -> Int whenever it is used on integers.

There exists a third kind of polymorphism besides parametric polymorphism and ad-hoc polymorphism. Although function length can count the elements of a list with values of any datatype, it cannot count the nodes of a tree. Instead new (and very similar) functions have to be written to count the nodes of each new datatype. Polytypism lets us write a general length function for any regular datatype.^{1} The generalised version of function length is called a polytypic function. Another example of a polytypic function is the familiar map function. The map function takes a function f :: a -> b and a list x :: [a] and applies f to all elements in x, obtaining a list of type [b]. A similar function can be defined on binary trees: the map function on binary trees takes a function f :: a -> b and a binary tree t :: Tree a, and applies function f to all elements of t, obtaining a tree of type Tree b. Function map can be defined on all regular datatypes.

1A datatype D is regular if it contains no function spaces, and if the arguments of the

More examples of polytypic functions can be found in software products, programming languages, and programming methodologies. For example, Yacc takes a grammar (a grammar can be viewed as a datatype), and returns a parser for that grammar. Haskell’s deriving construct takes a datatype and a class name, and returns definitions for the functions specified in the class. For example, writing deriving Text after a datatype gives amongst others a function that takes a value of the datatype and returns a string representing the value. The deriving construct supports five other classes. Caml Light’s [22] generic comparison functions generate code for equality, less than, etc. for a regular datatype (the generic comparison functions are a slight extension of Haskell’s Eq class). LP, the Larch Prover, generates amongst others induction rules for datatypes.

Polytypic functions are standard in the Squiggol community, see [23, 25, 26, 28], where the ‘Theory of Lists’ [3, 4, 16] is extended to datatypes that can be defined by means of a regular functor. The category theory needed for this extension has been developed by Manes and Arbib [24] and Hagino [10]. The polytypic functions used in Squiggol are general recursive functions such as catamorphisms (generalised folds), paramorphisms, maps, etc. Sheard [37], and Böhm and Berarducci [5] give programs that automatically synthesise these functions. Special purpose polytypic functions such as the generalised version of function length and the operator (==) can be found in [25, 32, 33, 2, 36, 17, 18, 14]. These are only a few examples of polytypic functions appearing in software products, programming languages, and programming methodologies.

In Haskell or any other software product or programming language we can use a limited amount of polytypic functions. However, we want to be able to write polytypic functions in Haskell itself. This paper discusses how the type system of a language like ML or Haskell can be extended to facilitate writing polytypic functions.

1.2 Type systems

Implementing the polytypic pattern matching function [18] and the polytypic unification function [14] was a cumbersome process, and led to a strong desire for a type system that facilitates writing polytypic functions. Polytypic functions cannot be written using parametric polymorphism or ad-hoc polymorphism. A polytypic function depends on the structure of a datatype, so its type should contain a variable that ranges over type structures. Instantiations of polytypic functions on different datatypes are related but different functions. It follows that the type of a polytypic function cannot be given by means of a parametric polymorphic type variable. On the other hand, a polytypic function depends only on the structure of a datatype, so instantiations on different datatypes only differ in their structure, whereas definitions of an ad-hoc polymorphic function, such as the operator (+) :: Num a => a -> a -> a, on different datatypes may be completely unrelated.

recursive calls of the datatype at the right-hand side of the definition are the same as the arguments of the datatype on the left-hand side. The collection of regular datatypes contains datatypes such as Int, List a, different kinds of trees, and mutual recursive types. A regular datatype can be modelled as an initial fixed point in a category of functor-algebras.

We would like to be able to implement polytypic functions directly in a strongly typed programming language. One could use dynamic types [1], or compile-time reflection [13] to implement polytypic functions, but then definitions of polytypic functions cannot be typechecked, which may result in run-time type errors.

In [7], Dubois et al. propose an extension of the ML-type system that allows writing functions by pattern matching on types. The main difference with normal ML typing is the presence of dynamic type variables, which may be instantiated to normal types during type inference. Using this type system, the operator (==) is defined on all basic types, and on the type of lists of arbitrary depth. However, the type system cannot be used to define (==), or any other function, on user-defined types. So functions length and map discussed above cannot be written in the extended ML-type system. Harper and Morrisett [12] describe a type system that is very similar to the type system of Dubois et al. However, it does not give users the possibility to define functions by pattern matching on types.

In [19, 20], Jones proposes a type system for higher-order polymorphism. Using higher-order polymorphism, functions can be generalised with respect to type constructors. For example, it is possible to define a function size of type

size :: ∀c a . c a → Int

where c is a constructor variable. We might expect that length would be an instance of function size, substituting the list type constructor for the variable c. However, to quote Jones [20], by itself, higher-order polymorphism is often too general for practical examples. For example, in the case of function size, it is hard to construct a definition for any interesting functions of type ∀c a . c a → Int because we need a definition that will work for any type constructor c, and any type a. So again, we cannot write the generalised versions of functions length and map using higher-order polymorphism. The combination of higherorder polymorphism with overloading in constructor classes gives possibilities for writing polytypic functions [29, 20]. For this purpose a type has to be defined by describing its recursive structure, and the recursive structure has to be declared an instance of the class Functor. If a type has been defined thus, one can define functions fold, map and size on the datatype. However, defining a polytypic function this way is a rather lengthy and cumbersome process. Furthermore, the datatypes for which folds can be generated are the datatypes with precisely one argument, for a datatype with another number of arguments, all instance declarations have to be repeated. We will define a polytypic construct with which polytypic functions can be written and typechecked. Polytypic functions thus defined are translated into overloaded higher-order polymorphic functions.

1.3 A type system for polytypic functions

This paper proposes to extend languages with Hindley/Milner typing with a polytypic construct, that allows the programmer to write polytypic functions. The type system is based on the categorical approach to modelling datatypes as initial objects in categories of functor-algebras. This means that we view a user-defined regular datatype D a as a type of the form Mu F a, where F is a functor that describes the structure of the type. A polytypic function is defined by induction on the structure of datatypes, i.e., by induction on functors. So instead of dynamic variables or constructor variables we use functor variables to define polytypic functions. For example, if the polytypic version of function length is called size, we define

   polytypic  size :: Mu F a -> Int  where
     ...

where F is a functor variable, and where the dots should be replaced by the definition (by induction on functor F) of the polytypic function size.

The polytypic construct serves several purposes. Firstly, it is a natural generalisation of Haskell’s rather ad-hoc deriving construct. The functions derived by Haskell can be defined with the polytypic construct. Secondly, we can define general versions of basic functions such as foldr, map, zip, etc. Using these and many more functions, we can subsequently write for example a polytypic term rewriting system in Haskell. As a small example, assume that the polytypic function size has been defined. If one writes the declaration

   data Tree a  =  Leaf a | Bin (Tree a) (Tree a)

one can use the function

   size :: Tree a -> Int

which counts the number of elements in a tree, in the remaining part of the program.

How do we extend a language with a Hindley/Milner typing system with the polytypic construct? We start with extending the language of Core-ML [31] with expression pairs, left and right injection into a sum, and the polytypic construct. We extend the type system in such a way that an expression cannot only have a regular type, but also a functor type. The grammar for the type language of Core-ML is extended with four extra productions: two productions for pairs and sums, a production ϕ τ τ for functor types (τ is the start-symbol for types, ϕ is the start-symbol for functors), and a production Mu ϕ τ for userdefined datatypes. For example, function size will have the following type.

size :: ∀f a . Mu f a → Int

where f is a functor variable. Given a program, we want to assign types to all expressions. We split the programs into data declarations and other expressions. Using the data declarations, we build an initial environment Γ consisting of the type assignments to the constructors appearing in the data declarations. Furthermore, the initial environment contains two functions, called in and out [23], that construct and destruct values of user-defined datatypes, respectively.

in : ∀f a . f a (Mu f a) → Mu f a
out : ∀f a . Mu f a → f a (Mu f a)

We show that most general types can still be inferred. The proof of this fact is an extension of the proof of the main results of Damas and Milner [30, 6]. Finally, we give a translation of programs with the polytypic construct to programs in Gofer with constructor classes.

1.4 Related work

At FPCA ’95 we found that there exists at least three other independent attempts to develop a type system for polytypic functions.

Ruehr [34, 35] uses type-pattern abstraction to define polytypic functions. A language with type-pattern abstraction is more expressive than our language, at the cost of possibly ambiguous typings. Thus, a language with type-pattern abstraction does not admit principal types, and furthermore, inferring types for type-pattern abstractions is undecidable. Since we do not seem to need the additional power of a language with type-pattern abstraction, we prefer to have a language with principal types and decidable type inference. However, the precise relation between a language with type-pattern abstraction and our language is not completely clear to us.

Jay [15] develops a type system rather similar to ours. Instead of types and functors he uses types and so-called forms. A language with this type system has the same expressive power as our language, but it seems more difficult to define new polytypic functions, such as polytypic zip, in Jay’s language. Furthermore, mutual recursion and multiple variable datatypes seem to be more problematic than in our approach.

Sheard [38] develops a type system using existential types. Polytypic functions are defined only as catamorphisms. This gives nice definitions of polytypic functions, but it limits the expressive power of the language. It is likely that this is not a severe restriction, but we do not know. Sometimes, writing polytypic functions as catamorphisms has a slight disadvantage: functions like zip and equality have to be defined as higher-order catamorphisms, whereas their ‘natural’ definition is a first-order inductive definition. Since we do not have a paper describing Sheard’s type system, it is hard to give a fair comparison between his type system and ours.

Since the development of some of the above type systems is in a very preliminary stage it is hard to compare the systems. However, we do think that our system is simpler than the above systems, due to its similarity to Hindley/Milner. Furthermore, our system is expressive enough for writing the desired polytypic functions. Finally, although we have not worked out the details, we see no serious problems in dealing with multiple variable datatypes and mutual recursive datatypes, due to the freedom the translation scheme gives us.

1.5 Organisation

This paper is organised as follows. Section 2 shows some example definitions of polytypic functions. Section 3 introduces the Core-ML language extended with constructor expressions, pairs and sums, and introduces the type language. Section 4 discusses the type inference rules for the language, the unification algorithms needed in the type inference algorithm, and the type inference algorithm itself for this language. Section 5 extends the language and the type inference rules with the polytypic construct, and adjusts the type inference algorithm to the extended language. Section 6 describes the semantics of the language with the extended type system: it translates the extended ML language to Gofer with constructor classes. Section 7 concludes the paper.

2 Polytypic functions

In this section we define the polytypic function map, which generalises function map :: (a -> b) -> [a] -> [b], and the polytypic function size, which generalises the length function. We first discuss the relation between datatypes and functors, and we introduce the functions map and size, together with some other auxiliary functions, on some example datatypes.

2.1 Datatypes and functors

The datatype List

Consider the datatype List defined by

   data List a  =  Nil | Snoc (List a) a

Values of this datatype are built by appending instead of prepending values of type a to a list. This datatype can be viewed as the fixed point with respect to the second argument of the datatype FList defined by

   data FList a x =  FNil | FSnoc x a

The datatype FList describes the structure of the datatype List. Since we are only interested in the structure of List, the names of the constructors of FList are not important. FList is a category theoretical functor. We define FList using a more conventional notation by removing the constructors (writing () for the empty space we obtain by removing FNil, where () is the unit type containing one element denoted by ()), and replacing | with +, and juxtaposition with ×.

FList a x = () + x × a

We now abstract from the arguments a and x. Function Par (for parameter) returns the parameter a, and function Rec returns the recursive parameter x. Con is the constant functor. Operators + and × are lifted to the function level.

FList = Con () + Rec × Par

The initial object in the category of FList a-algebras (the fixed point of FList), denoted by Mu FList a, models the datatype List a. The initial object consists of two parts: the datatype Mu FList a, and a function in that corresponds to the constructors of the datatype List a.

in :: FList a (Mu FList a) → Mu FList a
in (inl ()) = Nil
in (inr (xs, x)) = Snoc xs x

For example, the list value Snoc (Snoc Nil 2) 1 is represented by the value in (inr (in (inr (in (inl ()), 2)), 1)). An equivalent definition of function in reads

in = const Nil ‘junc‘ uncurry Snoc

where operator ‘junc‘ takes a function f of type a → c and a function g of type b → c, and applies f to left-tagged values, and g to right-tagged values, throwing away the tag information. Function in constructs values of type Mu FList a, and function out destructs values of type Mu FList a. Function out is the inverse of function in.

out :: Mu FList a → FList a (Mu FList a)
out Nil = inl ()
out (Snoc xs x) = inr (xs, x)

In category theory, a functor is a function between categories that preserves the algebraic structure of the category. Since a category consists of objects (types) and arrows (functions), a functor consists of two parts: a definition on types, and a definition on functions. FList takes two types and returns a type. The part of the functor that takes two functions and returns a function is called fmap.

fmap :: (a → c) → (b → d) → FList a b → FList c d
fmap f g = id + g × f

The operators × and + are the ‘fmaps’ on products and sums, respectively.

(×) :: (a → c) → (b → d) → (a, b) → (c, d)
(f × g) (x, y) = (f x, g y)
(+) :: (a → c) → (b → d) → a + b → c + d
(f + g) (inl x) = inl (f x)
(f + g) (inr y) = inr (g y)

Function fmap is used in the definition of cata (we use the name cata for generalised folds) on List. Function cata is defined as foldl in Haskell.

cata :: (FList a b → b) → Mu FList a → b
cata f = f · fmap id (cata f) · out

Here we have used function out to avoid a definition of cata by pattern matching. Function fmap applies cata f recursively to the constituents of the argument.

Finally, we use function cata to define functions size (function length in Haskell) and mapp (we use the name mapp for generalised maps) on the datatype Mu FList a.

size :: Mu FList a → Int
size = cata (const 0 ‘junc‘ \(n, x) → n + 1)
mapp :: (a → b) → Mu FList a → Mu FList b
mapp f = cata (const Nil ‘junc‘ \(xs, x) → Snoc xs (f x))

An equivalent definition of function mapp, in which we avoid naming arguments, reads as follows.

mapp f = cata (in · fmap f id)

The type constructor List (= Mu FList) and the function mapp form a functor, just as FList and fmap form a functor.

The datatype Tree

The datatype Tree is defined by

   data Tree a  =  Leaf a | Bin (Tree a) (Tree a)

Applying the same procedure as for the datatype List, we obtain the following functor for the datatype Tree.

FTree = Par + Rec × Rec

Functions in and out are defined as follows on this datatype.

in :: FTree a (Mu FTree a) → Mu FTree a
in = Leaf ‘junc‘ uncurry Bin
out :: Mu FTree a → FTree a (Mu FTree a)
out (Leaf x) = inl x
out (Bin l r) = inr (l, r)

Function cata on Mu FTree is defined in terms of functions out and fmap.

fmap :: (a → c) → (b → d) → FTree a b → FTree c d
fmap (f, g) = f + g × g
cata :: (FTree a b → b) → Mu FTree a → b
cata f = f · fmap id (cata f) · out

Note that the definition of cata on the datatype Tree is exactly the same as the definition of cata on the datatype List. Functions size and mapp are defined by

size :: Mu FTree a → Int
size = cata (const 1 ‘junc‘ uncurry (+))
mapp :: (a → b) → Mu FTree a → Mu FTree b
mapp f = cata (in · fmap f id)

Functors for datatypes

We have given functors that describe the structure of the datatypes List and Tree. We have that for each regular datatype there exists a (bi)functor F such that the datatype is the initial algebra in the category of F a-algebras [23]. A functor is a value generated by the following grammar.

F ::= F :+: F | F :×: F | Mu F :@: F | Con τ | Rec | Par

where τ in Con τ is a type. The alternative Mu F :@: F in this grammar is used to describe the structure of types that are defined in terms of other userdefined types. Note that functors generated by this grammar can only represent datatypes with one type variable; to represent datatypes with another number of type variables we have to adjust the Par case. A polytypic function is either defined by induction on functors, or in terms of other polytypic functions.

2.2 Generalising functions mapp and size

Generalising function mapp

We want to define a polytypic function mapp that takes a function f and a value x of type D a, and applies function f to all occurrences of values of type a in x, giving a value of type D b.

For each regular user-defined datatype D a we assume the existence of a functor F such that D a = Mu F a, and we assume the existence of functions in and out of type

   in   ::  F a (Mu F a) -> Mu F a
   out  ::  Mu F a -> F a (Mu F a)

These functions are automatically constructed for each user-defined datatype in the program. Function fmap, the functional part of the functor describing the structure of datatype D, is a basic function that is used in many definitions of polytypic functions. It is defined by induction to the structure of functors.

   polytypic fmap :: (a -> c) -> (b -> d) -> F a b -> F c d where
     fmap = \f g -> case F of
                      F :+: G     ->  fmap f g -+- fmap f g
                      F :*: G     ->  fmap f g -*- fmap f g
                      Mu F :@: G  ->  mapp (fmap f g)
                      Con x       ->  id
                      Rec         ->  g
                      Par         ->  f

A definition of a polytypic function starts with the keyword polytypic, followed by the name of the function and its type. Names starting with capitals in the type declaration and not defined as a datatype elsewhere in the program are assumed to be functor variables. So the F in the above type declaration is a functor variable. The type declaration and the inductive definition of the function are separated by the keyword where. The inductive definition defines fmap for all functors. The operator -+- implements +, and -*- implements ×. Note that in the Mu F :@: G case, fmap is defined in terms of function mapp on Mu F; fmap and mapp are mutually recursive for types defined in terms of other user-defined types.

Using functions fmap and out, we can define the polytypic function cata by

   polytypic cata :: (F a b -> b) -> Mu F a -> b where
     cata = \f -> f . fmap id (cata f) . out

We use functions fmap, cata and in to define mapp.

   polytypic mapp :: (a -> b) -> Mu F a -> Mu F b where
     mapp = \f -> cata (in . fmap f id)

Generalising function size

We want to define a polytypic function size that for a value x of datatype D a counts the number of occurrences of values of type a in x. The polytypic function size is defined in terms of function cata.

   polytypic size :: Mu F a -> Int
     where size = cata size2
   polytypic size2 :: F a Int -> Int where
     size2 = case F of
               F :+: G     ->  size2 `junc` size2
               F :*: G     ->  \(x,y) -> size2 x + size2 y
               Mu F :@: G  ->  \x -> sum (map size2 x)
               Con x       ->  \x -> 0
               Rec         ->  \x -> x
               Par         ->  \x -> 1

The definition of function size2 requires the existence of a polytypic function sum, which sums the integers in a value of an arbitrary datatype. The definition of sum is very similar to size, and therefore omitted.

Generalising function (==)

The equality function (==) is a polytypic function too. It can be defined as follows on a datatype Mu F a. Suppose that we have the following polytypic functions:

   polytypic zip :: Mu F a -> Mu F b -> Maybe (Mu F (a,b))
   polytypic flatten :: Mu F a -> [a]

Function zip zips two values of datatype Mu F a, returning a value of the form Just x if the values have the same shape, and returning Nothing otherwise.

Function flatten flattens a value of type Mu F a to a value of type [a]. The precise definitions of zip and flatten are omitted. Function (==) is now defined by:

   polytypic (==) :: Eq a => Mu F a -> Mu F a -> Bool where
     (==) = \x y -> case  zip x y  of
                      Nothing  ->  False
                      Just z   ->  all (uncurry (==)) (flatten z)

3 The language

A program is a list of declarations followed by an expression. An expression is a Core-ML expression [31], a pair of expressions or the left or right injection into a sum. Programs and expressions are values generated by the following grammars.

P ::= E | DP
E ::= x | λx.E | EE | let x = E in E | (E, E) | inl E | inr E

D generates datatype declarations. The definition of D is straightforward and omitted. A type is a value generated by the following grammar.

τ ::= t  type variable
| T τ ... τ type constructor with all its arguments
| ϕ τ τ  functor type
| Mu ϕ τ type with structure ϕ
T ::= → | (,) | + | C

For readability we will write the function type, pair type and sum type constructors in their normal infix notation (τ → τ, (τ, τ) and τ + τ respectively). C ranges over other pre- and user-defined type constructors including nullary constructors denoting base types such as Int, Bool, etc. A (bi)functor is a value generated by the following grammar.

ϕ ::= f  functor variable
| ϕ :+: ϕ  sum functor
| ϕ :∗: ϕ  product functor
| Mu ϕ :@: ϕ functor composition
| Con τ  constant functor
| Rec  second component
| Par  first component

Type schemes are generated by the following grammar.

σ ::= ∀f_{i} t_{i}.τ

where f_{i} and t_{i} range over finite sets of functor variables and finite sets of type variables, respectively. In this language we can use polytypic functions but to define new polytypic functions we need the polytypic construct defined in section 5.

We define a function teval that transforms types with functor expressions to types without functor expressions, except possibly for functor variables. Function teval is defined by induction on the mutually recursive structures of types and functors. It is defined using function feval, which transforms functor expressions to type expressions containing no other functor expressions than functor variables.

teval :: type → type
teval (T τ_{1}...τ_{n}) = T (teval τ_{1}) … (teval τ_{n})
teval (ϕ τ τ′) = feval ϕ (teval (τ, τ′))
teval (Mu ϕ τ) = Mu ϕ (teval τ)
teval t = t
feval :: functor → type → type
feval (F :+: G) τ = feval F τ + feval G τ
feval (F :×: G) τ = (feval F τ, feval G τ)
feval (Mu F :@: G) τ = feval (Mu F) (feval G τ)
feval (Con x) τ = teval x
feval Rec (τ, τ′) = τ′
feval Par (τ, τ′) = τ
feval ϕ (τ, τ′) = ϕ τ τ′

Note that teval is a cata on the datatype of types and feval is a cata on the datatype of functors. Composed with a substitution of all functor variables to functors without variables, teval gives the semantics of the functor types in terms of normal types extended with the Mu F construct.

4 Type inference

4.1 Type inference rules

We divide the typing rules for our language in two parts. The first part is Damas-Milner’s type system [6] and the second part consists of rules for pairs and sums. These rules are omitted. A type scheme σ = ∀f_{i} t_{i} . τ is more general than σ′ = ∀g_{i} s_{i} . τ′ (written σ ≥ σ′) iff no free variable in σ is bound in σ′ and τ′ = Sτ where S only changes variables bound in σ.

For each regular datatype declaration generated by D a functor F such that D a = Mu F a is generated. Whenever a polytypic function is applied to a value v of datatype D a, v is translated to a value of type Mu F a. This means that we have functions that translate values of type D a into values of type Mu F a, and vice versa. The initial environment contains the functions in and out of type:

in : ∀f t . f t (Mu f t) → Mu f t
out : ∀f t . Mu f t → f t (Mu f t)

4.2 Unification

In the type inference algorithm in the following section we use algorithm mgu to compute the most general unifier of two types. Since our type language differs substantially from the well known type languages, we describe the unification algorithm here.

A substitution is an assignment that maps functor variables to functors, and type variables to types. A unifier of two types τ and τ′ is a substitution S such that S(τ) = S(τ′). The most general unifier of two types τ and τ′ is a substitution that factors any other unifier.

Function mgu returns the most general unifier of two type expressions. The algorithm is the usual unification algorithm that matches variables with any expressions but constructors only with themselves. The only extension is that in types containing functors the corresponding functors are unified with mguf, which returns the most general unifier of two functor expressions.^{2} This means that even though we are using functors we do not need higher order unification.

Theorem. Function mgu returns the most general unifier of two type expressions, and function mguf returns the most general unifier of two functor expressions.

4.3 A type inference algorithm

To assign types to all expressions in a program we first traverse the list of datatype declarations. Using the datatype declarations, we build an initial environment Γ consisting of type assignments to the constructors appearing in the datatype declarations, and to the functions in and out . Using this initial environment, we infer the types of the other expressions.

Let e be an expression, and Γ be a typing environment. We define an algorithm W such that W (Γ, e) = (S, τ), where τ equals the type inferred for expression e, and S is a substitution. Algorithm W is very similar to Damas and Milner’s algorithm W, and omitted.

2The algorithm for computing the most general unifier is in itself an example of a polytypic function. The algorithm has the same structure on each datatype on which it is used, see [14].

(POLY)

Γ′ = Γ, x : ∀_{{}}(τ)
Γ′ ⊢ e_{i} : teval {f ↦ f_{i}}τ
Γ′ ⊢ e : τ′

                        Γ ⊢ polytypic x : τ where case f of {f_{i} → e_{i}} in e : τ′

Figure 1: Type inference rule for the polytypic construct

Theorem. Algorithm W is sound and complete with respect to the typing rules, and infers the most general type of an expression.

5 The polytypic construct

To be able to define new polytypic functions we extend the expression language with the polytypic construct.

E ::= ...

                        | polytypic x : τ where
                             case f of {F → E}
                           in E

where f ranges over functor variables. This construct defines the explicitly typed polytypic value x to be used within E just as the let-construct defines normal polymorphic values. The value x is explicitly typed because type inference from the types of the cases to the type of the whole construct in general is undecidable. We can still infer types for other expressions involving polytypic values. The type inference rule for the polytypic construct is given in figure 1. The main point here is that the expressions in the branches of the case must have the types calculated by teval. As an example we can take the case F :*: G in the definition of size2.

   polytypic size2 :: F a Int -> Int where
     size2 = case F of
               F :*: G     ->  \(x,y) -> size2 x + size2 y
               ...

The type of the expression to the right in the case is (F a Int , G a Int) -> Int and not (F :*: G) a Int -> Int which we would get by substituting F

:*: G for F in F a Int -> Int.

We now extend algorithm W such that it can also deal with polytypic functions. The new case is given in figure 2 where we use the notation S(Γ) ⊢ e : τ

[POLY] \frac{Γ′ = Γ, x : ∀_{\{\}}(τ) S_{i}(T_{i−1}Γ′) ⊢ e_{i} : τ_{i} ∀_{T_{n}Γ′}(S_{n}...S_{i+1}τ_{i}) ≥ teval \{f ↦ f_{i}\}τ T_{0} = \{\}, T_{i} = S_{i}T_{i−1} T (T_{n}Γ′) ⊢ e : τ′}{T T_{n}(Γ) ⊢ polytypic x : τ where case f of \{f_{i} → e_{i}\} in e : τ′}

Figure 2: The new case in algorithm W

to denote that W succeeds on the input (Γ, e) giving the result (S, t). In algorithm W we use the functions ∀_{Γ} and mgu. The expression ∀_{Γ}(σ) denotes the generalisation of σ with respect to Γ, defined as ∀f_{i} t_{i}.σ, where {f_{i}} ({t_{i}}) is the set of functor variables (type variables) that occur free in σ but not free in Γ. The extended type inference algorithm is still sound and complete.

6 Translation

This section describes the semantics of the polytypic construct by translating programs containing the polytypic constructs into programs without the polytypic construct.

We translate programs containing polytypic declarations to programs without polytypic declarations, but with class declarations. The class declarations can subsequently be removed by a dictionary passing transform, see amongst others Hall et al. [11], to obtain a program without polytypic or class declarations. An alternative way to translate our programs would be to use a direct dictionary passing transform.

Each polytypic declaration is translated to a class declaration. For example, polytypic cata is translated into:

   class Fmap f => Cata f where
     cata  :: (f a b -> b) -> Mu f a -> b
     cata  =  \h -> h . fmap id (cata h) . out

The definition of the datatype Mu can be found in [20]. The translation of a polytypic declaration that uses induction on the structure of functors is a bit more complicated. For example, fmap is translated as follows:

   class Mapp f => Fmap f where
     fmap  ::  (a -> c) -> (b -> d) -> f a b -> f c d

and each case in the case expression is translated into a separate instance declaration. The second case is translated thus:

   instance (Fmap f, Fmap g) => Fmap (Prod f g) where
     fmap  =  \f -> \g -> \x ->
                enProd ((fmap f g -*- fmap f g) (deProd x))

where function deProd takes an element of a product functor type, and returns a pair, and enProd takes a pair, and returns an element of a product functor type. Prod is the datatype of product functors. The definition of fmap in the different cases is obtained by applying a combinator that takes the type of fmap, the encoding and decoding functions for a functor type, and an expression, and inserts the decoding and encoding functions in the right place in the expression. The definition of this combinator is by induction on types, and omitted.

Finally, as mentioned in Section 4, a value of a user-defined datatype D a with D a = Mu F a for some functor F, is interpreted as a value of datatype Mu F a whenever a polytypic function is applied to it. It follows that we have to translate values of type D a to values of type Mu F a in applications of a polytypic function to a value of type D a. This boxing/unboxing translation is a simple inductive function over explicitly typed expressions, very similar to the translation given in Leroy [21].

7 Conclusions and future work

We have extended Core-ML with the polytypic construct, which can be used to define functions by induction over the structure of user-defined datatypes, and we have given a sound and complete type inference algorithm for extended Core-ML.

The need for a type inference algorithm for a language with polytypic functions arose from practical considerations: we found it very hard to write polytypic functions without a type inference algorithm. The polytypic construct defined in this paper can be used to define many useful polytypic functions, but we have yet to write larger applications, such as a term rewriting system, using our extended language. We implemented the type inference algorithm, but it has yet to be incorporated in a Gofer (Haskell) compiler. We are working on both extending Gofer, and writing a rewriting system, and hope to complete these programs soon.

The polytypic construct as introduced in this paper allows us to define a large collection of polytypic functions on a large collection of datatypes, but there are some restrictions. Firstly, the collection of user-defined datatypes for which we can construct instances of polytypic functions is the collection of regular datatypes. This class can be extended in some ways [9, 27], but the precise limits are not clear. Secondly, the user-defined datatypes on which polytypic functions are defined must have exactly one type argument, that is, the user-defined datatypes are of the same kind [20]. It is possible to encode all user-defined datatypes into datatypes of this form, but that is against the spirit of polytypic functions, and we would like to have a ‘kind-polymorphic’ theory. We think this can be solved by an extension of the translation scheme, but we have not worked out the details. Thirdly, as it stands, the polytypic construct cannot handle mutual recursive types. However, we see no difficulties other than a more complicated syntax, in extending the polytypic construct to mutual recursive types.

Acknowledgements Discussions with Barry Jay, Mark Jones, Erik Meijer, Fritz Ruehr, Tim Sheard, and Phil Wadler on polytypic functions are gratefully acknowledged. Mark Jones showed us how to translate polytypic functions to Gofer with constructor classes.

References

[1] Martin Abadi, Luca Cardelli, Benjamin Pierce, and Gordon Plotkin. Dynamic typing in a statically typed language. ACM Transactions on Programming Languages and Systems, 13(2):237–268, 1991.

[2] Richard Bird, Oege de Moor, and Paul Hoogendijk. Generic programming with relations and functors. Submitted for publication, 1993.

[3] R.S. Bird. An introduction to the theory of lists. In M. Broy, editor, Logic of Programming and Calculi of Discrete Design, volume F36 of NATO ASI Series, pages 5–42. Springer–Verlag, 1987.

[4] R.S. Bird. Lectures on constructive functional programming. In M. Broy, editor, Constructive Methods in Computing Science, volume F55 of NATO ASI Series, pages 151–216. Springer–Verlag, 1989.

[5] C. Böhm and A. Berarducci. Automatic synthesis of type λ-programs on term algebras. Theoretical Computer Science, 39:135–154, 1985.

[6] L. Damas and R. Milner. Principal type-schemes for functional programs. In 9th Symposium on Priciples of Programming Languages, POPL ’82, pages 207–212, 1982.

[7] C. Dubois, F. Rouaix, and P. Weis. Extensional polymorphism. In 22nd Symposium on Priciples of Programming Languages, POPL ’95, pages 118– 129, 1995.

[8] J.H. Fasel, P. Hudak, S. Peyton Jones, and P. Wadler. Sigplan Notices Special Issue on the Functional Programming Language Haskell. ACM SIGPLAN notices, 27(5), 1992.

[9] P. Freyd. Recursive types reduced to inductive types. In Proceedings Logic in Computer Science, LICS ’90, pages 498–507, 1990.

[10] T. Hagino. Category Theoretic Approach to Data Types. PhD thesis, University of Edinburgh, 1987.

[11] C. Hall, K. Hammond, S. Peyton Jones, and P. Wadler. Type classes in Haskell. In Donald Sannella, editor, Proceedings Programming Languages and Systems-ESOP ’94, pages 241–256. Springer–Verlag, 1994. LNCS 788.

[12] Robert Harper and Greg Morrisett. Compiling polymorphism using intensional type analysis. In 22nd Symposium on Priciples of Programming Languages, POPL ’95, pages 130–141, 1995.

[13] James Hook and Tim Sheard. A semantics of compile-time reflection. Oregon Graduate Institute of Science and Technology, Beaverton, OR, USA, 1993.

[14] P. Jansson. Polytypism and polytypic unification. Master’s thesis, Chalmers University of Technology and University of Göteborg, 1995.

[15] C. Barry Jay. Polynomial polymorphism. In Proceedings of the Eighteenth Australasian Computer Science Conference, pages 237–243, 1995.

[16] J. Jeuring. Algorithms from theorems. In M. Broy and C.B. Jones, editors, Programming Concepts and Methods, pages 247–266. North-Holland, 1990.

[17] J. Jeuring. Polytypic combinatorial functions. Unpublished manuscript, 1994.

[18] J. Jeuring. Polytypic pattern matching. In S. Peyton Jones, editor, Conference Record of FPCA ’95, SIGPLAN-SIGARCH-WG2.8 Conference on Functional Programming Languages and Computer Architecture, pages 238–248, 1995.

[19] Mark P. Jones. A system of constructor classes: overloading and implicit higher-order polymorphism. In Proceedings of the 6th ACM Conference on Functional Programming Languages and Computer Architecture, FPCA ’93, pages 52–61, 1993.

[20] Mark P. Jones. Functional programming with overloading and higher-order polymorphism. In J. Jeuring and E. Meijer, editors, Advanced Functional Programming, LNCS 925, pages 97–136. Springer-Verlag, 1995.

[21] Xavier Leroy. Unboxed objects and polymorphic typing. In 19th Symposium on Principles of Programming Languages, POPL ’92, pages 177–188, 1992.

[22] Xavier Leroy. The caml light system release 0.7. Available from ftp.inria.fr in lang/caml-light, 1995.

[23] G. Malcolm. Data structures and program transformation. Science of Computer Programming, 14:255–279, 1990.

[24] E.G. Manes and M.A. Arbib. Algebraic Approaches to Program Semantics. Text and Monographs in Computer Science. Springer Verlag, 1986.

[25] L. Meertens. Paramorphisms. Formal Aspects of Computing, 4(5):413–425, 1992.

[26] E. Meijer, M. Fokkinga, and R. Paterson. Functional programming with bananas, lenses, envelopes, and barbed wire. In J. Hughes, editor, Proceedings of the 5th ACM Conference on Functional Programming Languages and Computer Architecture, FPCA ’91, pages 124–144, 1991.

[27] E. Meijer and G. Hutton. Bananas in space: Extending fold and unfold to exponential types. In S. Peyton Jones, editor, Conference Record of FPCA ’95, SIGPLAN-SIGARCH-WG2.8 Conference on Functional Programming Languages and Computer Architecture, pages 324–333, 1995.

[28] E. Meijer and J. Jeuring. Merging monads and folds for functional programming. In J. Jeuring and E. Meijer, editors, Advanced Functional Programming, LNCS 925, pages 228–266. Springer-Verlag, 1995.

[29] Erik Meijer and Mark Jones. Gofer goes bananas. Unpublished note, Utrecht University, 1994.

[30] R. Milner. A theory of type polymorphism in programming. Journal of Computer and Systems Sciences, 17:348–375, 1978.

[31] John C. Mitchell and Robert Harper. The essence of ML. In 15th Symposium on Priciples of Programming Languages, POPL ’88, pages 28–46, 1988.

[32] O. de Moor. Categories, relations and dynamic programming. PhD thesis, Oxford University, 1992. Technical Monograph PRG-98.

[33] O. de Moor. Categories, relations and dynamic programming. Mathematical Structures in Computer Science, 4:33–69, 1994.

[34] Fritz Ruehr. Analytical and structural polymorphism. Unpublished manuscript, 1992.

[35] Fritz Ruehr. Analytical and Structural Polymorphism Expressed Using Patterns Over Types. PhD thesis, University of Michigan, 1992.

[36] T. Sheard. Type parametric programming. Oregon Graduate Institute of Science and Technology, Portland, OR, USA, 1993.

[37] Tim Sheard. Automatic generation and use of abstract structure operators. ACM Transactions on Programming Languages and Systems, 13(4):531– 557, 1991.

[38] Tim Sheard. Personal communication. 1995.