Xref: utzoo comp.lang.scheme:2511 comp.theory:2000 comp.lang.functional:791 Path: utzoo!utgpu!news-server.csri.toronto.edu!bonnie.concordia.ca!uunet!mcsun!ukc!newcastle.ac.uk!turing!ncmh From: Chris.Holt@newcastle.ac.uk (Chris Holt) Newsgroups: comp.lang.scheme,comp.theory,comp.lang.functional Subject: Re: ML-like type-checker for Scheme subset? Message-ID: <1991May15.212335.15981@newcastle.ac.uk> Date: 15 May 91 21:23:35 GMT References: <5710@goanna.cs.rmit.oz.au> <7487@rex.cs.tulane.edu> Sender: news@newcastle.ac.uk Organization: University of Newcastle upon Tyne, UK, NE1 7RU Lines: 62 fs@caesar.cs.tulane.edu (Frank Silbermann) writes: >Type theory confuses me. >How does it fits into a language's semantics? Do you include the operators used to generate the values of a type in with that type? >I see two reasonable, yet mutually exclusive, >interpretations: >A) Some have explained typed functional languages > as being based on a _typed lambda calculus_. > If we interpret lambda calculus as a functional notation, > then an assertion that some lambda expression has type A->B > means that `A' is the name of the function's input domain, > and `B' the name of its codomain. where a function is a triple I assume you mean. Okay so far. > Therefore, the word `type' must be synonymous with > `domain' or, more specifically, `pointed complete partial order'. > (Yet, most authors neglect to develop this association, > or even to mention the idea of a partial ordering.) Are you requiring your functions to be monotonic? Or is this a red herring? >B) Others have suggested that a type discipline is > `imposed' on a language (i.e. that it is > not actually _part_ of the language, > but is rather a notation for the user > to embed statically-checkable invarient assertions). > Such a language would be based on a lambda calculus > of a single type (i.e. untyped). > To prevent use of undefined operations, > the type system permits the user to limit > a function's application to just one of several > component subdomains. Is this the same as saying that the type definition f: A -> B means that f is prefixed with a retract for A, and postfixed with a retract for B? Or is this what you meant with the typed version in (A) above? As far as I can see, the difference between your alternatives is whether an application to a value not in the domain returns bottom or is undefined, in the sense of being outside the system. Personally I have no trouble with 3 + true yielding bottom, but it worries some people. Is this what you mean? ----------------------------------------------------------------------------- Chris.Holt@newcastle.ac.uk Computing Lab, U of Newcastle upon Tyne, UK ----------------------------------------------------------------------------- "And when they die by thousands why, he laughs like anything." G Chesterton