[Haskell-cafe] type metaphysics

[Gregg Reynolds]

On Mon, Feb 2, 2009 at 12:39 PM, Ketil Malde <ketil at malde.org> wrote:

> Gregg Reynolds <dev at mobileink.com> writes:
>
> > This gives a very interesting way of looking at Haskell type
> > constructors: a value of (say) Tcon Int is anything that satisfies
> > "isA Tcon Int".
>
> Reminiscent of arguments between dynamic and static typing camps - as
> far as I understand, a "dynamic type" is just a predicate.  So
> division by zero is a "type error", since the domain of division is
> the type of all numbers except zero.
>
> In contrast, I've always thought of (static) types as disjoint sets of
> values.
>
> > My reasoning is that we can
> > define an infinite number of data constructors for it, including at
> > least all possible polynomials (by which I mean data constructors of
> > any arity taking args of any type).
>
> I guess I don't quite understand what you mean by "Tcon Int" above.
> Could you give a concrete example of such a type?
>

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.

>
> > To my naive mind this sounds suspiciously like the set of all sets,
> > so it's too big to be a set.
>
> I suspect that since types and values are separate domains, you avoid
> the complications caused by self reference.
>
> > In any case, Tcon Int does not depend on any particular constructor,
> > just as homo sapiens does not depend on any particular man.   So it
> > can't be a set because it doesn't have its members essentially.
>
> I don't follow this argument.  Are you saying you can remove a
> data constructor from a type, and still have the same type?  And
> because of this, the values of the type do not constitute a set?
>

Yep.  Well, that is /if/ you start from the "Open-World Assumption" - see
http://en.wikipedia.org/wiki/Open_World_Assumption (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.

>
> I guess it boils down to how "Tcon Int" does not depend on any
> particular constructor.
>

That seems like a good way of putting it.

-g
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090202/d26de7ac/attachment.htm