Dualing Types

The Curry-Howard correspondence was the original insight into the relationship between typed programming languages and intuitionistic logics. At a high level this relationship associates types with propositions, and this connection allows understanding programming from the perspective of logic and vice versa. Thinking about programming in this context can often be used to help establish an intuition for the rules of a type system and to provide a more fundamental basis for reasoning about many features and design patterns present in common programming languages. One practical application of this is that it allows constructing one programming language feature in terms of others, which is useful when the feature being constructed isn't built-in to the language.

Implication, Conjunction, Disjunction

The standard logical connectives for forming propositions are implication, conjunction, and disjunction. These relate to programming language types as functions, pairs, and sums:

But it still may not be easy to see how pairs and sums relate to most programming languages. The reason has to do with how they are indexed: while pairs and sums are indexed positionally, most programming languages use labels for indexing, resulting in records and variants, respectively. Object-oriented languages often extend records with additional capabilities and call them 'classes' or 'interfaces', and functional languages extend variants with extra capabilities compared to sums, but for our purposes these distinctions hardly matter; what matters is that you can think of a definition like: 

class Pair { public int fst; public String snd; }

as a type representing the conjunction of all of its fields, indexed by the field names. Similarly, a definition like: 

type sum = Left of int | Right of string

can be thought of as a type representing a disjunction of its cases, indexed by the constructors.

Encoding Sums

While almost every programming language has functions and pairs in one form or another, many of the most popular programming languages lack sum types as a direct feature. However, it turns out that with a little manipulation it is often possible to encode them using other features of a language. Let's use Java as an example of a language without built-in sum types, and figure out how to implement them in it. We can use this logical equivalence as a guide: 

(A \/ B) <-> (forall T, ((A -> T) /\ (B -> T)) -> T)

The forall T corresponds to universal quantification over types, which translates into generics in Java. So we can represent sums in terms of generics, functions, and pairs. If A = Integer and B = String, the Java translation of the right side of the above formula is: 

abstract class Sum {
  public abstract <T>
  T select(Function<Integer,T> fst, Function<String,T> snd);
}

And we need two different implementations corresponding to the two constructors of the sum - one constructed with an integer that selects the first function, and another constructed with a string that selects the second function: 

class InjectLeft extends Sum {
  private final Integer i;
  public InjectLeft(Integer i) { this.i = i; }
  public <T>
  T select(Function<Integer,T> fst, Function<String,T> snd) {
    return fst.apply(i);
  }
}

class InjectRight extends Sum {
  private final String s;
  public InjectRight(String s) { this.s = s; }
  public <T>
  T select(Function<Integer,T> fst, Function<String,T> snd) {
    return snd.apply(s);
  }
}

This pattern can be extended beyond just two cases, and at that point it might make sense to capture the operations that are performed on the values of the sum in a single type rather than as individual parameters to the selection method. The standard name for such a type is the 'Visitor', and the standard name for the pattern as a whole is the 'Visitor Pattern'. The select method is usually named 'accept' when following this pattern.

Existentials

Existential types provide an interface that hides a type variable, restricting uses of values with that type to what the interface allows. While universal types (formed with parametric polymorphism or generics) allow users to instantiate with any type but require implementers to treat the type parameter as opaque, existential types allow implementers to instantiate with any type but require users to treat the type parameter as opaque. In order to encode such types in Java we can use the following logical equivalence: 

(exists T, X<T>) <-> (forall R, (forall T, X<T> -> R) -> R)

And for the sample interface we'll use: 

interface X<T> {
  public T hd();
  public X<T> tl();
  public String printVal(T t);
}

When used existentially, this interface only allows retrieving a value with hd, generating a new instance of the interface with tl, and converting a value into a string with printVal. Here is the Java translation of the right side of the above formula: 

interface ExistentialOperation<R> {
  public abstract <T>
  R apply(X<T> x);
}

interface ExistentialX {
  public abstract <R>
  R applyOp(ExistentialOperation<R> op);
}

Here are some example implementations of the interface: 

class XString implements X<String>, ExistentialX {
  public XString() {}
  public String hd() { return "XString"; }
  public X<String> tl() { return this; }
  public String printVal(String s) { return s; }
  public <R>
  R applyOp(ExistentialOperation<R> op) { return op.apply(this); }
}

class XIntCounter implements X<Integer>, ExistentialX {
  private final Integer count;
  public XIntCounter() { this.count = 0; }
  private XIntCounter(int count) { this.count = count; }
  public Integer hd() { return count; }
  public X<Integer> tl() { return new XIntCounter(count+1); }
  public String printVal(Integer count) { return Integer.toString(count); }
  public <R>
  R applyOp(ExistentialOperation<R> op) { return op.apply(this); }
}

And here is an operation that treats the interface existentially: 

class UseExistentialX implements ExistentialOperation<String> {
  public UseExistentialX() {}
  public <T>
  String apply(X<T> x) {
    T t = x.tl().tl().tl().hd();
    return x.printVal(t);
  }
}

It is important to note that the operation is unable to make assumptions about the type that the interface is instantiated with - it must treat the type parameter as opaque.