C++ Concepts as GADTs

I'm learning about GADTs in OCaml, and thinking about how one might be able to achieve the same kind of thing in C++. With C++ concepts, I think you can actually get pretty much all the way there.

GADTs

The canonical example of GADTs seems to be implementing a little embedded DSL, such that the embedded language's typechecking rules are checked by the embedding language's typechecker. Real World OCaml says this:

type _ value =
  | Int : int -> int value
  | Bool : bool -> bool value
type _ expr =
  | Value : 'a value -> 'a expr
  | Eq : int expr * int expr -> bool expr
  | Plus : int expr * int expr -> int expr
  | If : bool expr * 'a expr * 'a expr -> 'a expr

What it's saying here is that each type of node has a type parameter, indicating what type is returned from evaluating that node. So if you evaluate an Int node, the return type is int. An Eq node has two children, both of which have to evaluate to int when evaluated, and when the Eq node itself is evaluated, the result is bool. The If node is a bit interesting: its "then" child and its "else" child can return any type when evaluated, provided those two types are identical, and the result of the If node itself is that same type.

Normally, these kinds of type parameters would be represented by template parameters in C++, but in GADTs, it's flipped around: instead of the user of a parameterized type passing in a concrete type (whichever type the caller wants) as its parameter, in a GADT, the concrete type is passed out to the user, and the user has to deal with whichever type it ended up receiving.

So, in C++, the way you'd do this is with nested types, not templates, as such:

struct IntValue {
    using Result = int;
    int value;
};
struct BoolValue {
    using Result = bool;
    bool value;
};
template<typename LHS, typename RHS>
struct Eq {
    using Result = bool;
    std::shared_ptr<LHS> lhs;
    std::shared_ptr<RHS> rhs;
};
template<typename LHS, typename RHS>
struct Plus {
    using Result = int;
    std::shared_ptr<LHS> lhs;
    std::shared_ptr<RHS> rhs;
};
template<typename Condition, typename Then, typename Else>
struct If {
    using Result = Then::Result;
    std::shared_ptr<Condition> conditionExpr;
    std::shared_ptr<Then> thenExpr;
    std::shared_ptr<Else> elseExpr;
};

Note how all the structs have a nested Result type, indicating the same thing as the 'a type in the OCaml: the type of the result of the node, once it gets evaluated. Whichever code actually creates objects of these structs can determine the result type by saying typename Foo::Result. The result type is passed out rather than passed in.

Also, neither IntValue nor BoolValue are templated at all, because they don't need to be.

However, this C++ (so far) doesn't represent everything that the OCaml does - none of the nodes place any requirements on which types of children they can have. Eq : int expr * int expr -> bool expr means that the Eq node is only supposed to be able to have int nodes as children. So, we somehow want struct Eq's LHS and RHS template parameters to require that LHS::Result and RHS::Result are both int.

Concepts

This is where C++ concepts come in, as a way to constrain template parameters:

template<typename Expr, typename Result>
concept RequiredResult = std::is_same_v<typename Expr::Result, Result>;

template<typename LHS, typename RHS>
concept IdenticalResult = std::is_same_v<typename LHS::Result, typename RHS::Result>;

struct IntValue {
    using Result = int;
    int value;
};
struct BoolValue {
    using Result = bool;
    bool value;
};
template<RequiredResult<int> LHS, RequiredResult<int> RHS>
struct Eq {
    using Result = bool;
    std::shared_ptr<LHS> lhs;
    std::shared_ptr<RHS> rhs;
};
template<RequiredResult<int> LHS, RequiredResult<int> RHS>
struct Plus {
    using Result = int;
    std::shared_ptr<LHS> lhs;
    std::shared_ptr<RHS> rhs;
};
template<RequiredResult<bool> Condition, typename Then, typename Else>
requires IdenticalResult<Then, Else>
struct If {
    using Result = Then::Result;
    std::shared_ptr<Condition> conditionExpr;
    std::shared_ptr<Then> thenExpr;
    std::shared_ptr<Else> elseExpr;
};

