Hi and thanks for the response,<br><br><div class="gmail_quote">On Mon, Feb 2, 2009 at 10:32 AM, Lennart Augustsson <span dir="ltr"><<a href="mailto:lennart@augustsson.net">lennart@augustsson.net</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">Thinking of types as sets is not a bad approximation. You need to add<br>
_|_ to your set of values, though.<br>
<br>
So, Bool={_|_, False, True}, Nat={_|_,Zero,Succ _|_, Succ Zero, ...}<br>
</blockquote></div><br>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.<br><br>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.<br>
<br>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.)<br>
<br>Thanks,<br><br>gregg<br>