Path: utzoo!censor!geac!torsqnt!news-server.csri.toronto.edu!cs.utexas.edu!uunet!zephyr.ens.tek.com!uw-beaver!cornell!oravax!sanjiva
From: sanjiva@oravax.UUCP (Sanjiva Prasad)
Newsgroups: comp.lang.functional
Subject: Re: A question about types in ML
Message-ID: <1832@oravax.UUCP>
Date: 7 Dec 90 15:43:22 GMT
References: <3438@bruce.cs.monash.OZ.AU> <1990Dec6.214847.19785@Neon.Stanford.EDU>
Reply-To: sanjiva@oravax.odyssey.UUCP (Sanjiva Prasad)
Distribution: comp
Organization: Odyssey Research Associates, Ithaca, New York
Lines: 61

In article <1990Dec6.214847.19785@Neon.Stanford.EDU> iam@Gang-of-Four.Stanford.EDU (Ian Mason) writes:
>>fs@caesar.cs.tulane.edu (Frank Silbermann) writes:
>
>>C) I've never seen a programming language
>>   based on typed lambda calculus whose typechecking system
>>   permits the user to define a fixpoint combinator
>>   out of more primitive elements.  The type signature
>>   of the necessary lambda expression cannot be written
>>   as a finite combination of the primitive types
>>   (so Y-combinators must be added as primitives).

The typed lambda calculus (without fixpoint primitives) is said to be
strongly normalizing. So it should not be possible to write a Y combinator
as a finite combination of primitives. To that extent you are right. The
examples that someone gave about defining fixpoint combinators in ML, 
Miranda or Algol are all cheats, since they assume a recursive definition 
mechanism, or recursive (least fixed point) types. 

However, as Ian Mason points out using an example (more on that later), 
one can augment the typed lambda calculus with additional constructs that 
are NON-FUNCTIONAL and be able to write a fixpoint combinator for each
nonempty ground (open question: weakly polymorphic?) arrow type "t1 -> t2". 

>
>if one adds ml references to the simply typed (lazy) lambda calculus,
>then for each non-empty  functional type (s->t) one can write 
>a fixpoint combinator for that type. assume that g: s-> t, then
>(using a mish mash of typed lambda calculus and ml notation) one
>such example is
>
> lambda N : (s->t)->(s->t) . 
>    let z = ref g in  ( z := (lambda x : s . ( N(! z)(x))) ; (! z)
>
>note that g is only used as a dummy to allocate the necessary cell
>for the  self reference.
>
>		-iam-		

However, Ian Mason's use of ref is also a sleight of hand, because the
behaviour of memory cells is an inherently recursive behaviour (Write down
the bahaviour of a memory cell process in a CCS-like notation -- cf Milner's 
CCS). Bent Thomsen in his 89 POPL paper on higher-order CCS gives an (untyped)
Y context that shows that recursion can be simulated in higher-order 
communicating processes. 

In our language Facile (see International Journal of Parallel Programming, 
Vol 18, No 2, April 1989, Plenum, pp 121-160), which is based on an
extension of the typed lambda calulus with higher-order CCS-like constructs,
we can indeed (for every ground arrow type t1 -> t2) define a recursion
combinator. What we (Prateek Mishra, Alessandro Giacalone and I) have done 
is to modify Thomsen's treatment of a Y context that uses process creation 
and process passing to Facile, a call-by-value typed lambda calculus 
extension. (* We're still proving it is a recursion combinator with respect 
to the notion of program equivalence given in our ICALP'90 paper). 

Perhaps, in Flemming Nielson's TPL (see proceedings of PARLE '89) one
can  define a fixpoint  combinator. This language too is based on the typed 
lambda calculus. [Since no notion of program equivalence is given there, we
can't quite say that it indeed corresponds to the usual recursion combinator].

- Sanjiva