Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!sun-barr!olivea!uunet!mcsun!ukc!edcastle!edcogsci!lex From: lex@cogsci.ed.ac.uk (Alexander Holt) Newsgroups: comp.theory Subject: Re: Sorts, Types in logic and programming languages Message-ID: <5845@scott.ed.ac.uk> Date: 22 May 91 18:29:10 GMT References: <5710@goanna.cs.rmit.oz.au> <7487@rex.cs.tulane.edu> Organization: Centre for Cognitive Science, Edinburgh, UK Lines: 32 mark@adler.philosophie.uni-stuttgart.de (Mark Johnson) writes: > ( For example, expressions in the untyped lambda calculus have no > type, even though there are different sorts of entities described > (functions, constants, etc.). It's a little harder to find an > example of a typed language where the type distinctions don't > correspond to sort distinctions---the only one I know of is the > language IL devised by Richard Montague for describing the semantics > of natural language sentences, where expressions of type e/t and e//t > both denote entities of sort (I think I got this right) ). Except that Montague and his followers would tend to call e/t and e//t `categories', or `syntactic categories', and call a type. Given this usage, it is expressions of Montague's formal fragment of English that have categories, while types apply to expressions of the logic IL. This is not to deny that in studies of, for example, combinatory systems for syntactic categories (such as the Lambek calculus) categories are often called types. The use of `sort' is pretty variable too. In my experience, at least in the area of formal semantics for natural language, both `sort' and `type' have been used to mark distinctions in some semantic domain. The difference is that `sort' often seems to be used as a synonym for `primitive type', or is used in the description of a system that does not have complex types. Lex Holt Tel: +44 31 650 4452 | University of Edinburgh JANET: lex@uk.ac.ed.cogsci | Centre for Cognitive Science Internet: lex%cogsci.ed@nsfnet-relay.ac.uk | 2 Buccleuch Place UUCP: ...!uunet!mcsun!ukc!edcogsci!lex | Edinburgh EH8 9LW Scotland