[Prev][Next][Index][Thread]
Greatest fixpoints have existential types
Date: Fri, 13 Jul 90 19:12:44 BST
Hagino wrote a very nice paper on adding least and greatest fixpoints
of covariant functors explicitly to simply typed lambda calculus (LNCS
238). He mentions that it is possible to code least fixpoints directly
in polymorphic lambda calculus, and states that he doesn't know whether
it is possible to similarly code greatest fixpoints.
Least fixpoint are coded in polymorphic lambda calculus by
the formula
Lfix X. T(X) = All X. (T(X) -> X) -> X
where Lfix is the least fixpoint and T is a covariant functor (or,
equivalently, a type where X appears only in positive positions). This
is not always a true least fixpoint, but will be so in certain models
(e.g., those satisfying parametricity).
Similarly, we can make the coding
Gfix X. T(X) = Exists X. (X -> T(X)) * X
where Gfix is the greatest fixpoint and T is still a covariant
functor. Is this known? It seems an obvious dual of the least
fixpoint result, but Hagino seems unaware of it.
For example, streams of integers are yielded by the greatest fixpoint
of T(X) = Int * X. The formula above instantiates to
IntStream
= Gfix X. Int * X
= Exists X. (X -> Int * X) * X
= Exists X. (X -> Int) * (X -> X) * X.
Essentially, what is going on here is that from the abstract type
(X, (h, t, x)) one can only extract terms of the form (h (t^i x)),
which corresponds to the i'th element of the stream. This is slightly
surprising, as it gives a way of embedding an infinite stream in a
language that has strong normalisation.
Hagino suggests that streams be defined by operations
generate, head, and tail. We can define these by:
generate : All X. ((X -> Int) * (X -> X) * X) -> IntStream
= Lam X. lam (h, t, x). (X, (h, t, x))
head : IntStream -> Int
= lam s. case s of {(X, (h, t, x)) -> h x}
tail : IntStream -> IntStream
= lam s. case s of {(X, (h, t, x)) -> (X, (h, t, t x))}
(The notation used above is based on viewing existential types as
generalised products. It is explained by the following typing and
reduction rules:
A |- v:V[U/X]
-----------------------
A |- (U,v) : Exists X.V
A |- t : Exists X.V A, y:V |- w:W
------------------------------------- (X not in A, W)
A |- (case t of {(X,y) -> w}) : W
(case (U,v) of {(X,y) -> w}) ---> w[U/X, V/y]
Mitchell and Plotkin write (X,u) as (pack X u) and
(case t of {(X,y) -> w}) as (abstype X y is t in w).)
Regarding pragmatics, it is well known that the embedding of least
fixpoints is less efficient than one would like. For instance, the
operation to find the tail of a list takes time proportional to the
length of the list: one would hope that this takes constant time.
Greatest fixpoints have a dual problem: finding the tail of a stream is
cheap, but consing an element onto the front of a stream is more
expensive than one would like. So one would still be tempted to add
least and greatest fixpoints to a language for pragmatic reasons, though
it is good to know that in doing so one does not change the language in
any fundamental way (in particular, strong normalisation is still
preserved).
By the way, is there any known way of coding lists in polymorphic
lambda calculus that (a) uses space proportional to the length of the
list, (b) performs cons in constant time, and (c) performs tail in
constant time? Or is there a proof that this is impossible?
Any comments on these ideas would be welcome.
-- Phil