Template Meta なんちゃら

TypeLevel.cpp

// >=gcc-4.7
#include <iostream>
#include <type_traits>

// Universes
template < unsigned int Level >
struct Set {
    typedef Set< 1 + Level > type;
    typedef Set< Level > value;
    static const unsigned int level = Level;
};

// data ⊥ : Set where
struct Bottom {
    typedef Set< 0 > type;
    typedef Bottom value;
    // no constructor
};

// record ⊤ : Set where
//   constructor tt
struct Top {
    typedef Set< 0 > type;
    typedef Top value;
    struct tt {
        typedef Top type;
        typedef tt value;
    };
};

// data _≡_ {a} {A : Set a} (x : A) : A → Set a where
//   refl : x ≡ x
template < typename X >
struct PropositionalEquality {
    typedef Set< 1 + X::type::type::level > type;
    template < typename Y, bool Dummy = std::is_same< typename X::value, typename Y::value >::value >
    struct _Equal;
    template < typename Y > using Equal = _Equal< Y >;
    template < typename Y >
    struct _Equal< Y, false > {
        typedef Set< X::type::type::level > type;
    };
    template < typename Y >
    struct _Equal< Y, true > {
        typedef Set< X::type::type::level > type;
        typedef _Equal< X > value;
        struct Refl {
            typedef PropositionalEquality< X >::Equal< Y > type;
            typedef Refl value;
        };
    };
};

// sym : {a : Level} {A : Set a} {i j : A} → i ≡ j → j ≡ i
// sym = refl
template < typename A, typename B, typename AeqB >
struct Sym {
    typedef typename PropositionalEquality< B >::template Equal< A > type;
    typedef AeqB value;
    typedef typename std::enable_if< std::is_same< typename PropositionalEquality< A >::template Equal< B >, typename AeqB::type >::value >::type _AeqB;
};

// trans : {a : Level} {A : Set a} {i j k : A} → i ≡ j → j ≡ k → i ≡ k
// trans refl eq = eq
template < typename A, typename B, typename C, typename AeqB, typename BeqC >
struct Trans {
    typedef typename PropositionalEquality< A >::template Equal< C > type;
    typedef AeqB value;
    typedef typename std::enable_if< std::is_same< typename PropositionalEquality< A >::template Equal< B >, typename AeqB::type >::value >::type _AeqB;
    typedef typename std::enable_if< std::is_same< typename PropositionalEquality< B >::template Equal< C >, typename BeqC::type >::value >::type _BeqC;
};

template < typename A, typename B, template < typename X > class P, typename AeqB >
struct Cong {
    typedef typename PropositionalEquality< P< A > >::template Equal< P< B > > type;
    typedef typename PropositionalEquality< P< A > >::template Equal< P< A > >::Refl::value value;
    typedef typename std::enable_if< std::is_same< typename PropositionalEquality< A >::template Equal< B >, typename AeqB::type >::value >::type _AeqB;
};

template < typename A, typename B, template < typename X > class P, typename PA, typename AeqB >
struct Subst {
    typedef typename PropositionalEquality< P< A > >::template Equal< P< B > > type;
    typedef typename PropositionalEquality< P< A > >::template Equal< P< B > >::Refl value;
    typedef typename std::enable_if< std::is_same< P< A >, typename PA::type >::value >::type _PAisPA;
    typedef typename std::enable_if< std::is_same< typename PropositionalEquality< A >::template Equal< B >, typename AeqB::type >::value >::type _AeqB;
};

// ¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
// ¬ P = P → ⊥
template < typename P >
struct Not {
    typedef typename P::type type;
    template < typename X >
    struct PtoBottom {
        typedef Bottom::type type;
        typedef Bottom value;
        typedef typename std::enable_if< std::is_same< P, X >::value >::type XisP;
    };
    template < typename X > using value = PtoBottom< X >;
};

// ⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever
// ⊥-elim ()
template < typename P, typename B >
struct Bottom_elimination {
    typedef typename P::type type;
    typedef typename P::value value;
    typedef typename std::enable_if< std::is_same< Bottom, typename B::type >::value >::type BisBottom;
};

