LeeeeT

from collections.abc import Callable
from dataclasses import dataclass
from itertools import count
from typing import Any


type Name = int


name = count(0)

LeeeeT

from dataclasses import dataclass
from itertools import count


type Name = int


name = count(0)

LeeeeT

from collections.abc import Callable
from dataclasses import dataclass
from typing import Any


type Term[T] = Var[T] | Typ[T] | Lam[T] | Fun[T] | App[T]


@dataclass(frozen=True)
class Var[T]:

LeeeeT

# Algebra f a = f a → a
# Fix f = ∀x. Algebra f x → x

# Coalgebra f a = a → f a
# Cofix f = ∃x. x × Coalgebra f x

# ListF a x = 1 + a × x
# List a = Fix (ListF a)
# Colist a = Cofix (ListF a)

LeeeeT

This script simulates IO (print and input) in a pure functional manner using a coinductive data structure.

---

Python-compatible generator:

Generator yield send return = ∃state . state × (state → return + yield × (send → state))

With the point functor:

LeeeeT

P ⊢ Q
----- →-Intro
P → Q


P → Q        P
-------------- →-Elim
Q

LeeeeT

from __future__ import annotations

import asyncio

from collections.abc import Callable
from dataclasses import dataclass
from typing import Protocol

import felis

LeeeeT

from __future__ import annotations

import itertools
import sys

from collections import Counter, defaultdict

from dataclasses import dataclass

LeeeeT

import itertools


port = itertools.count()


wires = dict[int, int]()
cells = dict[int, tuple[str, int, tuple[int, ...]]]()
queue = set[tuple[int, int]]()

LeeeeT

from sys import setrecursionlimit


setrecursionlimit(10000)


lift2 = lambda identity: lambda apply: lambda function: lambda first: apply(apply(identity(function))(first))


bind = lambda map: lambda join: lambda value: lambda function: join(map(function)(value))