Skip to content

Instantly share code, notes, and snippets.

@msakai
Last active Dec 31, 2019
Embed
What would you like to do?
# Encoding existential types in Python using ∃X. F(X) ≅ ∀R. (∀X. F(X) → R) → R.
import abc
from typing import Generic, TypeVar
S = TypeVar('S')
R = TypeVar('R')
class Automata(Generic[S], metaclass=abc.ABCMeta):
@abc.abstractmethod
def initial_state(self) -> S:
raise NotImplementedError()
@abc.abstractmethod
def delta(self, state: S, x: int) -> S:
raise NotImplementedError()
@abc.abstractmethod
def is_final(self, state: S) -> bool:
raise NotImplementedError()
class Counter(Automata[int]):
def initial_state(self) -> int:
return 0
def delta(self, state: int, x: int) -> int:
return state + x
def is_final(self, state: int) -> bool:
return state >= 10
class Cont(Generic[R], metaclass=abc.ABCMeta):
@abc.abstractmethod
def __call__(self, automata: Automata[S]) -> R:
raise NotImplementedError()
class EAutomata(metaclass=abc.ABCMeta):
"""
∃S. Automata[S]
"""
@abc.abstractmethod
def unpack(self, cont: Cont[R]) -> R:
raise NotImplementedError()
@staticmethod
def pack(automata: Automata[S]) -> 'EAutomata':
return EAutomataBody[S](automata)
class EAutomataBody(EAutomata, Generic[S]):
def __init__(self, automata: Automata[S]):
self._automata = automata
def unpack(self, cont: Cont[R]) -> R:
return cont(self._automata)
class Test:
automata: EAutomata
def __init__(self, automata: Automata[S]):
self.automata = EAutomata.pack(automata)
def test(self) -> bool:
class C(Cont[bool]):
def __call__(self, automata: Automata[S]) -> bool:
s0 = automata.initial_state()
s1 = automata.delta(s0, 1)
s2 = automata.delta(s1, 2)
s3 = automata.delta(s2, 3)
return automata.is_final(s3)
return self.automata.unpack(C())
test = Test(Counter())
test.test()
# $ mypy existential_type.py
# Success: no issues found in 1 source file
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment