Xref: utzoo comp.lang.scheme:2539 comp.theory:2016 comp.lang.functional:796
Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!think.com!spool.mu.edu!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: <7593@rex.cs.tulane.edu>
Date: 21 May 91 19:05:40 GMT
Article-I.D.: rex.7593
References: <1991May13.164558.3703@news.cs.indiana.edu> <7504@rex.cs.tulane.edu> <ROCKWELL.91May15223913@socrates.umd.edu>
Sender: news@rex.cs.tulane.edu
Organization: Computer Science Dept., Tulane Univ., New Orleans, LA
Lines: 45

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