Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!dali.cs.montana.edu!uakari.primate.wisc.edu!sdd.hp.com!swrinde!ucsd!hub.ucsb.edu!henri!doner From: doner@henri.ucsb.edu (John Doner) Newsgroups: comp.theory Subject: Re: Sorts, Types in logic and programming languages Message-ID: <11461@hub.ucsb.edu> Date: 21 May 91 17:33:44 GMT References: <5710@goanna.cs.rmit.oz.au> <7487@rex.cs.tulane.edu> Sender: news@hub.ucsb.edu Reply-To: doner@henri.UUCP (John Doner) Organization: University of California, Santa Barbara Lines: 23 In article 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