[Haskell-cafe] type metaphysics
Gregg Reynolds
dev at mobileink.com
Mon Feb 2 13:39:10 EST 2009
On Mon, Feb 2, 2009 at 11:51 AM, Lennart Augustsson
<lennart at 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090202/d54fcb5b/attachment.htm
More information about the Haskell-Cafe
mailing list