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-