ic.py

from dataclasses import dataclass
from itertools import count


type Name = int


name = count(0)


def fresh() -> Name:
    return next(name)


type Term = Var | Lam | App | Dup | Sup


@dataclass(frozen=True)
class Var:
    name: Name


@dataclass(frozen=True)
class Lam:
    name: Name
    body: Term


@dataclass(frozen=True)
class App:
    fun: Term
    arg: Term


@dataclass(frozen=True)
class Dup:
    fst: Name
    snd: Name
    value: Term
    body: Term


@dataclass(frozen=True)
class Sup:
    fst: Term
    snd: Term


def show(term: Term) -> str:
    match term:
        case Var(name):
            return f"{name}"
        case Lam(name, body):
            return f"λ{name}.{show(body)}"
        case App(fun, arg):
            return f"({show(fun)} {show(arg)})"
        case Dup(fst, snd, value, body):
            return f"!&{{{fst}, {snd}}} = {show(value)}; {show(body)}"
        case Sup(fst, snd):
            return f"&{{{show(fst)}, {show(snd)}}}"


def nf(term: Term, ctx: dict[Name, Term] | None = None) -> Term:
    if ctx is None:
        ctx = {}

    match whnf(term, ctx):
        case Lam(name, body):
            return Lam(name, nf(body, ctx))
        case App(fun, arg):
            return App(nf(fun, ctx), nf(arg, ctx))
        case Dup(fst, snd, value, body):
            return Dup(fst, snd, nf(value, ctx), nf(body, ctx))
        case Sup(fst, snd):
            return Sup(nf(fst, ctx), nf(snd, ctx))
        case term:
            return term


def whnf(term: Term, ctx: dict[Name, Term] | None = None) -> Term:
    if ctx is None:
        ctx = {}

    match term:
        case Var(name):
            if name in ctx:
                return whnf(ctx[name], ctx)
            return term
        case App(fun, arg):
            match whnf(fun, ctx):
                case Lam(name, body):
                    ctx[name] = arg
                    return whnf(body, ctx)
                case Sup(fst, snd):
                    c0 = fresh()
                    c1 = fresh()
                    a0 = App(fst, Var(c0))
                    a1 = App(snd, Var(c1))
                    return whnf(Dup(c0, c1, arg, Sup(a0, a1)), ctx)
                case fun:
                    return App(fun, arg)
        case Dup(fst, snd, value, body):
            match whnf(value, ctx):
                case Lam(lname, lbody):
                    x0 = fresh()
                    x1 = fresh()
                    f0 = fresh()
                    f1 = fresh()
                    ctx[fst] = Lam(x0, Var(f0))
                    ctx[snd] = Lam(x1, Var(f1))
                    ctx[lname] = Sup(Var(x0), Var(x1))
                    return whnf(Dup(f0, f1, lbody, body), ctx)
                case Sup(sfst, ssnd):
                    ctx[fst] = sfst
                    ctx[snd] = ssnd
                    return whnf(body, ctx)
                case value:
                    return Dup(fst, snd, value, body)
        case term:
            return term


id = Lam(x:=fresh(), Var(x))
app = App(Var(id1:=fresh()), Var(id2:=fresh()))
main = Dup(id1, id2, id, app)

print(show(main))
print(show(nf(main)))

ic_new_dup.py

from dataclasses import dataclass
from itertools import count


type Name = int


name = count(0)


def fresh() -> Name:
    return next(name)


type Term = Var | Lam | App | Dup | Sup


@dataclass(frozen=True)
class Var:
    name: Name


@dataclass(frozen=True)
class Lam:
    name: Name
    body: Term


@dataclass(frozen=True)
class App:
    fun: Term
    arg: Term


@dataclass(frozen=True)
class Dup:
    name: Name
    body: Term


@dataclass(frozen=True)
class Sup:
    fst: Term
    snd: Term


def show(term: Term) -> str:
    match term:
        case Var(name):
            return f"{name}"
        case Lam(name, body):
            return f"λ{name}.{show(body)}"
        case App(fun, arg):
            return f"({show(fun)} {show(arg)})"
        case Dup(name, body):
            return f"&{name}.{show(body)}"
        case Sup(fst, snd):
            return f"{{{show(fst)} {show(snd)}}}"


def nf(term: Term, ctx: dict[Name, Term] | None = None) -> Term:
    if ctx is None:
        ctx = {}

    match whnf(term, ctx):
        case Lam(name, body):
            return Lam(name, nf(body, ctx))
        case App(fun, arg):
            return App(nf(fun, ctx), nf(arg, ctx))
        case Dup(name, body):
            return Dup(name, nf(body, ctx))
        case Sup(fst, snd):
            return Sup(nf(fst, ctx), nf(snd, ctx))
        case term:
            return term


def whnf(term: Term, ctx: dict[Name, Term] | None = None) -> Term:
    if ctx is None:
        ctx = {}

    match term:
        case Var(name):
            if name in ctx:
                return whnf(ctx[name], ctx)
            return term
        case App(fun, arg):
            match whnf(fun, ctx):
                case Lam(name, body):
                    ctx[name] = arg
                    return whnf(body, ctx)
                case Sup(fst, snd):
                    x = fresh()
                    return whnf(Sup(App(fst, Dup(x, arg)), App(snd, Var(x))), ctx)
                case fun:
                    return App(fun, arg)
        case Dup(name, body):
            match whnf(body, ctx):
                case Lam(lname, lbody):
                    x = fresh()
                    y = fresh()
                    z = fresh()
                    ctx[name] = Lam(z, Var(y))
                    ctx[lname] = Sup(Var(x), Var(z))
                    return Lam(x, Dup(y, lbody))
                case Sup(sfst, ssnd):
                    ctx[name] = ssnd
                    return whnf(sfst, ctx)
                case body:
                    return Dup(name, body)
        case term:
            return term


id = Lam(x:=fresh(), Var(x))
main = App(Dup(id1:=fresh(), id), Var(id1))

print(show(main))
print(show(nf(main)))