Phil's (Robin Milner's ??) example typechecks in ML.
% Incidentally, there has been a lot of work done on Milner's type
% system extended to allow polymorphic recursion; this system is
% sometimes called ML+. One motivating example -- which I first
% heard from Milner -- is:
%
% data Trie x = Atom x | List [Trie x]
%
% maptrie :: (a -> b) -> Trie a -> Trie b
% maptrie f (Atom x) = Atom (f x)
% maptrie f (List xts) = List (map (maptrie f) xts)
The reason why there is no problem is that type Trie has a regular
recursion. One could modify the example as follows to get the desired effect:
data Trie x = Atom x | List (Trie [x])
maptrie f (Atom x) = Atom (f x)
maptrie f (List xts) = List (maptrie (map f) xts)
Frankly, I don't find this example a particularly convincing
justification for adding power of the type system.
Here is my favourite example,
de Bruijn lambda-calculus without any natural numbers:
data Opt x = ONE | An x
data Term x = Var x | App (Term x)(Term x) | Lam (Term(Opt x))
substitute :: (a -> Term b) -> Term a -> Term b
substitute f (Var v) = f v
substitute f (App a b) = App (substitute f a)(substitute f b)
substitute f (Lam t) =
Lam (substitute (\x ->
case x of {
ONE -> Var ONE;
An y -> substitute (Var.An) (f y) }
) t)
Again this does not typecheck, because Term has an irregular recursion
and substitute uses proper instances of its type in the last clause.
Stefan Kahrs
