Xref: utzoo comp.lang.scheme:2499 comp.theory:1987 comp.lang.functional:781
Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!wuarchive!udel!haven.umd.edu!socrates.umd.edu!socrates!rockwell
From: rockwell@socrates.umd.edu (Raul Rockwell)
Newsgroups: comp.lang.scheme,comp.theory,comp.lang.functional
Subject: Re: ML-like type-checker for Scheme subset?
Message-ID: <ROCKWELL.91May15084326@socrates.umd.edu>
Date: 15 May 91 13:43:26 GMT
References: <5710@goanna.cs.rmit.oz.au> <7487@rex.cs.tulane.edu>
Sender: rockwell@socrates.umd.edu (Raul Rockwell)
Followup-To: comp.lang.scheme,comp.theory,comp.lang.functional
Organization: Traveller
Lines: 39
In-Reply-To: fs@caesar.cs.tulane.edu's message of 13 May 91 19: 00:46 GMT

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 Rockwell