Re: [very] basic question

To: scott@projtech.com, types@cis.upenn.edu
Subject: Re: [very] basic question
From: jeremy@discus.anu.edu.au
Date: Thu, 8 Nov 2001 09:17:51 +1100 (EST)

  Could someone explain the difference between types & sets?  The maths
  texts I have available (undergrad comp. sci. stuff) state their
  equivalence explicitly, yet many writings I've looked up on the web
  differentiate between them.

In functional programming languages (such as Standard ML, 
used in the following example) a type may well not be a set.

For example

(* set up a type called thing *)
datatype thing = T of thing -> bool ;

(* an example value of this type *)
val example_thing = T (fn _ => true) ;

(* an isomorphism between things and functions : thing -> bool *)

val make_thing = T ;
fun dest_thing (T f) = f ;

(* ie make_thing and dest_thing are mutually inverse; *)

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.

When you run the above, the output (which reports types of the 
things - excuse the pun - you've declared)

> New type names: thing
  datatype thing = (thing,{con T : (thing -> bool) -> thing})
  con T = fn : (thing -> bool) -> thing
- > val example_thing = T fn : thing
- > val make_thing = fn : (thing -> bool) -> thing
- > val dest_thing = fn : thing -> thing -> bool

Jeremy Dawson