Hi Martijn,<br><br>On Mon, Feb 2, 2009 at 9:49 AM, Martijn van Steenbergen &lt;<a href="mailto:martijn@van.steenbergen.nl">martijn@van.steenbergen.nl</a>&gt; wrote:<br>&gt;<br>&gt; There are many answers to the question &quot;what is a type?&quot;, depending on one&#39;s<br>
&gt; view.<br>&gt;<br>&gt; One that has been helpful to me when learning Haskell is &quot;a type is a set of<br>&gt; values.&quot;<br><br>That&#39;s the way I&#39;ve always thought of types, never having had a good reason to think otherwise. &nbsp;But it seems it doesn&#39;t work - type theory goes beyond set theory. &nbsp;I&#39;ve even found an online book[1] that uses type theory to construct set theory! &nbsp;At least I think that&#39;s what it does (not that I understand it.)<br>
<br>&gt;&gt; This gives a very interesting way of looking at Haskell type<br>&gt;&gt; constructors: a value of (say) Tcon Int is anything that satisfies<br>&gt;&gt; &quot;isA Tcon Int&quot;. &nbsp;The tokens/values of Tcon Int may or may not<br>
&gt;&gt; constitute a set, but even if they, we have no way of describing the<br>&gt;&gt; set&#39;s extension. &nbsp;<br>&gt;<br>&gt; Int has 2^32 values, just like in Java. You can verify this in GHCi:<br>&gt;<br><br>Ok, but that&#39;s an implementation detail.&nbsp; My question is what is the theoretical basis of types.<br>
<br>Notice that the semantics of Haskell&#39;s built-in types are a matter of social convention.&nbsp; The symbols used - Int, 0, 1, 2, ... - are well-known, and we agree not to add data constructors.&nbsp; But we could if we wanted to.&nbsp; Say, Foo ::&nbsp; Int -&gt; Int.&nbsp; Then Foo 3 is an Int, distinct from all other Ints; in particular it is not equal to &quot;3&quot;.<br>
<br>I suspect a full definition of type would have to say something about operations.<br><br>&gt;&gt; To my naive mind this sounds<br>&gt;&gt; suspiciously like the set of all sets, so it&#39;s too big to be a set.<br>&gt;<br>
&gt; Here you&#39;re probably thinking about the distinction between countable and<br>&gt; uncountable sets. See also:<br>&gt;<br><br>It could be that values of a constructed type form an uncountably large set, rather than something too big to be a set at all. I&#39;m afraid I don&#39;t know how to work with such critters.<br>
<br>In any case, the more interesting thing (to me) is the notion that sets contain their members &quot;essentially&quot;, but data types don&#39;t, as far as I can see.<br><br>Thanks much,<br><br>gregg<br><br><br>[1] <a href="http://www.cs.chalmers.se/Cs/Research/Logic/book/">http://www.cs.chalmers.se/Cs/Research/Logic/book/</a>