Xref: utzoo comp.lang.scheme:2489 comp.theory:1973
Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!swrinde!elroy.jpl.nasa.gov!sdd.hp.com!wuarchive!rex!caesar!fs
From: fs@caesar.cs.tulane.edu (Frank Silbermann)
Newsgroups: comp.lang.scheme,comp.theory
Subject: Re: ML-like type-checker for Scheme subset?
Message-ID: <7480@rex.cs.tulane.edu>
Date: 13 May 91 17:56:58 GMT
References: <5710@goanna.cs.rmit.oz.au>
Sender: news@rex.cs.tulane.edu
Organization: Computer Science Dept., Tulane Univ., New Orleans, LA
Lines: 61

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