[Prev][Next][Index][Thread]
Re: [very] basic question
> From: John R Harrison <johnh@ichips.intel.com>
>
>
> | datatype thing = T of thing -> bool ;
> |
> | [....]
> |
> | So if the type thing were a set then the cardinalities
> | |thing| and |{predicates on thing}| would be the same.
> | Note that {predicates on thing} is equiv to P (thing),
> | where P means power-set.
> | So the type thing cannot be modelled as a set.
>
> Your example does nothing to justify such a claim. It merely suggests
> that in such a model the type constructor "->" should not be interpreted
> as the full function space. Since there are only countably many
> computable functions, this is hardly a surprising observation. You might
> just as well say that floating-point numbers "cannot be modelled" as real
> numbers because the `+' you write in a program is not associative.
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.
But such models would have the unhelpful feature that there wouldn't
be much correspondence between the characteristics of floats (or types)
and those of reals, integers or whatever.
The textbooks I have which say types are sets also tell us that A -> B
means the entire set of functions from A to B.
(eg Sethi, Programming Languages Concepts and Constructs,
Watt, Programming Languages Concepts and Paradigms)
To me this is the "natural" way of thinking of types as sets,
and, as I understand it, my example shows that it doesn't work
for the ML/Haskell-like languages.
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.
Regards,
Jeremy
Follow-Ups: