[Prev][Next][Index][Thread]
Re: [very] basic question
| 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'm
not taking any particular position on the type/set distinction here,
merely pointing out what seems to me something of an overstatement.
John.