So, we're able to describe "the child nodes must have a particular result type when evaluated, and, assuming they do, the result of my own node is Result." The requires syntax is even a way of indicating two types must be identical! How cool is that!

Evaluation

Alright, so how do we write an evaluation function for these things? Real World Ocaml has:

let eval_value : type a. a value -> a = function
  | Int x -> x
  | Bool x -> x;;
val eval_value : 'a value -> 'a = <fun>
let rec eval : type a. a expr -> a = function
  | Value v -> eval_value v
  | If (c, t, e) -> if eval c then eval t else eval e
  | Eq (x, y) -> eval x = eval y
  | Plus (x, y) -> eval x + eval y;;
val eval : 'a expr -> 'a = <fun>

The OCaml is pretty terse, but we can more-or-less transcribe it line by line into C++:

IntValue::Result eval(const IntValue& value) {
    return value.value;
}
BoolValue::Result eval(const BoolValue& value) {
    return value.value;
}
template<RequiredResult<int> LHS, RequiredResult<int> RHS>
Eq<LHS, RHS>::Result eval(const Eq<LHS, RHS>& value) {
    return eval(*value.lhs) == eval(*value.rhs);
}
template<RequiredResult<int> LHS, RequiredResult<int> RHS>
Plus<LHS, RHS>::Result eval(const Plus<LHS, RHS>& value) {
    return eval(*value.lhs) + eval(*value.rhs);
}
template<RequiredResult<bool> Condition, typename Then, typename Else>
requires IdenticalResult<Then, Else>
If<Condition, Then, Else>::Result eval(const If<Condition, Then, Else>& value) {
    return eval(*value.conditionExpr) ? eval(*value.thenExpr) : eval(*value.elseExpr);
}

And the OCaml example usage:

let i x = Value (Int x)
and b x = Value (Bool x)
and (+:) x y = Plus (x,y);;
val i : int -> int expr = <fun>
val b : bool -> bool expr = <fun>
val ( +: ) : int expr -> int expr -> int expr = <fun>
i 3;;
- : int expr = Value (Int 3)
b 3;;
Line 1, characters 3-4:
Error: This expression has type int but an expression was expected of type
         bool
i 3 +: i 6;;
- : int expr = Plus (Value (Int 3), Value (Int 6))
i 3 +: b false;;
Line 1, characters 8-15:
Error: This expression has type bool expr
       but an expression was expected of type int expr
       Type bool is not compatible with type int

with its corresponding C++:

auto i = [](int value) {
    return std::make_shared<IntValue>(IntValue{ value });
};
auto b = [](bool value) {
    return std::make_shared<BoolValue>(BoolValue{ value });
};
auto plus = []<RequiredResult<int> LHS, RequiredResult<int> RHS>(
    std::shared_ptr<LHS>&& lhs,
    std::shared_ptr<RHS>&& rhs) {
    return std::make_shared<Plus<LHS, RHS>>(Plus{
        .lhs = std::move(lhs),
        .rhs = std::move(rhs),
    });
};

std::cout << eval(*i(3)) << std::endl; // 3

//std::cout << eval(*b(3)) << std::endl;

/*

1>main.cpp(140,26): error C2220: the following warning is treated as an error

1>  (compiling source file '/main.cpp')

1>main.cpp(140,26): warning C4305: 'argument': truncation from 'int' to 'bool'

1>  (compiling source file '/main.cpp')

*/

std::cout << eval(*plus(i(3), i(6))) << std::endl; // 9

//std::cout << eval(*plus(i(3), b(false))) << std::endl;

/*

1>              main.cpp(39,8):

1>              'Plus': the associated constraints are not satisfied

1>                  main.cpp(38,35):

1>                  the concept 'RequiredResult<BoolValue,int>' evaluated to false

1>                      main.cpp(7,26):

1>                      the constraint was not satisfied

1>              main.cpp(39,8):

1>              see declaration of 'Plus'

*/

Pretty neat stuff!