// data ℕ : Set where
//   zero : ℕ
//   suc  : (n : ℕ) → ℕ
struct Nat {
    typedef Set< 0 > type;
    typedef Nat value;
    struct Zero {
        typedef Nat type;
        typedef Zero value;
        static const unsigned int eval = 0;
    };
    template < typename N >
    struct Suc {
        typedef Nat type;
        typedef Suc< typename N::value > value;
        typedef typename std::enable_if< std::is_same< Nat, typename N::type >::value >::type NisNat;
        static const unsigned int eval = 1 + N::eval;
    };
};

// data Bool : Set where
//   true  : Bool
//   false : Bool
struct Bool {
    typedef Set< 0 > type;
    typedef Bool value;
    struct True {
        typedef Bool type;
        typedef True value;
    };
    struct False {
        typedef Bool type;
        typedef False value;
    };
};

// add : Nat -> Nat -> Nat
// add 0 b = b
// add (suc a) b = suc (add a b)
template < typename A, typename B >
struct add { // eval
    typedef Nat type;
    typedef typename add< typename A::value, B >::value value;
    static const unsigned int eval = value::eval;
};
template < typename B >
struct add < Nat::Zero, B > { // add 0 b
    typedef Nat type;
    typedef typename B::value value;
    static const unsigned int eval = value::eval;
};
template < typename A, typename B >
struct add < Nat::Suc< A >, B > { // add (suc a) b
    typedef Nat type;
    typedef Nat::Suc< typename add< A, B >::value > value;
    static const unsigned int eval = value::eval;
};

// fib : Nat -> Nat
// fib 0 = 1
// fib 1 = 1
// fib (suc (suc n)) = add (fib (suc n)) (fib n)
template < typename N >
struct fib { // eval
    typedef Nat type;
    typedef typename fib< typename N::value >::value value;
    static const unsigned int eval = value::eval;
};
template <>
struct fib< Nat::Zero > { // fib 0
    typedef Nat type;
    typedef Nat::Suc< Nat::Zero > value;
    static const unsigned int eval = value::eval;
};
template <>
struct fib< Nat::Suc< Nat::Zero > > { // fib 1
    typedef Nat type;
    typedef Nat::Suc< Nat::Zero > value;
    static const unsigned int eval = value::eval;
};
template < typename N >
struct fib< Nat::Suc< Nat::Suc< N > > > { // fib (suc (suc n))
    typedef Nat type;
    typedef typename add< fib< Nat::Suc< N > >, fib< N > >::value value;
    static const unsigned int eval = value::eval;
};

template < typename A, typename N >
class Vec {};
// nil
template < typename A >
class Vec< A, Nat::Zero > {
public:
    Vec() {}
};
// cons
template < typename A, typename N >
class Vec< A, Nat::Suc< N > > {
public:
    Vec< A, Nat::Suc< N > >(const A& x, const Vec< A, N >& xs ) : x(x), xs(xs) {}
    A head() const { return x; }
    Vec< A, N > tail() const { return xs; }
private:
    const A x;
    const Vec< A, N > xs;
};

template < typename A, typename N >
Vec< A, Nat::Suc< N > > cons( const A& x, const Vec< A, N >& xs) {
    return Vec< A, Nat::Suc< N > >(x, xs);
}

template < typename N >
struct Zero_is_left_identity;
template <>
struct Zero_is_left_identity< Nat::Zero > {
public:
    typedef typename PropositionalEquality< add< Nat::Zero, Nat::Zero > >::Equal< Nat::Zero > type;
    typedef typename PropositionalEquality< add< Nat::Zero, Nat::Zero > >::Equal< Nat::Zero >::Refl::value value;
};
template < typename N >
struct Zero_is_left_identity< Nat::Suc< N > > {
public:
    typedef typename PropositionalEquality< add< Nat::Zero, Nat::Suc< N > > >::template Equal< Nat::Suc< N > > type;
    typedef typename PropositionalEquality< add< Nat::Zero, Nat::Suc< N > > >::template Equal< Nat::Suc< N > >::Refl::value value;
};

