An even smaller type system in Python

typesys2.py

# Types and type constructors
# flake8: noqa

from __future__ import annotations


class TypeConstructor:
    def __init__(
        self, parameters: list[TypeParameter], super_: Instance | BottomType
    ) -> None:
        self.parameters = parameters
        self.super = super_

    def __eq__(self, other):
        if not isinstance(other, TypeConstructor):
            return NotImplemented
        return self is other

    def parents(self) -> list[Type]:
        result: list[Type] = []
        current = self.super
        while True:
            if isinstance(current, BottomType):
                break
            result.append(current)
            current = current.type_constructor.super
        return result


class TypeParameter:
    def __init__(self, constraint: Constraint, bound: Type) -> None:
        self.constraint = constraint
        self.bound = bound

    def __eq__(self, other):
        if not isinstance(other, TypeParameter):
            return NotImplemented
        return self.constraint == other.constraint and self.bound == other.bound


class Constraint:
    def satisfies(self, left: Type, right: Type) -> bool:
        raise NotImplementedError()


class InvariantConstraint(Constraint):
    def satisfies(self, left: Type, right: Type) -> bool:
        return left == right

    def __eq__(self, other):
        if not isinstance(other, Constraint):
            return NotImplemented
        return isinstance(other, InvariantConstraint)


class ContravariantConstraint(Constraint):
    def satisfies(self, left: Type, right: Type) -> bool:
        return left == right or right.is_supertype_of(left)

    def __eq__(self, other):
        if not isinstance(other, Constraint):
            return NotImplemented
        return isinstance(other, ContravariantConstraint)


class CovariantConstraint(Constraint):
    def satisfies(self, left: Type, right: Type) -> bool:
        return left == right or left.is_supertype_of(right)

    def __eq__(self, other):
        if not isinstance(other, Constraint):
            return NotImplemented
        return isinstance(other, CovariantConstraint)


class Type:
    def is_supertype_of(self, other: Type) -> bool:
        raise NotImplementedError()


class BottomType(Type):
    def is_supertype_of(self, other: Type) -> bool:
        return True

    def __eq__(self, other):
        if not isinstance(other, Type):
            return NotImplemented
        return isinstance(other, BottomType)


class TopType(Type):
    def is_supertype_of(self, other: Type) -> bool:
        return False

    def __eq__(self, other):
        if not isinstance(other, Type):
            return NotImplemented
        return isinstance(other, TopType)


class TypeVariable(Type):
    def __init__(self, constraint: Constraint, bound: Type) -> None:
        self.constraint = constraint
        self.bound = bound

    def is_supertype_of(self, other: Type) -> bool:
        # If this variable is a covariant type parameter, it could be its bound
        # or any subtype of its bound.
        # If it's a contravariant type parameter, it could be its bound or any
        # supertype of its bound.
        # Therefore, this variable "is a supertype" (i.e. `other` is compatible
        # with it) if `other` satisfies the constraint relative to the bound.
        # (I think)
        return self.constraint.satisfies(self.bound, other)

    def __eq__(self, other):
        if not isinstance(other, Type):
            return NotImplemented
        elif not isinstance(other, TypeVariable):
            return False
        return self.constraint == other.constraint and self.bound == other.bound


class Instance(Type):
    def __init__(
        self, type_constructor: TypeConstructor, arguments: list[Type]
    ) -> None:
        self.type_constructor = type_constructor
        self.arguments = arguments

    def is_supertype_of(self, other: Type) -> bool:
        if not isinstance(other, Instance) or self == other:
            return False
        if self.type_constructor == other.type_constructor:
            return all(
                p.constraint.satisfies(l, r)
                for p, l, r in zip(
                    self.type_constructor.parameters, self.arguments, other.arguments
                )
            )
        for parent in other.type_constructor.parents():
            if self == parent or self.is_supertype_of(parent):
                return True
        return False

    def __eq__(self, other):
        if not isinstance(other, Type):
            return NotImplemented
        elif not isinstance(other, Instance):
            return False
        return (
            self.type_constructor == other.type_constructor
            and self.arguments == other.arguments
        )


# Tests

bottom = BottomType()
top = TopType()
object_instance = Instance(TypeConstructor([], bottom), [])

A = TypeConstructor([], object_instance)
B = TypeConstructor([], Instance(A, []))

# Invariant type parameter
C = TypeConstructor([TypeParameter(InvariantConstraint(), bottom)], object_instance)
assert not Instance(C, [Instance(A, [])]).is_supertype_of(Instance(C, [Instance(B, [])]))
assert not Instance(C, [Instance(B, [])]).is_supertype_of(Instance(C, [Instance(A, [])]))
assert Instance(C, [Instance(A, [])]) == Instance(C, [Instance(A, [])])

# Covariant type parameter
D = TypeConstructor([TypeParameter(CovariantConstraint(), bottom)], object_instance)
assert Instance(D, [Instance(A, [])]).is_supertype_of(Instance(D, [Instance(B, [])]))
assert not Instance(D, [Instance(B, [])]).is_supertype_of(Instance(D, [Instance(A, [])]))

# Contravariant type parameter
E = TypeConstructor([TypeParameter(ContravariantConstraint(), bottom)], object_instance)
assert Instance(E, [Instance(B, [])]).is_supertype_of(Instance(E, [Instance(A, [])]))
assert not Instance(E, [Instance(A, [])]).is_supertype_of(Instance(E, [Instance(B, [])]))

# Type constructor for all binary functions
function2 = TypeConstructor(
    [
        TypeParameter(ContravariantConstraint(), bottom),
        TypeParameter(ContravariantConstraint(), bottom),
        TypeParameter(CovariantConstraint(), top),
    ],
    bottom,
)

function_type = Instance(
    function2,
    [
        Instance(A, []),
        Instance(B, []),
        object_instance,
    ],
)

assert function_type.is_supertype_of(
    Instance(
        function2,
        [
            object_instance,
            Instance(A, []),
            Instance(B, []),
        ],
    )
)

I got top and bottom backwards, huh