Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!usc!apple!agate!shelby!neon!Gang-of-Four.Stanford.EDU!iam
From: iam@Gang-of-Four.Stanford.EDU (Ian Mason)
Newsgroups: comp.lang.functional
Subject: Re: A question about types in ML
Message-ID: <1990Dec6.214847.19785@Neon.Stanford.EDU>
Date: 6 Dec 90 21:48:47 GMT
References: <3438@bruce.cs.monash.OZ.AU>
Sender: news@Neon.Stanford.EDU (USENET News System)
Reply-To: iam@Gang-of-Four.Stanford.EDU (Ian Mason)
Distribution: comp
Organization: Stanford University
Lines: 27

i though i posted a note yesterday but it failed to appear,
so i'll try try again.


>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).

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-		


Brought to you by Super Global Mega Corp .com