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 `int`

s 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`

`int`

s.

We can actually write up a `foldl`

for this case. First we declare the type of a generic function (we have to use `struct`

s 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 `typedef`

ing 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`

`typedef`

ed iff `Lt<P(A), P(B)>`

has it `typedef`

ed. 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

Nice post! I want just to warning that your blog doesn’t escape ” characters in source code and all the template argument lists are not visible. Bye, Nicola

Look, it happened in my comment, too 😛 It doesn’t escape ‘<‘ and ‘>’ characters 😉

you have an open ‘a’ tag just before ‘I was surprised how close C++ can get to Haskell at this point.’

WordPress ate your syntax.

I thought this was interesting (I found it when trying to google to find if c++ could sorta do sigma types), and, seeing that there weren’t any comments after , almost 4 years now at the time that I found this, that I should say that I enjoyed this blog post, and it is interesting, etc.

Thanks!

(though, maybe the reason for no other comments is just because you didn’t approve any? I don’t know. That doesn’t really change my reason for commenting though.)

Hi drocta,

This is a old backed up version of my blog (so I don’t check in often to see if there are comments I need to approve etc.). My current blog is at http://playingwithpointers.com

Thanks for dropping by!

— Sanjoy