Faking Dependent Types in C++

It is possible to have some kind of dependent typing in C++ using templates. The “solution” isn’t elegant or usable, but I found it mildly interesting so I’ll try to explain it here. The C++ type system with templates is Turing complete, so that something like this can be done shouldn’t be a surprise. The entire source file is here [1].

We will need to convert ints to types and vice versa (we’ll soon see why), so we might as well get that out of the way. One way to convert an int to a type is by exploiting the fact that templates are allowed to take integral values as parameters:

template
struct Integer {
}

typedef Integer Zero;
typedef Integer One;

// ... and so on

The issue with this is the lack of control over the types we’re producing. In this particular case, we want to prevent (at compile time) the creation of types corresponding to negative integers. We do this by following Peano’s definition of natural numbers:

template
struct S { typedef T Previous;
  enum { ToInt = T::ToInt + 1 };
};

struct Z { enum { ToInt = 0 }; };

template
struct ToType {
  typedef S<typename ToType::TypeValue > TypeValue;
};

template
struct ToType {
  typedef Z TypeValue;
};

#define P(n) typename n::Previous
#define TO_INT(n) n::ToInt

In this case, S<S<S<Z > > > represents 3 and it is obvious that using S and Z, it is possible to enumerate only positive integers.

Secondly, we want some mechanism which to use to “lift” normal integers into a corresponding type. This is done by ToType. The recursion is simple, for 0, ToType “returns” Z and for N, it “returns” S< the “return value” of ToType<N - 1> >. P and TO_INT are macros to save typing.

Note that we’ve not really solved the problem of creation of negative integers — ToType<-50>::TypeValue will throw a “template depth exceeds maximum of XYZ” error and not a proper compile time error. All this mechanism does is isolate the issue of negative numbers to within ToType so that the rest of the code can work with a cleaner representation. I think this can be improved:

• Create a dummy struct ZeroFlag with one int template paramenter.
• Specialize ZeroFlag on 0 and add a static field DummyF to it.
• Create a struct Abs that computes the absolute value of its int template parameter.
• Add typedef ZeroFlag<Abs<N>::Value >::DummyF to ToType.

This should give a compile time error on instantiating ToType<0>. However, right now, we concentrate elsewhere. Importantly, check the Previous typedef in struct S, which isn’t present when we specialize in struct Z — Previous will be our main weapon in generating compile time errors, as we shall see.

We now create a “linked list” which keeps track of the number of nodes in it at compile time:

// N denotes the size of the list here
template
struct List {
  T data;
  List next;
};

template
struct List {
};

We don’t need to have a pointer to a node since the next field always points to a smaller type — there is no circularity (and hence no possibility of a loop in the linked list). I’m not exactly sure of this, but I think, at least in terms of memory layout, List<100> should be equivalent to an array of 100 ints.

We can actually write up a foldl for this case. First we declare the type of a generic function (we have to use structs everywhere because C++ does not allow partial template specialization on functions):

template
struct Func2 {
  typedef C functionType(A, B);
};

Now, to fold a type T, we need a function of type A->T->A and an initial value of type A:

template
struct List {
  T data;
  List next;

  template
  A foldl(typename Func2::functionType f, A a) {
    return next.foldl(f, f(a, data));
  }
};

template
struct List {
  template
  A foldl(typename Func2::functionType f, A a) {
    return a;
  }
};

I was surprised how close C++ can get to Haskell at this point.

Right now we have a dependently typed (only in a loose sense of the term — I’ve not had enough rigour with type systems to formally claim this) linked list in C++. We can now write a “safe” sorting function using this:

(I’ve used a shitty algorithm here to focus on the things this post is actually supposed to focus on.)

template
struct Sorter {
  static void sort(List &list) {
    List rest = list.next;
    Sorter::sort(rest);
    if (list.data > rest.data) {
      std::swap(rest.data, list.data);
      Sorter::sort(rest);
    }
    list.next = rest;
  }
};

// List of length 1 is already sorted.
template
struct Sorter<t, S > {
  static void sort(List<t, S > &list) { };
};

The cute part about this code is, if the specialization Sorter<T, S<Z> > is removed you get a compile time error, since the compiler tries to sort a list of on element using the general template which then tries to sort a list of zero elements. Since the general template tries to access the Previous field (via the P macro), you get a compile time error. That the code compiles is “proof” that your algorithm will not try to walk the past of an empty linked list.

It is easy to create a struct ListCreator which creates a linked list of a specified length and printing is a matter of folding with the function

template
std::vector accumulate(std::vector in, T t) {
  in.push_back(t);
  return in;
}

and an empty std::vector and print the resulting vector. The exact code is in [1].

The entire list, the sorting function could all be implemented inside the template system, by the way. However, in that case the elements of the list would all be baked in; in the present situation, we have the option of reading (a compile-time-constant obviously) number of entries from a file or from the user. I think more interesting applications will be seen in “lifting” a partial amount of data and algorithms into the type system, providing a fuzzier boundary between what programmers have to keep in their heads and what the type system proves for them.

For dessert, let’s see how you can implement compile-time bound checking on the list. First a template to assert the less-than relation:

template<typename A, typename B>
struct Lt {
  typedef typename Lt<P(A), P(B)>::Flag Flag;
};

template<typename B>
struct Lt<Z, S<B> > {
  typedef bool Flag;
};

Essentially A < B iff Lt<A, B>::Flag exists. The non-existence of Flag can be made a compile-time error by typedefing it in the template which requires the relation to be valid. So, in this case, Z is less than all integers which can be written as S<A> for some A and A is less than B iff A - 1 is less than B - 1. Notice that these two axioms are both necessary and sufficient for comparing any two positive integers. Also note how we are inductively asserting in the general case — since we typedef Lt<P(A), P(B)>::Flag to Flag, Lt<A, B> will have Flag typedefed iff Lt<P(A), P(B)> has it typedefed. Stating a correct indexing operation is now trivial:

template
struct Idx {
  typedef typename Lt::Flag Flag;
  static T idx(List list) {
    return list.data;
  }
};

—

[1] https://github.com/sanjoy/Snippets/blob/master/DependentTypes.cc

Advertisements