<div class="gmail_quote">On Mon, Feb 2, 2009 at 12:39 PM, Ketil Malde <span dir="ltr"><<a href="mailto:ketil@malde.org">ketil@malde.org</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;">
<div class="Ih2E3d">Gregg Reynolds <<a href="mailto:dev@mobileink.com">dev@mobileink.com</a>> writes:<br>
<br>
> This gives a very interesting way of looking at Haskell type<br>
> constructors: a value of (say) Tcon Int is anything that satisfies<br>
> "isA Tcon Int".<br>
<br>
</div>Reminiscent of arguments between dynamic and static typing camps - as<br>
far as I understand, a "dynamic type" is just a predicate. So<br>
division by zero is a "type error", since the domain of division is<br>
the type of all numbers except zero.<br>
<br>
In contrast, I've always thought of (static) types as disjoint sets of<br>
values.<br>
<div class="Ih2E3d"><br>
> My reasoning is that we can<br>
> define an infinite number of data constructors for it, including at<br>
> least all possible polynomials (by which I mean data constructors of<br>
> any arity taking args of any type).<br>
<br>
</div>I guess I don't quite understand what you mean by "Tcon Int" above.<br>
Could you give a concrete example of such a type?<br>
<div class="Ih2E3d"></div></blockquote><div><br>Just shorthand for something like "data Tcon a = Dcon a", applied to Int. Any data constructor expression using an Int will yield a value of type Tcon Int.</div>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><div class="Ih2E3d"><br>
> To my naive mind this sounds suspiciously like the set of all sets,<br>
> so it's too big to be a set.<br>
<br>
</div>I suspect that since types and values are separate domains, you avoid<br>
the complications caused by self reference.<br>
<div class="Ih2E3d"><br>
> In any case, Tcon Int does not depend on any particular constructor,<br>
> just as homo sapiens does not depend on any particular man. So it<br>
> can't be a set because it doesn't have its members essentially.<br>
<br>
</div>I don't follow this argument. Are you saying you can remove a<br>
data constructor from a type, and still have the same type? And<br>
because of this, the values of the type do not constitute a set?<br>
</blockquote><div><br>Yep. Well, that is /if/ you start from the "Open-World Assumption" - see <a href="http://en.wikipedia.org/wiki/Open_World_Assumption">http://en.wikipedia.org/wiki/Open_World_Assumption</a> (very important in ontologies e.g. OWL and Description Logics). Just because we know that e.g. expressions like Dcon 3 yield values of type Tcon Int does not mean that we know that those are the only such expressions. So we can't really say anything about how big it can be. Who knows, it might actually be a useful distinction for an OWL reasoner in Haskell. <br>
</div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><br>
I guess it boils down to how "Tcon Int" does not depend on any<br>
particular constructor.<br>
</blockquote><div><br>That seems like a good way of putting it.<br><br>-g</div></div><br>