Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!wuarchive!sdd.hp.com!ucsd!ucbvax!bloom-beacon!eru!hagbard!sunic!mcsun!unido!opal!wg From: wg@opal.cs.tu-berlin.de (Wolfgang Grieskamp) Newsgroups: comp.lang.functional Subject: Re: A question about types in ML Message-ID: <2235@opal.cs.tu-berlin.de> Date: 17 Nov 90 14:42:51 GMT References: <4906@rex.cs.tulane.edu> <2215@opal.cs.tu-berlin.de> <4971@rex.cs.tulane.edu> Sender: news@opal.cs.tu-berlin.de Reply-To: wg@opal.cs.tu-berlin.de Followup-To: comp.lang.functional Distribution: comp Organization: Technical University of Berlin Lines: 34 Nntp-Posting-Host: troll.cs.tu-berlin.de 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