Re: [very] basic question

To: jeremy@discus.anu.edu.au
Subject: Re: [very] basic question
From: John R Harrison <johnh@ichips.intel.com>
Date: Fri, 09 Nov 2001 08:54:41 -0800
cc: types@cis.upenn.edu, John Harrison <johnh@ichips.intel.com>
In-Reply-To: Your message of "Fri, 09 Nov 2001 10:36:52 +1100." <200111082336.KAA23650@discus.anu.edu.au>


| I probably would say that, actually, though I have to admit I'd be wrong,
| since I can't deny you could model floats (or types, for that matter)
| as reals, integers, naturals or even prime numbers.

I wasn't trying to engage in that kind of sophistry. The analogy I was
making is simply the following. You can model floating-point numbers by
reals, though floating-point addition is not modelled by real addition.
Similarly, you can perfectly well model the types of programming
languages as sets, though the function type constructor is not
interpreted as the (at least full) set-theoretic function space.

| If there's a way of fixing this model of types as sets by  having type
| constructor "->" mean something less than the full function space, I'd be
| interested to hear about it.

There's an extensive literature on set-theoretic models of recursively
defined domains, even for languages without type distinctions, starting
with Scott's first models for untyped lambda calculus (D_infinity,
P(omega) etc.)

John.

References:

Re: [very] basic question

From: jeremy@discus.anu.edu.au