mark@adler.philosophie.uni-stuttgart.de (Mark Johnson) (05/21/91)
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 <e,t> (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
doner@henri.ucsb.edu (John Doner) (05/22/91)
In article <MARK.91May21104405@adler.philosophie.uni-stuttgart.de> mark@adler.philosophie.uni-stuttgart.de (Mark Johnson) writes: >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. I've worked a little bit with the theorem prover/proof checker EKL, created by Ketonen & Weening at Stanford. It has both types and sorts, with the intent that types were mainly a syntactic idea, whereas sorts would have some semantic content. There are operations on types (union, product) and similar ones on sort. In fact, the algebras for types and sort appear to be isomorphic, so one initially wonders why it's necessary to do the same thing twice. And in practice, one often uses only one or the other. Awhile back, Ketonen told me they planned to do away with the distinction. John E. Doner doner@henri.ucsb.edu (805)893-3941 Dept. Mathematics, UCSB, Santa Barbara, CA 93106
fs@caesar.cs.tulane.edu (Frank Silbermann) (05/22/91)
<MARK.91May21104405@adler.philosophie.uni-stuttgart.de> mark@adler.philosophie.uni-stuttgart.de Mark Johnson: > 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. > > The notion of "sort" is a _semantic_ one; > the universe of entities is conceptualized > as divided into distinct sorts. > > The notion of "type" is a _syntactic_ one > expressions of a language are classified into distinct types. > > Clearly, type distinctions in a language are most useful > if they correspond to something semantic. > 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. Declarative programming paradigms (e.g. functional programming), are characterized by a very close correspondence between syntactic and semantic constructs. At least when proposing a new type system for functional programming, it would seem proper to explain the semantic meaning of "type" before core-dumping a set of mechanical rules. If the "types" _are_ meant to denote sorts, then these sorts (domains?) ought to be understood and explained. Frank Silbermann fs@cs.tulane.edu Tulane University New Orleans, Louisiana USA
lex@cogsci.ed.ac.uk (Alexander Holt) (05/23/91)
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 <e,t> (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 <e,t> 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
mark@adler.philosophie.uni-stuttgart.de (Mark Johnson) (05/24/91)
In reply to Lex Holt (lex@uk.ac.ed.cogsci), I suspect that the fact that 'sort' and 'type' are being used as virtual synonyms shows that the distinction between syntax and semantics is being lost. In my own area of feature structure logics, I sometimes get the feeling that researchers almost deliberately try to confuse the issue, and don't want to say if their entities are semantic objects (something _in_ the domain of discourse, where it would make sense to talk about _sorts_ of feature structure elements), or if they are constraints on such entities --- abstractly, a kind of expression from a 'language' for talking about feature structures (even if the 'expressions' of this language are directed graphs) --- so it would make sense to talk about _types_ of feature structure constraints. Regarding my Montague Grammar example, Lex Holt (lex@uk.ac.ed.cogsci) correctly notes that: > ... > Except that Montague and his followers would tend to call e/t and e//t > `categories', or `syntactic categories', and call <e,t> 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. > ... Yes, Lex is right. I had forgotten that Montague defines the meaning of English expressions by translating them into expressions of another language which he called IL, and expressions of categories e/t and e//t in English are both translated into expressions of _type_ <e,t> in IL. So in Montague's system the terms 'category' and 'type' classify expressions of the respective languages. (Since Montague defines the semantics of English via translation into IL, a lot of linguists _mistakenly_ think that the IL expression itself is the semantics of the English it translates, whereas it is the semantics of that IL translation that is the semantics of the English expression). Comments? Mark -- Mark Johnson Institut fuer maschinelle Sprachverarbeitung - Computerlinguistik Universitaet Stuttgart Keplerstrasse 17 D-7000 Stuttgart 1 West Germany. (you need "West" otherwise mail from the US is not delivered!) work 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