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) Brought to you by Super Global Mega Corp .com