Xref: utzoo comp.theory:2018 comp.lang.functional:797 Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!think.com!samsung!rex!caesar!fs From: fs@caesar.cs.tulane.edu (Frank Silbermann) Newsgroups: comp.theory,comp.lang.functional Subject: Re: Sorts, Types in logic and programming languages Message-ID: <7594@rex.cs.tulane.edu> Date: 21 May 91 19:28:44 GMT References: <7487@rex.cs.tulane.edu> Sender: news@rex.cs.tulane.edu Organization: Computer Science Dept., Tulane Univ., New Orleans, LA Lines: 32 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