Chris Haynes <chaynes@sunfish.cs.indiana.edu> (05/13/91)
>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
fs@caesar.cs.tulane.edu (Frank Silbermann) (05/14/91)
In article <5710@goanna.cs.rmit.oz.au> ok@goanna.cs.rmit.oz.au (Richard A. O'Keefe) writes: > I am pushing for Scheme to be adopted as the > (or an) introductory programming language here. > The essential programming concepts can be presented > with the exception of two: > > -- the idea that programming language implementations are entitled > to quietly deliver incorrect results (Pascal implementations > are often like this, and C implementations almost always are) > > -- static type checking. > > Static type checking could be introduced _after_ > the other concepts have been presented, > and an ML-style type checker would suit Scheme rather well. > There are a handful of functions like memq which would require > union types, but well-typed replacements are easy to define. > Has anyone already done this? Type theory confuses me. How does it fits into a language's semantics? I see two reasonable, yet mutually exclusive, interpretations: A) Some have explained typed functional languages as being based on a _typed lambda calculus_. If we interpret lambda calculus as a functional notation, then an assertion that some lambda expression has type A->B means that `A' is the name of the function's input domain, and `B' the name of its codomain. Therefore, the word `type' must be synonymous with `domain' or, more specifically, `pointed complete partial order'. (Yet, most authors neglect to develop this association, or even to mention the idea of a partial ordering.) 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). Such a language would be based on a lambda calculus of a single type (i.e. untyped). To prevent use of undefined operations, the type system permits the user to limit a function's application to just one of several component subdomains. I get confused when a author neglects to state which of the two interpretations he is using, or worse yet, if he alternates from one to the other. Unfortunately, this confusion is very common. Frank Silbermann fs@cs.tulane.edu Tulane University New Orleans, Louisiana USA
rockwell@socrates.umd.edu (Raul Rockwell) (05/15/91)
Frank Silbermann:
Type theory confuses me. How does it fits into a language's
semantics? I see two reasonable, yet mutually exclusive,
interpretations:
the word `type' must be synonymous with `domain' or, more
specifically, `pointed complete partial order'. (Yet, most
authors neglect to develop this association, or even to mention
the idea of a partial ordering.)
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).
I get confused when a author neglects to state which of the two
interpretations he is using, or worse yet, if he alternates from
one to the other. Unfortunately, this confusion is very common.
Well, after participating for the last month in the comp.lang.misc
"dynamic typing" (vs. static typing) threads, I almost hesitate to
follow up on this (give me another week :-).
A part of the confusion lies in the tendency of a language implementer
to think both in terms of the implemented language and the target
language. Quite often, types which are different in one are not
different in the other. (Though you could easily argue that for such
confusion to exist the implementer hasn't thought things through well
enough).
Anyway, the Right Orthodox View of Types (based on current compiler
technology and what I've been told on comp.lang.misc) seems to be that
the above two cases (type as domain vs type as static assertion) are
synonomous, and that there are no practical differences between the
two.
Your milage will vary.
Raul Rockwellfs@caesar.cs.tulane.edu (Frank Silbermann) (05/16/91)
>> A) Some have explained typed functional languages >> as being based on a _typed lambda calculus_. >> ... the word `type' must be synonymous with `domain', >> >> 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). chaynes@sunfish.cs.indiana.edu (Chris Haynes): > In some contexts the model theory of type systems > is studied without regard for the problems > of static type analysis (A), (I.e., describing the meaning of functional expressions that are _assumed_ to be well-typed) > and at other times,static type disciplines are studied > without regard for semantics models (B). Agreed. If you can both describe the model theory _and_ perform the static type analysis, the result is a typed functional programming language which fits paradigm A). rockwell@socrates.umd.edu (Raul Rockwell) adds: > type as domain vs type as static assertion > seem to be synonomous, with no practical differences. The difference has to do with the interpretation of type clashes. If types are domain names (A), then a type-clash is mathematical _nonsense_. Under this paradigm, a functional language can include _only_ well-typed programs. Ill-typed programs have no meaning. This severely hampers the usefulness of runtime typechecking, since the program is invalid _even if_ the type clash occurs in an unevaluated subexpression. In paradigm (B), a type clash _does_ have meaning in the language (even if that meaning is BOTTOM or ERROR). Instead of deciding mathematical validity, the type system weeds out (valid) programs which are viewed as _undesirable_ (i.e. those not likely to have captured the programmer's intent). Because well-typing is merely desired (but not mathematically essential), it need not be "strong." The choice between dynamic and static typing becomes a tradeoff between flexibility versus efficiency and safety. In conclusion, the determination of whether the type signature names a domain or whether it screens out undesirable portions of the domain has GREAT bearing upon: i) the language's model theory; and ii) the validity of dynamic typechecking. Frank Silbermann fs@cs.tulane.edu Tulane University New Orleans, Louisiana USA
Chris.Holt@newcastle.ac.uk (Chris Holt) (05/16/91)
fs@caesar.cs.tulane.edu (Frank Silbermann) writes: >Type theory confuses me. >How does it fits into a language's semantics? Do you include the operators used to generate the values of a type in with that type? >I see two reasonable, yet mutually exclusive, >interpretations: >A) Some have explained typed functional languages > as being based on a _typed lambda calculus_. > If we interpret lambda calculus as a functional notation, > then an assertion that some lambda expression has type A->B > means that `A' is the name of the function's input domain, > and `B' the name of its codomain. where a function is a triple <domain, codomain, pairs> I assume you mean. Okay so far. > Therefore, the word `type' must be synonymous with > `domain' or, more specifically, `pointed complete partial order'. > (Yet, most authors neglect to develop this association, > or even to mention the idea of a partial ordering.) Are you requiring your functions to be monotonic? Or is this a red herring? >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). > Such a language would be based on a lambda calculus > of a single type (i.e. untyped). > To prevent use of undefined operations, > the type system permits the user to limit > a function's application to just one of several > component subdomains. Is this the same as saying that the type definition f: A -> B means that f is prefixed with a retract for A, and postfixed with a retract for B? Or is this what you meant with the typed version in (A) above? As far as I can see, the difference between your alternatives is whether an application to a value not in the domain returns bottom or is undefined, in the sense of being outside the system. Personally I have no trouble with 3 + true yielding bottom, but it worries some people. Is this what you mean? ----------------------------------------------------------------------------- Chris.Holt@newcastle.ac.uk Computing Lab, U of Newcastle upon Tyne, UK ----------------------------------------------------------------------------- "And when they die by thousands why, he laughs like anything." G Chesterton
rockwell@socrates.umd.edu (Raul Rockwell) (05/16/91)
Frank Silbermann: If types are domain names then a type-clash is mathematical _nonsense_. Under this paradigm, a functional language can include _only_ well-typed programs. Ill-typed programs have no meaning. This severely hampers the usefulness of runtime typechecking, since the program is invalid _even if_ the type clash occurs in an unevaluated subexpression. Now I'm confused. Simple example: x % (y - z) where % indicates division. It seems to me that (A) this program has meaning, and (B) there is the potential for a type clash (y - z might be outside the domain of %). It also seems to me that this might be an unevaluated subexpression for conditions where the type clash occurs. Color me perplexed. Raul Rockwell
fs@caesar.cs.tulane.edu (Frank Silbermann) (05/22/91)
>> If types are domain names then a type-clash is mathematical >> nonsense. Under this paradigm, a functional language can include >> _only_ well-typed programs. Ill-typed programs have no meaning. >> This severely hampers the usefulness of runtime typechecking, since >> the program is invalid _even if_ the type clash occurs in an >> unevaluated subexpression. <ROCKWELL.91May15223913@socrates.umd.edu> rockwell@socrates.umd.edu Raul Rockwell: > > Simple example: x % (y - z) where % indicates division. > It seems to me that > (A) this program has meaning, and > (B) there is the potential for a type clash > (y - z might be outside the domain of %). One would like to say that the output domain of `y-z' is the set of integers, and that the input domain of `%' is the set of nonzero integers. Alternatively, one might say that `%' is a _partial_ function. Overlapping domains and partial functions are mathematically difficult to work with, and ordinary typed lambda calculus doesn't seem appropriate. Domain theory solves this problem by using a new BOTTOM value to trivially extend partial functions into total functions. E.g. (x % 0) is given the value BOTTOM. This converts the problem for a question of, "Does this expression make sense, mathematically?" to "Does this expression have a nontrivial meaning?" Whether you call division-by-zero a type error depends on whether your types represent domains (in which case division by zero is not a type error), or whether they represent computer checkable assertions, inserted as a runtime debugging aid (in which case division by zero _would_ be a type error). My point is that these two concepts have different logical implications. Frank Silbermann fs@cs.tulane.edu Tulane University New Orleans, Louisiana USA