[Haskell-cafe] type metaphysics

[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?

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.

There's a natural ordering of the elements {False,True,_|_}.  The _|_
is less than False and less than True, whereas False and True are
unordered with respect to each other.  Think of this ordering as how
much information you get.  Non-termination is less information than a
definite False or True.
Domain theory deals with this kind of ordered sets.

  -- Lennart

On Mon, Feb 2, 2009 at 4:51 PM, Gregg Reynolds <dev at mobileink.com> wrote:
> Hi and thanks for the response,
>
> On Mon, Feb 2, 2009 at 10:32 AM, Lennart Augustsson <lennart at augustsson.net>
> wrote:
>>
>> Thinking of types as sets is not a bad approximation.  You need to add
>> _|_ to your set of values, though.
>>
>> So, Bool={_|_, False, True}, Nat={_|_,Zero,Succ _|_, Succ Zero, ...}
>
> I'm afraid I haven't yet wrapped my head around _|_ qua member of a set.  In
> any case, I take it that sets being a reasonable /approximation/ of types
> means there is a difference.
>
> Back to metaphysics:  you pointed out that the function space is countable,
> and Christopher noted that there are countably many strings that could be
> used to represent a function.  So that answers my question about the size of
> e.g. Tcon Int.  But then again, that's only if we're working under the
> assumption that the "members" of Tcon Int are those we can express with data
> constructors and no others.  If we drop that assumption,then it seems we
> can't say much of anything about its size.
>
> FWIW, what started me on this is the observation that we don't really know
> anything about constructed types and values except that they are
> constructed. I.e. we know that "Foo 3" is the image of 3 under Foo, and
> that's all we know.  Any thing else (like operations) we must construct out
> of stuff we do know (like Ints or Strings.)  This might seem trivial, but to
> me it seems pretty fundamental, since it leads to the realization that we
> can use one thing (e.g. Ints) to talk about something we know nothing about,
> which seems to be what category theory is about.  (Amateur speaking here.)
>
> Thanks,
>
> gregg
>