gadt.py

# Attempt to mimick following GADT (Generalized algebraic data type) in Python:
#
# data Expr a where
#     Const :: a  -> Expr a
#     Add :: Expr Int -> Expr Int -> Expr Int
#     Eq :: Expr Int -> Expr Int -> Expr Bool
#     IfThenElse :: Expr Bool -> Expr a -> Expr a -> Expr a

import abc
from typing import Generic, TypeVar


A = TypeVar('A')


class Expr(Generic[A], metaclass=abc.ABCMeta):
    pass


class Const(Expr[A]):
    def __init__(self, value: A):
        self._value = value

    @property
    def value(self) -> A:
        return self._value


class Add(Expr[int]):
    def __init__(self, left: Expr[int], right: Expr[int]):
        self._left = left
        self._right = right

    @property
    def left(self) -> Expr[int]:
        return self._left

    @property
    def right(self) -> Expr[int]:
        return self._right


class Eq(Expr[bool]):
    def __init__(self, left: Expr[int], right: Expr[int]):
        self._left = left
        self._right = right

    @property
    def left(self) -> Expr[int]:
        return self._left

    @property
    def right(self) -> Expr[int]:
        return self._right


class IfThenElse(Expr[A]):
    def __init__(self, condition: Expr[bool],
                 then_expr: Expr[A], else_expr: Expr[A]):
        self._condition = condition
        self._then_expr = then_expr
        self._else_expr = else_expr

    @property
    def condition(self) -> Expr[bool]:
        return self._condition

    @property
    def then_expr(self) -> Expr[A]:
        return self._then_expr

    @property
    def else_expr(self) -> Expr[A]:
        return self._else_expr


def eval(e: Expr[A]) -> A:
    if isinstance(e, Const):
        # reveal_type(e)  # => note: Revealed type is 'gadt.Const[Any]'
        return e.value
    elif isinstance(e, Add):
        # reveal_type(e)  # => note: Revealed type is '<nothing>'
        return eval(e.left) + eval(e.right)
        # error: <nothing> has no attribute "left"
        # error: <nothing> has no attribute "right"
    elif isinstance(e, Eq):
        # reveal_type(e)  # => note: Revealed type is '<nothing>'
        return eval(e.left) == eval(e.right)
        # error: <nothing> has no attribute "left"
        # error: <nothing> has no attribute "right"
    elif isinstance(e, IfThenElse):
        # reveal_type(e)  # => note: Revealed type is 'gadt.IfThenElse[Any]'
        return eval(e.then_expr) if eval(e.condition) else eval(e.else_expr)
    else:
        assert False


example = IfThenElse[str](
    Eq(Add(Const[int](2), Const[int](1)), Const[int](0)),
    Const[str]("foo"),
    Const[str]("bar")
)
# reveal_type(example)
# # =>  note: Revealed type is 'gadt.IfThenElse[builtins.str*]'
print(eval(example))