Xref: utzoo comp.lang.scheme:2491 comp.theory:1975 Newsgroups: comp.lang.scheme,comp.theory Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!sdd.hp.com!news.cs.indiana.edu!chaynes@sunfish.cs.indiana.edu From: Chris Haynes Subject: Re: ML-like type-checker for Scheme subset? Message-ID: <1991May13.164558.3703@news.cs.indiana.edu> Organization: Computer Science, Indiana University, Bloomington. References: <5710@goanna.cs.rmit.oz.au> <7480@rex.cs.tulane.edu> Date: Mon, 13 May 91 16:45:43 EST >Type theory confuses me. >How does it fits into a language's semantics? >I see two reasonable, yet mutually exclusive, > > >A) Some have explained typed functional languages > as being based on a _typed lambda calculus_. >... > >B) Others have suggested that a type discipline is > `imposed' on a language (i.e. that it is > not actually _part_ of the language, > but is rather a notation for the user > to embed statically-checkable invarient assertions). >... A and B *may* be mutually exclusive. In some contexts the model theory of type systems is studied without regard for the problems of static type analysis (A), and at other times static type disciplines are studied without regard for semantics models (B). But in the case of most practical type systems views A and B *can* coexist. That is, a type system may have both a model theory and a decidable syntactic deduction system. In this case one hopes for completeness and consistency theorems, which establish that these two views are suitably related. Chris Haynes