paula@SHUM.HUJI.AC.IL (Paula Ross) (11/10/90)
Is there any way in ML that you can create a data type which accepts sequences of objects of different types (when the number and types of the objects are not known in advance) ? i.e. can you create a list type without the restriction that each element of the list must be of the same type ?
fraser@bilby.cs.uwa.oz.au (Fraser Wilson) (11/12/90)
In <paula.658247771@shum> paula@SHUM.HUJI.AC.IL (Paula Ross) writes: >Is there any way in ML that you can create a data type which accepts >sequences of objects of different types (when the number and types of the >objects are not known in advance) ? >i.e. can you create a list type without the restriction that each element of >the list must be of the same type ? As far as I know you can only do this using a union type, which means you have to know what types you will get. I don't think it can be done for an arbitary type. Fraser Wilson | Of all the knights in Appledore fraser@bilby.cs.uwa.oz | The bravest was Sir Thomas Tom | He multiplied as far as four There can be only one! | And knew what nine was taken from - CM | To make eleven. He could write | A letter to another knight. - A.A Milne
nick@cs.edinburgh.ac.uk (Nick Rothwell) (11/12/90)
In article <paula.658247771@shum>, paula@SHUM.HUJI.AC.IL (Paula Ross) writes: > Is there any way in ML that you can create a data type which accepts > sequences of objects of different types (when the number and types of the > objects are not known in advance) ? When they *are* known in advance, then you can use a datatype as a variant record (essentially): datatype Object = INTEGER of int | STRING of string | ... If you don't know how many cases you need in advance, then ML is (in theory) capable of expressing open-ended datatypes that you can add to. This is currently only available for the built-in type "exn" (the type of exceptions), so: exception A and B of int; val list = [A, B 4]; exception C of string; val list = (C "Hello") :: list; (A is a constructor of type exn, B has type int -> exn). But, since you have to introduce a new constructor for each new type you wish to work with, you have to retain the constructor in order to take a value apart for that type. -- Nick Rothwell, Laboratory for Foundations of Computer Science, Edinburgh. nick@lfcs.ed.ac.uk <Atlantic Ocean>!mcsun!ukc!lfcs!nick ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ "Now remember - and this is most important - you must think in Russian."
fs@caesar.cs.tulane.edu (Frank Silbermann) (11/12/90)
>In <paula.658247771@shum> paula@SHUM.HUJI.AC.IL (Paula Ross) writes: >> Is there any way in ML that you can create a data type >> which accepts sequences of objects of different types >> (when the number and types of the objects are not known >> in advance) ? i.e. can you create a list type without >> the restriction that each element of the list must be >> of the same type ? In article <fraser.658398987@melomys> fraser@bilby.cs.uwa.oz.au (Fraser Wilson) writes: > As far as I know you can only do this using a union type, > which means you have to know what types you will get. > I don't think it can be done for an arbitary type. One might seek to create a union type which contains within it _all_ possible types (i.e. as the solution to a recursive type equation). Unfortunately this violates the requirement that all type signatures be finite constructions from the primitive types. The problem is that typechecking (and type inference) in the typed lambda calculus is not generally decidable. To make typechecking decidable, we impose a restriction on type signatures, such as the one above. Because such restrictions handcuff the programmer, one line of reseach seeks to develop restrictions for decidablilty which maximize polymorphism. Because compromise between flexibility and safety will always involve a trade-off, I believe that untyped functional languages (e.g. those in the LISP/Scheme style) will never become completely obsolete. Frank Silbermann fs@cs.tulane.edu Tulane University New Orleans, Louisianna USA
suarez@prl.dec.com (Ascander Suarez) (11/13/90)
In article <4906@rex.cs.tulane.edu>, fs@caesar.cs.tulane.edu (Frank Silbermann) writes: |> ... |> One might seek to create a union type which |> contains within it _all_ possible types |> (i.e. as the solution to a recursive type equation). |> Unfortunately this violates the requirement |> that all type signatures be finite constructions |> from the primitive types. |> Although not in the standard, some versions of ML features the dynamic type. This type can be used to implement heterogeneous lists of values whose types are encapsulated as dynamics. A dynamic value can be seen as a pair (value, type of the value); ex (in caml V2-6): #let x = dynamic 3 and f = dynamic (fun x -> x);; Value x = (dynamic (3 : num)) : dyn Value f = (dynamic (<fun> : ('a -> 'a))) : dyn #let list = [f;x];; Value list = [(dynamic (<fun> : ('a -> 'a))); (dynamic (3 : num))] : dyn list #let classifyDyn = function # dynamic (b:bool) -> "bool" # | dynamic (n:num) -> "num" # | dynamic (l:'a list) -> "list" # | dynamic (f:'a ->'a) -> "id" # | _ -> "??";; Value classifyDyn = <fun> : (dyn -> string) #map classifyDyn list;; ["id"; "num"] : string list Of course there is one restriction related to the use of the dynamic constructor: It can't be used in local expressions to encapsulate a value whose type depends on the environment: Ex: #let g x = dynamic x;; line 1: cannot generalize type 'a of variable x for dynamic expression: dynamic x 1 error in typechecking Typecheck Failed - Ascander Suarez suarez@decprl.dec.com
chl@cs.man.ac.uk (Charles Lindsey) (11/13/90)
In <4906@rex.cs.tulane.edu> fs@caesar.cs.tulane.edu (Frank Silbermann) writes: >One might seek to create a union type which >contains within it _all_ possible types >(i.e. as the solution to a recursive type equation). >Unfortunately this violates the requirement >that all type signatures be finite constructions >from the primitive types. >The problem is that typechecking (and type inference) >in the typed lambda calculus is not generally decidable. >To make typechecking decidable, we impose a restriction >on type signatures, such as the one above. Please could you explain this more fully? I.e. can you show us an example of a recursive type equation that would cause problems in typechecking, together with the precise restriction that would cause it to be disallowed?
fs@caesar.cs.tulane.edu (Frank Silbermann) (11/14/90)
>>One might seek to create a union type which >>contains within it _all_ possible types >>(i.e. as the solution to a recursive type equation). >>Unfortunately this violates the requirement >>that all type signatures be finite constructions >>from the primitive types. > >>The problem is that typechecking (and type inference) >>in the typed lambda calculus is not generally decidable. >>To make typechecking decidable, we impose a restriction >>on type signatures, such as the one above. In article <chl.658489695@m1> chl@cs.man.ac.uk (Charles Lindsey) writes: > Please could you explain this more fully? > I.e. can you show us an example of a recursive type equation > that would cause problems in typechecking, together > with the precise restriction that would cause it > to be disallowed? I am not sure exactly how to answer your question, but since I am not expert on this subject. However, I've gathered these relevant statements from varied readings. A) General typechecking is said to be undecidable. B) In programming languages based on Church's typed lambda calculus, typechecking _is_ decidable. Therefore, if A) is true, these languages must impose some restriction to accomodate typechecking. 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). D) Church's typed lambda calculus subsumes the pure untyped lambda calculus as a special case. E) In the pure, untyped lambda calculus it _is_ possible to define a fixpoint combinator. Therefore, I conclude that typed languages (such as ML) must not permit the kind of type-unions necessary for definition of self-applicative functions. Frank Silbermann fs@cs.tulane.edu Tulane University New Orleans, Louisianna USA
wg@opal.cs.tu-berlin.de (Wolfgang Grieskamp) (11/16/90)
fs@caesar.cs.tulane.edu (Frank Silbermann) writes: >Because compromise between flexibility and safety >will always involve a trade-off, I believe that >untyped functional languages (e.g. those in the LISP/Scheme style) >will never become completely obsolete. There is no meaningful expression which has no type. In the case of lists consisting of values of different type, functions must exist defined over all instances of the "untyped" list in a given program to give meaning to the list. Thus the values of the list must have some common property (a type). In the very rare case, this property is to be just an object; in most other cases, the property will be much more specific: e.g. to be a number, a (graphic) view, etc. >Because such restrictions [on signatures] handcuff the programmer, >one line of reseach seeks to develop restrictions >for decidablilty which maximize polymorphism. Yes. The pragmatic problem for the design of a strongly-typed language maximizing polymorphism (regarding to ML polymorphism) is that its much harder for a programmer to keep track of sophisticated decidability restrictions then of (in a way) "syntacticly" expressable restrictions like non-recursive signatures. And the type-checker must handle undecidable problems, e.g. must avoid its own non-termination, still giving comfortable error reports. -- Wolfgang Grieskamp wg@opal.cs.tu-berlin.de tub!tubopal!wg wg%opal@DB0TUI11.BITNET
fs@caesar.cs.tulane.edu (Frank Silbermann) (11/16/90)
>> Because compromise between flexibility and safety >> will always involve a trade-off, I believe that >> untyped functional languages (e.g. those in the >> LISP/Scheme style) will never become completely obsolete. In article <2215@opal.cs.tu-berlin.de> wg@opal.cs.tu-berlin.de writes: >Wolfgang Grieskamp > There is no meaningful expression which has no type. > In the case of lists consisting of values of different type, > functions must exist defined over all instances > of the "untyped" list in a given program to give meaning to the list. > Thus the values of the list must have some common property (a type). > In the very rare case, this property is to be just an object ... ^^^^^^^^^ If you remove the imperative features from the core of Common Lisp, and remove the features which allow function definitions to be disassembled as lists, what remains _can_ be viewed as a functional language in which all expressions denote elements of the recursive domain D = (Atoms + Booleans + DxD + D->D)_bottom. It is "untyped" in the sense that all expressions denote objects of the same type -- domain D. You can create lists of arbitrary elements, and define functions which take and return arbitrary elements (even copies of the function itself). So it is not so rare actually to require only the property of being an object! I use just such a language as the basis for my work in functional/logic integration. Frank Silbermann fs@cs.tulane.edu Tulane University New Orleans, Louisianna USA
tmb@ai.mit.edu (Thomas M. Breuel) (11/16/90)
In article <4971@rex.cs.tulane.edu>, fs@caesar.cs.tulane.edu (Frank Silbermann) writes: |> >> Because compromise between flexibility and safety |> >> will always involve a trade-off, I believe that |> >> untyped functional languages (e.g. those in the |> >> LISP/Scheme style) will never become completely obsolete. |> |> > In the very rare case, this property is to be just an object ... |> ^^^^^^^^^ |> If you remove the imperative features from the core of Common Lisp, |> and remove the features which allow function definitions |> to be disassembled as lists, what remains _can_ be viewed |> as a functional language in which all expressions |> denote elements of the recursive domain |> |> D = (Atoms + Booleans + DxD + D->D)_bottom. Of course, you can use ML in the same way: datatype D = Atom of string | Bool of bool | Int of int | Real of real | Cons of (D * D) | Vector of (D array) But, at least in ML you have the option of using strong typing, whereas in CommonLisp (or other dynamically typed languages), there is no language support whatsoever for handling typing.
lgm@cbnewsc.att.com (lawrence.g.mayka) (11/16/90)
In article <11901@life.ai.mit.edu>, tmb@ai.mit.edu (Thomas M. Breuel) writes: > whereas in CommonLisp (or other dynamically typed languages), > there is no language support whatsoever for handling typing. Even with respect to compile-time typing, your statement is incorrect. Common Lisp permits (optional) type declarations, and implementations are invited to warn about any violation of them. Lawrence G. Mayka AT&T Bell Laboratories lgm@iexist.att.com Standard disclaimer.
peterson-john@cs.yale.edu (John C. Peterson) (11/16/90)
Regarding typing in Common Lisp & ML, it is incorrect to say that
Common Lisp lacks types; type declarations in CL are actually far more
general than those in ML. What Common Lisp lacks is any sort of well
defined type inference, a major deficiency.
John Petersonfs@caesar.cs.tulane.edu (Frank Silbermann) (11/17/90)
In article <11901@life.ai.mit.edu> tmb@ai.mit.edu writes: >In article <4971@rex.cs.tulane.edu>, fs@caesar.cs.tulane.edu (Frank Silbermann) writes: >|> >> Because compromise between flexibility and safety >|> >> will always involve a trade-off, I believe that >|> >> untyped functional languages (e.g. those in the >|> >> LISP/Scheme style) will never become completely obsolete. >|> >|> > In the very rare case, this property is to be just an object ... >|> ^^^^^^^^^ >|> If you remove the imperative features from the core of Common Lisp, >|> and remove the features which allow function definitions >|> to be disassembled as lists, what remains _can_ be viewed >|> as a functional language in which all expressions >|> denote elements of the recursive domain >|> >|> D = (Atoms + Booleans + DxD + D->D)_bottom. > >Of course, you can use ML in the same way: > >datatype D = Atom of string | Bool of bool | Int of int | > Real of real | Cons of (D * D) | Vector of (D array) I didn't know that -- thank you for correcting me. At least now we've finally answered the original question of <11901@life.ai.mit.edu> re how one can create an ML list of "anything". Just define datatype D as above, and then declare "list D". Frank Silbermann fs@cs.tulane.edu Tulane University New Orleans, Louisianna USA
tmb@ai.mit.edu (Thomas M. Breuel) (11/17/90)
In article <PETERSON-JOHN.90Nov15223106@object.cs.yale.edu>, peterson-john@cs.yale.edu (John C. Peterson) writes: |> Regarding typing in Common Lisp & ML, it is incorrect to say that |> Common Lisp lacks types; type declarations in CL are actually far more |> general than those in ML. What Common Lisp lacks is any sort of well |> defined type inference, a major deficiency. I didn't say that "CL lacks types", but that it does not have support for "handling typing". The fact that you can declare very general types that the compiler cannot possibly check at compile time is one indication of the problem. Sorry if I was imprecise.
wg@opal.cs.tu-berlin.de (Wolfgang Grieskamp) (11/17/90)
fs@caesar.cs.tulane.edu (Frank Silbermann) writes: > ... > D = (Atoms + Booleans + DxD + D->D)_bottom. >It is "untyped" in the sense that all expressions >denote objects of the same type -- domain D. >You can create lists of arbitrary elements, >and define functions which take and return arbitrary elements >(even copies of the function itself). >So it is not so rare actually to require only >the property of being an object! If a functions semantic maps D->D, then the rare case is that it maps also D/bottom->D/bottom. In fact i have problems to imagine meaningful functions except identity which behave like this. If you view types as a model to ensure that expressions are defined, then every expression has a type, since the programmer has some kind of theory wether his/her program is defined ( hope so :-) ). From the point of software engineering coming to terms with a formalized/communicatable type discipline seems to me very important. I believe that variants of bounded universal and existential type quantification together with dynamic binding (modelling whats called message passing in object-oriented languages) can make untyped languages obsolet in future in sense of giving a unique framework ranging infinitely variable from "untyped" to "strong-typed" programming style. -- Wolfgang Grieskamp wg@opal.cs.tu-berlin.de tub!tubopal!wg wg%opal@DB0TUI11.BITNET
wg@opal.cs.tu-berlin.de (Wolfgang Grieskamp) (11/17/90)
peterson-john@cs.yale.edu (John C. Peterson) writes: >Regarding typing in Common Lisp & ML, it is incorrect to say that >Common Lisp lacks types; type declarations in CL are actually far more >general than those in ML. What Common Lisp lacks is any sort of well >defined type inference, a major deficiency. As i remember from a short afair with LISP some years ago, type declarations in CL are always monomorphic: no parametric polymorphy, no type variables. Hence the "far more generalicity" you mentioned is to omit types? -- Wolfgang Grieskamp wg@opal.cs.tu-berlin.de tub!tubopal!wg wg%opal@DB0TUI11.BITNET
gudeman@cs.arizona.edu (David Gudeman) (11/18/90)
In article <2235@opal.cs.tu-berlin.de> Wolfgang Grieskamp writes:
]
]If a functions semantic maps D->D, then the rare case
]is that it maps also D/bottom->D/bottom. In fact i have problems
]to imagine meaningful functions except identity which behave like this.
I'm not sure I understand this. It sounds like you are talking about
functions that are strict in bottom (that is, if they are given bottom
as an argument, they produce bottom as a result). If so, then there
are hoards of natural functions that meet this criteria. Most
arithmetic functions for example. In fact, this case is so common
that some languages have only _one_ builtin function that is not
strict (if-then-else). And many languages do not allow the programmer
to define new non-strict functions, since they evaluate the arguments
before they call the function.
--
David Gudeman
Department of Computer Science
The University of Arizona gudeman@cs.arizona.edu
Tucson, AZ 85721 noao!arizona!gudemantmb@ai.mit.edu (Thomas M. Breuel) (11/19/90)
In article <2236@opal.cs.tu-berlin.de>, wg@opal.cs.tu-berlin.de (Wolfgang Grieskamp) writes: |> peterson-john@cs.yale.edu (John C. Peterson) writes: |> |> >Regarding typing in Common Lisp & ML, it is incorrect to say that |> >Common Lisp lacks types; type declarations in CL are actually far more |> >general than those in ML. What Common Lisp lacks is any sort of well |> >defined type inference, a major deficiency. |> |> As i remember from a short afair with LISP some years ago, type |> declarations in CL are always monomorphic: no parametric |> polymorphy, no type variables. |> |> Hence the "far more generalicity" you mentioned is to omit types? (deftype halting-function () '(and function (satisfies halting-p)))
wg@opal.cs.tu-berlin.de (Wolfgang Grieskamp) (11/19/90)
wg@opal.cs.tu-berlin.de (Wolfgang Grieskamp) writes: >peterson-john@cs.yale.edu (John C. Peterson) writes: > >Regarding typing in Common Lisp & ML, it is incorrect to say that > >Common Lisp lacks types; type declarations in CL are actually far more > >general than those in ML. What Common Lisp lacks is any sort of well > >defined type inference, a major deficiency. >As i remember from a short afair with LISP some years ago, type >declarations in CL are always monomorphic: no parametric >polymorphy, no type variables. Oh sorry, someone inspired me meanwhile to remember how it works in CS: its actually much more general then even, say, dependent types. Its based roughly on the general program transformation scheme (excuse LISP style errors): (def f '((T1 x1) ... (Tn xn)) E) => (def f '(x1 ... xn) '(if (and (T1 x1) ... (Tn xn)) E '(halt))) ... where Ti's are user defined predicates (checking types) or primitives for the predefined types. Now, the compiler can use abstract interpretation or other techniques to analysis preconditions Ti and actual arguments to applications of f (if he knows its an application) and generate type errors. This is a bit hard sometimes, but will often work for predefined types like bool, int, etc. - at least with the whole program under analysis. Hope i understood the "typing" discipline in Common LISP correct know (the LISP experts brought up typing and LISP should correct me otherwise). -- Wolfgang Grieskamp wg@opal.cs.tu-berlin.de tub!tubopal!wg wg%opal@DB0TUI11.BITNET
davis@barbes.ilog.fr (Harley Davis) (11/19/90)
In article <2236@opal.cs.tu-berlin.de> wg@opal.cs.tu-berlin.de (Wolfgang Grieskamp) writes: peterson-john@cs.yale.edu (John C. Peterson) writes: >Regarding typing in Common Lisp & ML, it is incorrect to say that >Common Lisp lacks types; type declarations in CL are actually far more >general than those in ML. What Common Lisp lacks is any sort of well >defined type inference, a major deficiency. As i remember from a short afair with LISP some years ago, type declarations in CL are always monomorphic: no parametric polymorphy, no type variables. Hence the "far more generalicity" you mentioned is to omit types? If you include CLOS, this is not true, at least for generic functions. It's still true for variables. -- Harley -- ------------------------------------------------------------------------------ Harley Davis internet: davis@ilog.fr ILOG S.A. uucp: ..!mcvax!inria!ilog!davis 2 Avenue Gallie'ni, BP 85 tel: (33 1) 46 63 66 66 94253 Gentilly Cedex France
jeff@aiai.ed.ac.uk (Jeff Dalton) (11/22/90)
In article <11901@life.ai.mit.edu> tmb@ai.mit.edu writes: >|> If you remove the imperative features from the core of Common Lisp, >|> and remove the features which allow function definitions >|> to be disassembled as lists, what remains _can_ be viewed >|> as a functional language in which all expressions >|> denote elements of the recursive domain >|> >|> D = (Atoms + Booleans + DxD + D->D)_bottom. But you can define new types using DEFSTRUCT and DEFCLASS. All of them are "atoms" in the sense of the predicate ATOM (ie, not a cons), but then so are functions. And any object can be used as a boolean. >Of course, you can use ML in the same way: > >datatype D = Atom of string | Bool of bool | Int of int | > Real of real | Cons of (D * D) | Vector of (D array) Not the same. "Atom" in CL does not mean "string". Even if we take it to mean "symbol" and suppose that ML could have symbols (why not?), it is possible in CL to add new types at run-time. >But, at least in ML you have the option of using strong typing, >whereas in CommonLisp (or other dynamically typed languages), >there is no language support whatsoever for handling typing. That is a very strong claim: no support whatsoever for typing. Indeed, it is false. -- Jeff
jeff@aiai.ed.ac.uk (Jeff Dalton) (11/22/90)
In article <4987@rex.cs.tulane.edu> fs@caesar.cs.tulane.edu (Frank Silbermann) writes: >>datatype D = Atom of string | Bool of bool | Int of int | >> Real of real | Cons of (D * D) | Vector of (D array) > >I didn't know that -- thank you for correcting me. >At least now we've finally answered the original question >of <11901@life.ai.mit.edu> re how one can create >an ML list of "anything". Just define datatype D as above, >and then declare "list D". D is not "anything"; it includes only 6 possibilities. That isn't all the types initially in Common Lisp, let alone those that can be added at run-time.
jeff@aiai.ed.ac.uk (Jeff Dalton) (11/22/90)
In article <11937@life.ai.mit.edu> tmb@ai.mit.edu writes: >In article <PETERSON-JOHN.90Nov15223106@object.cs.yale.edu>, peterson-john@cs.yale.edu (John C. Peterson) writes: >|> Regarding typing in Common Lisp & ML, it is incorrect to say that >|> Common Lisp lacks types; type declarations in CL are actually far more >|> general than those in ML. What Common Lisp lacks is any sort of well >|> defined type inference, a major deficiency. > >I didn't say that "CL lacks types", but that it does not have support >for "handling typing". But it does have support for "handling typing". It may not be enough support (in your view), it may not be the support you want, but your claim that there is no support whatsoever is just false. >The fact that you can declare very general types >that the compiler cannot possibly check at compile time is one >indication of the problem. Sorry if I was imprecise. If this is one indication of the problem, what is the problem? I don't doubt that the CL treatment of types has all sorts of problems, from various points of view.
ge@wn3.sci.kun.nl (Ge' Weijers) (12/05/90)
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)
markf@zurich.ai.mit.edu (Mark Friedman) (12/06/90)
In article <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). 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 This is cheating. The interesting property of the Y operator is that it does not make use of any primitive recursive definition mechanism. The above definition does this in the expression "g = f g". fac = y fac1 where fac1 f x = 1, x <= 1 = x * (fac1 (x-1)), otherwise I assume that you meant "= x * (f (x-1)), otherwise" for that last line. 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 This is a red herring. The above y is not the Y operator of interest to us; it does not create a procedure (i.e. a closure). The difficulties in writing and type checking the Y operator occur with higher order functions (i.e. first class procedures.) If Algol68 has them, try writing the "real" Y operator. Also, I assume you meant "ELSE x * f(f, x-1)". -Mark -- Mark Friedman MIT Artificial Intelligence Lab 545 Technology Sq. Cambridge, Ma. 02139 markf@zurich.ai.mit.edu
lloyd@bruce.cs.monash.OZ.AU (lloyd allison) (12/06/90)
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 )
iam@Gang-of-Four.Stanford.EDU (Ian Mason) (12/07/90)
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-
sanjiva@oravax.UUCP (Sanjiva Prasad) (12/07/90)
In article <1990Dec6.214847.19785@Neon.Stanford.EDU> iam@Gang-of-Four.Stanford.EDU (Ian Mason) 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 typed lambda calculus (without fixpoint primitives) is said to be strongly normalizing. So it should not be possible to write a Y combinator as a finite combination of primitives. To that extent you are right. The examples that someone gave about defining fixpoint combinators in ML, Miranda or Algol are all cheats, since they assume a recursive definition mechanism, or recursive (least fixed point) types. However, as Ian Mason points out using an example (more on that later), one can augment the typed lambda calculus with additional constructs that are NON-FUNCTIONAL and be able to write a fixpoint combinator for each nonempty ground (open question: weakly polymorphic?) arrow type "t1 -> t2". > >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- However, Ian Mason's use of ref is also a sleight of hand, because the behaviour of memory cells is an inherently recursive behaviour (Write down the bahaviour of a memory cell process in a CCS-like notation -- cf Milner's CCS). Bent Thomsen in his 89 POPL paper on higher-order CCS gives an (untyped) Y context that shows that recursion can be simulated in higher-order communicating processes. In our language Facile (see International Journal of Parallel Programming, Vol 18, No 2, April 1989, Plenum, pp 121-160), which is based on an extension of the typed lambda calulus with higher-order CCS-like constructs, we can indeed (for every ground arrow type t1 -> t2) define a recursion combinator. What we (Prateek Mishra, Alessandro Giacalone and I) have done is to modify Thomsen's treatment of a Y context that uses process creation and process passing to Facile, a call-by-value typed lambda calculus extension. (* We're still proving it is a recursion combinator with respect to the notion of program equivalence given in our ICALP'90 paper). Perhaps, in Flemming Nielson's TPL (see proceedings of PARLE '89) one can define a fixpoint combinator. This language too is based on the typed lambda calculus. [Since no notion of program equivalence is given there, we can't quite say that it indeed corresponds to the usual recursion combinator]. - Sanjiva
chl@cs.man.ac.uk (Charles Lindsey) (12/07/90)
In <2531@wn1.sci.kun.nl> ge@wn3.sci.kun.nl (Ge' Weijers) writes: >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 Both these contain bugs. I think what he meant to write was y f = g where g = f g fac = y fac1 where fac1 f x = 1, x <= 1 = x * (f (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(f, x-1) <---------------- FI; PROC y = (M f, INT x)INT: f (f,x); print((y(fac1,5), newline)) END In that form, the Algol68 program indeed works, and prints 120. However, I do not see that it is really equivalent to the Miranda version. Here is a better version, that also runs and prints 120. BEGIN MODE M = PROC(PROC(INT)INT,INT)INT; M fac1 = (PROC(INT)INT f, INT x)INT: IF x <= 1 THEN 1 ELSE x * f(x-1) FI; PROC y = (M f, INT x)INT: ( PROC g = (INT x)INT: f(g, x); f(g,x) ); print((y(fac1,5), newline)) END
hallgren@kermit.Berkeley.EDU (Thomas Hallgren) (12/08/90)
>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). Actually, you _can_ define a fixpoint combinator in Standard ML, in a purely functional way, without using recursion. ---------------------------------------------------------------------------- (* Defining a fix point combinator in ML, without using recursion *) datatype 'a T = K of 'a T -> 'a fun Y h = let fun g (K x) z= h (x (K x)) z (* no recursion! *) in g (K g) end; (* An example: the factorial function *) fun F f 0 = 1 | F f n = n * f(n-1); val fac = Y F; ----------------------------------------------------------------------------- The trick is the definition of the recursive type constructor T. In the language Fun, you can do it in a similar way: ----------------------------------------------------------------------------- (* The fixed point combinator Y can be defined without using recursion! *) rec type R[a]=R[a]->a; (* R is a recursively defined type operator *) value Y[a](h:a->a):a=(fun(x:R[a]) h (x x)) (fun(x:R[a]) h (x x)); value fac= let value F(f:Int->Int)(n:Int)= if n<=1 then 1 else n*f(n-1) in Y[Int->Int] F end; ----------------------------------------------------------------------------- The language Fun is described in "On Understanding Types, Data Abstraction, and Polymorphism", by L Cardelli & P Wegner, in ACM Computing Surveys, Vol 17, No 4, (Dec 1985). -- Thomas Hallgren hallgren@cs.chalmers.se