How do existential types differ from interfaces?

Question

Given the existential type

T = ∃X.{op₁:X, op₂:X→boolean}

and this generic Java interface:

interface T<X> {
    X op₁();
    boolean op₂(X something);
}

What are the fundamental differences between the existential type and the Java interface?

Obviously there are syntactical differences, and Java's object-orientation (which also includes details such as hidden this parameters etc.). I'm not so much interested in these as in conceptual and semantic differences — though if someone would like to shed light on some finer points (such as the notational difference between T vs. T<X>), that would be appreciated too.

Answer 1

Hmm... That definition looks very similar to some haskell sample I've seen long time ago.

{-# LANGUAGE ExistentialQuantification #-}
data X = forall a . X { value :: a, viewValue :: a -> String }
instance Show X where show (X { value = x, viewValue = f}) = f x
sample :: [X]
sample = [X 3 show, X "abc" show, X 3.14 show]

When constructor X is applied ∀ actually becomes ∃. Note that when you take out value you don't know the type and have empty set of operation over it. But since viewValue is kinda coherent with value it can be applied to it.

I guess the main difference of Java interface you proposed is the fact that you have to know intermediate type for passing result of op₁ to op₂. I.e. proper system for existential type should select the right type which is guaranteed to exist by condition. I.e. you should be able to write function with type: ∀X. X→(X→boolean)→T. In prev sample such function is X constructor used in X 3 show (show is function which takes argument of any type that implements Show and returns String)

Updated: I just re-read your question and I think I've got proper construction for Java:

interface T {
    boolean op₂();
}
...
T x = new T() {
    private final int op₁ = ...;
    public boolean op₂() { return ((op₁ % 2) == 0); }
};
T y = new T() {
    private final char op₁ = ...;
    public boolean op₂() { return ('0' <= op₁ && op₁ <= '9'); }
};
if (x.op₂() && y.op₂()) ...

You are right about mentioning this - it's actually your op₁.

So I guess I understood now that classical OOP languages (Java, C#, C++ etc) always implement existential type with single value this and a functions over it called "methods" which implicitly called with that value :)

P.S. Sorry, I'm not very familiar with Java, but I hope you've got the idea.

Answer 2

The only difference is that the Java interface actually means something to the Java compiler.

The existential type is the formal definition of a type, non-specific to any language. Computer scientists use this sort of definition to prove things about the type and about languages implementing it. The Java interface is one of Java's implementations of the formally defined type.

Answer 3

The 2 presented types are very different from each other. The interface definition you've written is an universal type (Java generics in general fall in this category).

An existential type hides a type within its implementation from the consumer. Intuitively, for X to be existential in T, X's identity cannot be known from any consumer; all that should be known is the set of operations provided at definition. There exists one type T for some type X.

In contrast, an universal type defines operations applicable to all types, from which the consumer is free to choose. The interface type T is exactly that. X is instantiated by the consumer, who'll know exactly which type X is. There exists a type T for every type X in the universe.

Existentials aren't actually present in Java as a language construct (except for in the limited case of wildcards (List)). But yes they can be emulated with interfaces. The problem then becomes more of design.

As ony pointed out, in an object-oriented setting, existentials become tricky to implement because the way you usually encode the type information of X (what you can do with it) is to have member functions in an interface type which X implements. In short, interfaces can buy some type abstraction capabilities, but require the elimination of the existential to some extent.