Terms are not types, but could I have Type be a subclass of Term in my OOP / C++ dependent type hierarchy?

Question

Here's the code so far in "Type.h".

#pragma once

#include "Term.h"
#include <string>

class Type
{
public:
    Type() {
        typeName = "Anonymous";
    }
    Type(const std::string& typeName) 
    {
        this->typeName = typeName;
    }
    Type(const Type& source) 
    {
        typeName = source.typeName;
    }
    virtual ~Type();
    virtual std::string toString() const { return typeName;  }

protected:
    std::string typeName;
};

class DependentType : Type
{
public:
    DependentType(const Term& x, const Type& A, const std::string& typeName) : Type(typeName)
    {
        *term = x;
        *type = A;
    }

    virtual Type* operator () (const Term& x) = 0;

    std::string toString() const {
        return Type::toString() + ":" + type->toString() + "→" + "Universe";
    }

protected:
    Term* term;
    Type* type;
};

class PiType : public DependentType
{

};

There's this definition of dependent types on Wikipedia: https://en.wikipedia.org/wiki/Dependent_type#Formal_definition

But if a dependent type is defined to be loosely a family of types $B : A \to \mathcal{U}$ the universe, then I thought that only terms can go on the LHS of $:$ in $B(x) : \mathcal{U}$. If not, then I would need several typing judgements which seems bad on the code re-use side of things. Howe should I code it?

I'm guessing it's safe here to let Type subclass (derive from / inherit) Term as a base class. Is that right?

Answer 1

Have been coding from the book. Here is a sample:

SimplyTypedLambdaCalculus::SimplyTypedLambdaCalculus(const Type* baseType)
{
    auto base_type = IsType(baseType);
    baseTypeIntro = InferenceRule({}, base_type);

    // Doing it like the below has two advantages:
    // 1. Each InferenceRule already makes copies that it owns (on the Heap), so this avoids doubling the heap allocs.
    // 2. Line-by-lines are great for debugging purposes.  To inspect each variable etc.

    auto A_type = IsType(A);
    auto B_type = IsType(B);
    auto AxB = Product(A, B);
    auto AxB_type = IsType(AxB);
    auto AtoB = Function(A, B);
    auto AtoB_type = IsType(AtoB);

    productTypeIntro = InferenceRule({ &A_type, &B_type }, AxB_type);
    functionTypeIntro = InferenceRule({ &A_type, &B_type }, AtoB_type);

    addInferenceRules({ &baseTypeIntro, &productTypeIntro, &functionTypeIntro });
}

The code is private, however.