Recently I saw a talk by one of active Idris contributors: David Christiansen - Coding for Types: The Universe Pattern in Idris where he shows some uses of dependent types. I'd like to use some of those examples to demonstrate that we actually have dependent types in D, or, really, in part of it. First let me show some original examples in Idris, a full blown depentently typed language, and then we'll translate them to D closely.

In the talk David says that in dependently typed languages we have types as first class values: you can create them on the fly, return from functions, store in data structures and pass around, however you shouldn't pattern-match on them because if we allow pattern-matching on types we lose free theorems (id may start to return 42 for all natural arguments) and this prevents proper type erasure when compiling the programs. I'm not sure if matching on types is actually banned in Idris now, I remember a few versions ago it actually worked, at least in simple cases. But sometimes doing different things depending on type passed is what we do want, and for this cases David describes what he calls The Universe Pattern: you take the types you wish to match on, encode them in a simple data type (as in AST), match on this data type, and when you need actual types use a mapping function from this encoding to actual types. For example, let's say we work with relational tables where each value can be either some text, an integer or a real number. We encode this with an algebraic data type:

data Column = TEXT | REAL | INTEGER

interpCol : Column -> Type
interpCol TEXT -> String
interpCol REAL -> Double
interpCol INTEGER -> Integer 

printCol : (c : Column) -> interpCol c -> String
printCol TEXT    x = x
printCol REAL    x = doubleToString x
printCol INTEGER x = intToString x  

Similarly David describes how to define a table schema and map it to an actual data type of one table row.

Table : Type
Table = List (String, Column)

interp : Table -> Type
interp tbl = HList (map (interpCol . snd) tbl) 

PeopleSchema : Table
PeopleSchema = [("Name", TEXT), ("Hamsters", INTEGER)]

People : List (interp PeopleSchema)
People = [["David", 1], ["Edwin", 0]]   

Now that we can map a table schema definition to a data type for its rows we can calculate total number of hamsters in this table and define a function for converting arbitrary table rows to strings.

countHamsters : List (interp PeopleSchema) -> Integer
countHamsters []             = 0
countHamsters ([_, h] :: xs) = h + countHamsters xs 

printRow : (tbl : Table) -> interp tbl -> String
printRow [] [] = "" 
printRow ((_, t) :: vs) (x :: xs) = printCol t x ++ "\t" ++ printRow vx xs 

Well, dependent types in Idris are not surprising, of course, being the key feature of the language. But did you know dependent types already got to mainstream being available in C++ and its younger brother D? Just not in whole language, only in half of it. We're used to thinking that D is a compiled language but it's also an interpreted language where the interpreter is built into the compiler and runs during the compilation stage, allowing CTFE (compile-time function execution) and many powerful metaprogramming features. Modern C++ also followed D in this direction. And at this interpreted stage we have real dependent types. Let's translate David's examples to D closely, to demonstrate the correspondence.

First, we had a data type Column encoding types of table cells, and its mapping to actual types.

enum Column { TEXT, REAL, INTEGER }

template interpCol(Column col) { // Column -> Type
    static if (col==Column.INTEGER) alias interpCol = int;     else
    static if (col==Column.REAL)    alias interpCol = double;  else
    static if (col==Column.TEXT)    alias interpCol = string;
}

string printCol(Column c, alias x)()    if (is(typeof(x) == interpCol!(c))) {
    static if (c==Column.TEXT) return x;
           else                return x.to!string;
}

The secret sauce here is two sets of parentheses after printCol: the arguments are listed inside the first pair of parentheses, this is where compile-time arguments are passed. The static if also does its job at compile time.

Now let's learn how to define table schemas, corresponding data and functions working with such tables. For compile-time lists there is a native D type TypeTuple (also known as AliasSeq starting from next compiler release), originally it appeared to define lists of compile-time arguments to templates, so it's heterogeneous and its elements can be types, numbers, strings, struct instances, other templates... virtually anything. The standard library contains functions for working with such lists - filter, map, reverse, etc. We're going to need map, it's called staticMap there. TypeTuple has one peculiarity: it flattens automatically, so a list of lists becomes just a single long list of all the elements. That's not what we want, so we'll make a wrapper:

struct List(Things...) { // compile-time HList
    alias contents = Things;
}

alias getType(x...) = typeof(x[0]);
alias listValueTypes(lst) = List!(staticMap!(getType, lst.contents));

struct NC(string A, Column B) { // named column
    alias name = A;
    alias col = B;
}

alias columnType(nc) = interpCol!(nc.col);
alias interp(tbl) = List!(staticMap!(columnType, tbl.contents));

string printRow(tbl, xs)()    if (is(listValueTypes!xs == interp!tbl)) {
    string[tbl.contents.length] res;
    foreach(i, x; xs.contents)
        res[i] = printCol!(tbl.contents[i].col, x);
    return res[].join("\t");
}

Definition of a particular table with hamsters and counting them will look like this:

alias PeopleSchema = List!( NC!("Name", Column.TEXT), NC!("Hamsters", Column.INTEGER) );

int countHamsters(rows...)() {
    int sum = 0;
    foreach(r; rows) {
        static assert(is(listValueTypes!r == interp!PeopleSchema));
        sum += r.contents[1];
    }
    return sum;
}

Let's run it on concrete data:

void main(string[] argv) {
    alias People = TypeTuple!( List!("David", 10), List!("Edwin", 11) );
    int n = countHamsters!People;
    string s = printRow!(PeopleSchema, People[0]);
    writeln("hamsters: ", n, ", first row: ", s);
}

In both Idris and D code above we had all the data in the source code but we didn't have to do it this way, we can define schema and data in a separate data file. In Idris we can use input-output to read the schema and data before processing. This is a fully dependently typed language where types can depend on values calculated in run-time. In D we can read the input and parse it at compile-time, there are ready means to do that (see Pegged library). All the interesting dependently-typed stuff happens at compile-time in D, but since this is where its interpreter is working, "compile-time" for ordinary D is "run-time" for the interpreted meta-programming part of D, and the types can depend on values there. We can use it as we would use Python or Ruby: just write "rdmd program.d arguments" and it will compile and run it in one go, so both stages (compile-time and run-time, interpeted D and compiled D) are executed together, and at least at one of the stages we have dependent types. Just like Idris, it may be not too practical but surely fun!

tags: programming