On Mon, Feb 2, 2009 at 11:51 AM, Lennart Augustsson <lennart@augustsson.net> wrote:
If we're talking Haskell types here I think it's reasonable to talk
about the values of a type as those that we can actually express in
the Haskell program, any other values are really besides the point.
Well, if you have a more philosophical view of types then I guess
there is a point, but I thought you wanted to know about Haskell
types?

The metaphysics thereof.  ;)  I want to situate them in the larger intellectual context to get a more precise answer to "what is a type, really?"

There's nothing mysterious about _|_ being a member of a set.  Say
that you have a function (Int->Bool).  What are the possible results
when you run this function?  You can get False, you can get True, and
the function can fail to terminate (I'll include any kind of runtime
error in this).
So now we want to turn this bit of computing into mathematics, so we
say that the result must belong to the set {False,True,_|_} where
we've picked the name _|_ for the computation that doesn't terminate.
Note that is is mathematics, there's no notion of non-termination
here.  The function simply maps to one of three values.

I like that, thanks.
 
-gregg