On Mon, Feb 2, 2009 at 11:51 AM, Lennart Augustsson
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