Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!sdd.hp.com!usc!samsung!munnari.oz.au!bruce!lloyd From: lloyd@bruce.cs.monash.OZ.AU (lloyd allison) Newsgroups: comp.lang.functional Subject: Re: A question about types in ML Message-ID: <3438@bruce.cs.monash.OZ.AU> Date: 6 Dec 90 03:53:28 GMT References: <4906@rex.cs.tulane.edu> <4953@rex.cs.tulane.edu> <2531@wn1.sci.kun.nl> Distribution: comp Organization: Monash Uni. Computer Science, Australia Lines: 62 In <2531@wn1.sci.kun.nl> ge@wn3.sci.kun.nl (Ge' Weijers) 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 self application (g g) in Y=\G.(\g.G(g g))(\g.G(g g)) requires a recursive type g:T where T=T->... You can program Y in SML: "cut the knot" with a constructor. You program the recursive version of Y in Pascal! but not the "proper" one as `function' is outside the type system. The following works in Algol 68: ( # Fixed-Pt Operator, Y, in Algol-68 L.Allison UWA 15/7/85 # MODE INTFN = PROC( INT )INT; MODE RECFF = PROC( RECFF, INT ) INT; MODE FFORM = PROC( INTFN, INT ) INT; #------------------------------------------------------------------------# PROC y = ( FFORM f, INT n ) INT: ( RECFF h = ( RECFF g, INT n ) INT: ( INTFN b = ( INT n ) INT: g( g, n ); f( b, n ) ); h( h, n ) ); FFORM big f = ( INTFN little f, INT n ) INT: IF n=0 THEN 1 ELSE n * little f(n-1) FI; INTFN usual factorial = (INT n) INT: IF n=0 THEN 1 ELSE n * usual factorial(n-1) FI; INTFN unusual factorial = (INT n) INT: big f( usual factorial, n); INTFN odd factorial = (INT n) INT: y( big f, n ); #-----------------------------------------------------------------------# FOR i TO 5 DO print(( usual factorial(i), unusual factorial(i), odd factorial(i), newline )) OD ) Brought to you by Super Global Mega Corp .com