Path: utzoo!utgpu!news-server.csri.toronto.edu!bonnie.concordia.ca!nstn.ns.ca!news.cs.indiana.edu!spool.mu.edu!sol.ctr.columbia.edu!ira.uka.de!rusmv1!rusmv1!mark From: mark@adler.philosophie.uni-stuttgart.de (Mark Johnson) Newsgroups: comp.theory Subject: Sorts, Types in logic and programming languages Message-ID: Date: 21 May 91 15:44:04 GMT References: <5710@goanna.cs.rmit.oz.au> <7487@rex.cs.tulane.edu> Sender: news@rusmv1.rus.uni-stuttgart.de (USENET News System) Followup-To: comp.theory Organization: IMSV, University of Stuttgart, Germany Lines: 56 In-Reply-To: rockwell@socrates.umd.edu's message of 15 May 91 13:43:26 GMT In most logic textbooks I've seen that deal with the topic at all (e.g. Gallier's "Logic for Computer Science", Andrews' "An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof") the notion of "sort" is a semantic one - the universe of entities is conceptualized as divided into distinct sorts - whereas the notion of "type" is a syntactic one - expressions of a language are classified into distinct types. Anyway, it seems to me in most work on programming languages the notions of sorts and types are systematically confused - often one hears the terms used as synonyms. Clearly, type distinctions in a language are most useful if they correspond to something semantic, say a sort distinction, so in practice often types and sorts are "coupled", i.e. expressions of a certain type are required to denote entities of a certain sort, but there is no logical necessity for this to be the case. ( 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) ). Comments? Mark Johnson -- Mark Johnson Institut fuer maschinelle Sprachverarbeitung - Computerlinguistik Universitaet Stuttgart Keplerstrasse 17 D-7000 Stuttgart 1 Germany. phone: 0711 - 121 3132. On leave until mid July 1991 from: Cognitive and Linguistic Sciences, Box 1978 Brown University Providence, RI 02912 USA email addresses: mark@adler.philosophie.uni-stuttgart.de mj@cs.brown.edu markj@ai.mit.edu johnson@csli.stanford.edu mark@ego.mit.edu