// template < typename N >
// struct Zero_is_right_identity;
// template <>
// struct Zero_is_right_identity< Nat::Zero > {
// public:
//     typedef typename PropositionalEquality< add< Nat::Zero, Nat::Zero > >::Equal< Nat::Zero > type;
//     typedef typename PropositionalEquality< add< Nat::Zero, Nat::Zero > >::Equal< Nat::Zero >::Refl::value value;
// };
// template < typename N >
// struct Zero_is_right_identity< Nat::Suc< N > > {
// public:
//     typedef typename PropositionalEquality< add< Nat::Suc< N >, Nat::Zero > >::template Equal< Nat::Suc< N > > type;
//     typedef typename Cong< add< N, Nat::Zero >, N, Nat::Suc, typename Zero_is_right_identity< N >::value >::value value;
// };

template < typename A, typename B, typename C >
struct plus_assoc;
template < typename B, typename C >
struct plus_assoc< Nat::Zero, B, C > {
    typedef typename PropositionalEquality< add< add< Nat::Zero, B >, C > >::template Equal< add< Nat::Zero, add< B, C > > > type;
    typedef typename PropositionalEquality< add< B, C > >::template Equal< add< B, C > >::Refl value;
};

template < unsigned int n >
struct _Nat { using type = Nat::Suc< typename _Nat< n-1 >::type >; };
template <>
struct _Nat< 0 > { using type = Nat::Zero; };
template < unsigned int n >
using N = typename _Nat< n >::type;

int main ()
{
    std::cout << N< 0 >::eval << std::endl;
    std::cout << N< 1 >::eval << std::endl;
    std::cout << N< 2 >::eval << std::endl;

    std::cout << add< N< 2 >, N< 2 > >::eval << std::endl;

    std::cout << fib< N< 0 > >::eval << std::endl;
    std::cout << fib< N< 1 > >::eval << std::endl;
    std::cout << fib< N< 2 > >::eval << std::endl;
    std::cout << fib< N< 3 > >::eval << std::endl;
    std::cout << fib< N< 4 > >::eval << std::endl;

    // p :  0 ≡ 0
    PropositionalEquality< N< 0 > >::Equal< N< 0 > >::Refl::value refl0 = refl0;
    // p :  0 ≡ 1
    // PropositionalEquality< N< 0 > >::Equal< N< 1 > >::Refl::value refl1 = refl1;
    // p :  1 ≡ 0
    // PropositionalEquality< N< 1 > >::Equal< N< 0 > >::Refl::value refl2 = refl2;
    // p :  1 ≡ 1
    PropositionalEquality< N< 1 > >::Equal< N< 1 > >::Refl::value refl3 = refl3;

    // p :  0 + 1 ≡ 1
    PropositionalEquality< add< N< 0 > , N< 1 > > >::Equal< N< 1 > >::Refl::value refl_id_l = refl_id_l;
    Zero_is_left_identity< N< 1 > >::value left_id0 = left_id0;
    // p :  1 + 0 ≡ 1
    // PropositionalEquality< add< N< 1 > , N< 0 > > >::Equal< N< 1 > >::Refl::value refl_id_r = refl_id_r;
    // Zero_is_right_identity< N< 1 > >::value right_id0 = refl_id_r;

    // p :  1 ≡ 0 + 1
    Sym< add< N< 0 >, N< 1 > >, N< 1 >, Zero_is_left_identity< N< 1 > > >::value sym_refl_l = sym_refl_l;
    // p :  1 ≡ 1 + 0
    // Sym< add< N< 1 >, N< 0 > >, N< 1 >, Zero_is_right_identity< N< 1 > > >::value sym_refl_r = sym_refl_r;

    PropositionalEquality< fib< N< 4 > > >::Equal< N< 5 > >::Refl::value refl8 = refl8;

    Vec< int, N< 0 > > nil;
    Vec< int, N< 2 > > xs(cons(2, (cons(1, nil))));
    xs.tail().tail();
    // xs.tail().tail().tail(); // compile error
    return 0;
}