Three typing rules and the constructive truth

STLC.markdown

This is a type constructor

class FunctionType:
    def __init__(self, tyA, tyB):
        self.tyA = tyA
        self.tyB = tyB

    def __eq__(self, other):
        return self.tyA == other.tyA and self.tyB == other.tyB

    def __repr__(self):
        return "(" + self.tyA + " => " + self.tyB + ")"

This is a typing rule and evaluation rule

class Variable:
    def __init__(self, name):
        self.name = name

    def type_check(self, context):
        if self.name in context:
            return context[self.name]
        else:
            raise Exception("type error")

    def evaluate(self, env):
        return env[self.name]

This is another

class Application:
    def __init__(self, e1, e2):
        self.e1 = e1
        self.e2 = e2

    def type_check(self, context):
        ty1 = self.e1.type_check(context)
        ty2 = self.e2.type_check(context)
        if isinstance(ty1, FunctionType) and ty1.tyA == ty2:
            return ty1.tyB
        else:
            raise Exception("type error")

    def evaluate(self, env):
        return self.e1.evaluate(env)(self.e2.evaluate(env))

This is a third

class Abstraction:
    def __init__(self, x, x_ty, e):
        self.x    = x
        self.x_ty = x_ty
        self.e    = e

    def type_check(self, context):
        context = context.copy()
        context[self.x] = self.x_ty
        ty = self.e.type_check(context)
        return FunctionType(self.x_ty, ty)

    def evaluate(self, env):
        def closure(x):
            env_inner = env.copy()
            env_inner[self.x] = x
            return self.e.evaluate(env_inner)
        return closure

Now form a programming language

http://static.tvtropes.org/pmwiki/pub/images/three-chordsimg-350px_3540.jpg