To illustrate a need for recursive type synonyms, Joe suggests the example:
| nil f g = f
| cons x xs f g = g x xs
|
| fold f z xs = xs z (\x xs -> f x (fold f z xs))
Indeed, this doesn't type check in Haskell, and recursive type synonyms
would fix it. (So would general recursive types if we defined List a b
as a synonym for mu l . b -> (a -> l -> b) -> b.) However, these definitions
don't quite correspond to the standard encoding of data structures as
functions. In polymorphic lambda calculus, we might define a type of lists:
List a = Forall b . b -> (a -> b -> b) -> b
nil = /\a. /\b. \n:b. \c:(a -> b -> b). n
cons = /\a. \x:a. \xs:List a. /\b. \n:b. \c:(a -> b -> b). c x (xs b n c)
Projecting back into a Hindley/Milner type system for Haskell gives:
type List a b = b -> (a -> b -> b) -> b
nil :: List a b
nil f g = f
cons :: a -> List a b -> List a b
cons x xs f g = g x (xs f g)
which is accepted by the type system (the price of the reduced polymorphism
being the need to carry the return type `b' around as an extra part of the
type of the lists). We can still define a fold function:
fold :: b -> (a -> b -> b) -> List a b -> b
fold z f xs = xs z f
and then, if we define example = cons 1 (cons 2 (cons 3 (cons 4 nil))), we
can find that fold 0 (+) example = 10 and fold 1 (*) example = 24.
So, I can't do the example exactly as Joe gave it without using recursive
types, but there is another way to do the same kind of things that doesn't
need recursive types or, in particular, recursive type synonyms.
Mark
