Alex Rivera | Logout

What is an existential type?

Asked 2008-11-15T07:31:00.803
216

I read through the Wikipedia article Existential types. I gathered that they're called existential types because of the existential operator (∃). I'm not sure what the point of it is, though. What's the difference between

T = ∃X { X a; int f(X); }

and

T = ∀x { X a; int f(X); }

?

Edit
Report

2 Answers

44

I think it makes sense to explain existential types together with universal types, since the two concepts are complementary, i.e. one is the "opposite" of the other.

I cannot answer every detail about existential types (such as giving an exact definition, list all possible uses, their relation to abstract data types, etc.) because I'm simply not knowledgeable enough for that. I'll demonstrate only (using Java) what this HaskellWiki article states to be the principal effect of existential types:

Existential types can be used for several different purposes. But what they do is to 'hide' a type variable on the right-hand side. Normally, any type variable appearing on the right must also appear on the left […]

Example set-up:

The following pseudo-code is not quite valid Java, even though it would be easy enough to fix that. In fact, that's exactly what I'm going to do in this answer!

class Tree<α>
{
    α       value;
    Tree<α> left;
    Tree<α> right;
}

int height(Tree<α> t)
{
    return (t != null)  ?  1 + max( height(t.left), height(t.right) )
                        :  0;
}

Let me briefly spell this out for you. We are defining…

  • a recursive type Tree<α> which represents a node in a binary tree. Each node stores a value of some type α and has references to optional left and right subtrees of the same type.

  • a function height which returns the furthest distance from any leaf node to the root node t.

Now, let's turn the above pseudo-code for height into proper Java syntax! (I'll keep on omitting some

answered 2011-12-31T03:52:41.887
12

An existential type is an opaque type.

Think of a file handle in Unix. You know its type is int, so you can easily forge it. You can, for instance, try to read from handle 43. If it so happens that the program has a file open with this particular handle, you'll read from it. Your code doesn't have to be malicious, just sloppy (e.g., the handle could be an uninitialized variable).

An existential type is hidden from your program. If fopen returned an existential type, all you could do with it is to use it with some library functions that accept this existential type. For instance, the following pseudo-code would compile:

let exfile = fopen("foo.txt"); // No type for exfile!
read(exfile, buf, size);

The interface "read" is declared as:

There exists a type T such that:

size_t read(T exfile, char* buf, size_t size);

The variable exfile is not an int, not a char*, not a struct File—nothing you can express in the type system. You can't declare a variable whose type is unknown and you cannot cast, say, a pointer into that unknown type. The language won't let you.

answered 2009-04-13T01:12:29.683

Your Answer