Xref: utzoo comp.lang.scheme:2502 comp.theory:1990 comp.lang.functional:782
Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!usc!zaphod.mps.ohio-state.edu!wuarchive!rex!caesar!fs
From: fs@caesar.cs.tulane.edu (Frank Silbermann)
Newsgroups: comp.lang.scheme,comp.theory,comp.lang.functional
Subject: Re: ML-like type-checker for Scheme subset?
Message-ID: <7504@rex.cs.tulane.edu>
Date: 15 May 91 20:14:15 GMT
References: <5710@goanna.cs.rmit.oz.au> <7480@rex.cs.tulane.edu> <1991May13.164558.3703@news.cs.indiana.edu>
Sender: news@rex.cs.tulane.edu
Organization: Computer Science Dept., Tulane Univ., New Orleans, LA
Lines: 71


>>		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