[Haskell-cafe] type metaphysics

[Gregg Reynolds]

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