[Haskell-cafe] type metaphysics

[Gregg Reynolds]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090202/b1fae972/attachment.htm