Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!uunet!mcsun!hp4nl!sci.kun.nl!wn3.sci.kun.nl!ge
From: ge@wn3.sci.kun.nl (Ge' Weijers)
Newsgroups: comp.lang.functional
Subject: Re: A question about types in ML
Message-ID: <2531@wn1.sci.kun.nl>
Date: 5 Dec 90 09:42:56 GMT
References: <4906@rex.cs.tulane.edu> <4953@rex.cs.tulane.edu>
Sender: root@sci.kun.nl
Distribution: comp
Lines: 58
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).
I assume that languages like Miranda (TM) and ML are based on typed lambda
calculus. In Miranda the Y combinator can be written as
y f = g
where
g = f g
fac = y fac1
where
fac1 f x = 1, x <= 1
= x * (fac1 (x-1)), otherwise
In Algol68 you can also write a Y combinator. The next example is not tested,
as elas no implementation is available to me anymore:
BEGIN
MODE M = PROC(M,INT)INT;
PROC fac1 = (M f, INT x)INT:
IF x <= 1
THEN 1
ELSE x * f(x-1)
FI;
PROC y = (M f, INT x)INT:
f (f,x);
print((y(fac1,5), newline))
END
(I hope this is about right, I don't have the RR handy at the moment)
>Therefore, I conclude that typed languages (such as ML)
>must not permit the kind of type-unions necessary
>for definition of self-applicative functions.
I conclude the opposite.
> Frank Silbermann fs@cs.tulane.edu
> Tulane University New Orleans, Louisianna USA
Ge' Weijers
University of Nijmegen, the Netherlands
--
Ge' Weijers Internet/UUCP: ge@cs.kun.nl
Faculty of Mathematics and Computer Science, (uunet.uu.net!cs.kun.nl!ge)
University of Nijmegen, Toernooiveld 1
6525 ED Nijmegen, the Netherlands tel. +3180652483 (UTC-2)