Hindley-Milner Type Inference — annotation ছাড়াই টাইপ বের করা

পুরো engine — copy-paste করে চালান:

# hm.py — Hindley-Milner type inference, minimal-but-real
import itertools

_fresh_counter = itertools.count()

def fresh():
    return ('tv', next(_fresh_counter))

def reset():
    """প্রতিটা test একই numbering থেকে শুরু হোক"""
    global _fresh_counter
    _fresh_counter = itertools.count()

# টাইপ:  'int' | 'bool' | ('tv', n) | ('qtv', n) | ('->', a, b)
# AST:   ('int', n) ('bool', b) ('var', x) ('lam', x, body)
#        ('app', f, arg) ('let', x, e1, e2) ('if', c, t, e)

def prune(t, subs):
    """union-find: variable-এর শেষ binding পর্যন্ত হাঁটো (path compression)"""
    while isinstance(t, tuple) and t[0] == 'tv' and t[1] in subs:
        subs[t[1]] = resolve(subs[t[1]], subs)     # compression
        t = subs[t[1]]
    return t

def resolve(t, subs):
    t = prune(t, subs)
    if isinstance(t, tuple) and t[0] == '->':
        return ('->', resolve(t[1], subs), resolve(t[2], subs))
    return t

def occurs(v, t, subs):
    t = prune(t, subs)
    if t[0] == 'tv':
        return t[1] == v
    if t[0] == '->':
        return occurs(v, t[1], subs) or occurs(v, t[2], subs)
    return False

def unify(a, b, subs):
    a, b = prune(a, subs), prune(b, subs)
    if a == b:
        return
    if isinstance(a, tuple) and a[0] == 'tv':
        if occurs(a[1], b, subs):
            raise TypeError(f"infinite type: t{a[1]} = {show(b)}")
        subs[a[1]] = b                              # equation solved!
        return
    if isinstance(b, tuple) and b[0] == 'tv':
        unify(b, a, subs)
        return
    if isinstance(a, tuple) and isinstance(b, tuple) \
            and a[0] == '->' and b[0] == '->':
        unify(a[1], b[1], subs)
        unify(a[2], b[2], subs)
        return
    raise TypeError(f"cannot unify {show(a)} with {show(b)}")

def free_tvs(t, subs, acc=None):
    acc = set() if acc is None else acc
    t = prune(t, subs)
    if t[0] == 'tv':
        acc.add(t[1])
    elif t[0] == '->':
        free_tvs(t[1], subs, acc)
        free_tvs(t[2], subs, acc)
    return acc

def generalize(env, t, subs):
    bound = set()
    for s in env.values():
        bound |= free_tvs(s, subs)
    qv = sorted(free_tvs(t, subs) - bound)
    if not qv:
        return t                                    # monomorphic
    qs = set(qv)

    def wrap(t):
        t = prune(t, subs)
        if t[0] == 'tv':
            return ('qtv', t[1]) if t[1] in qs else t
        if t[0] == '->':
            return ('->', wrap(t[1]), wrap(t[2]))
        return t

    return ('forall', tuple(qv), wrap(t))

def instantiate(sigma, subs):
    if not (isinstance(sigma, tuple) and sigma[0] == 'forall'):
        return sigma                                # monomorphic as-is
    mapping = {v: fresh() for v in sigma[1]}

    def cp(t):
        t = prune(t, subs)
        if isinstance(t, tuple) and t[0] in ('tv', 'qtv'):
            return mapping.get(t[1], t)
        if isinstance(t, tuple) and t[0] == '->':
            return ('->', cp(t[1]), cp(t[2]))
        return t

    return cp(sigma[2])

def infer(env, e, subs):
    tag = e[0]
    if tag == 'int':
        return 'int'
    if tag == 'bool':
        return 'bool'
    if tag == 'var':
        if e[1] not in env:
            raise NameError(f"unbound variable: {e[1]}")
        return instantiate(env[e[1]], subs)
    if tag == 'lam':
        tv = fresh()
        body_t = infer({**env, e[1]: tv}, e[2], subs)
        return ('->', tv, body_t)
    if tag == 'app':
        tf = infer(env, e[1], subs)
        ta = infer(env, e[2], subs)
        tr = fresh()
        unify(tf, ('->', ta, tr), subs)
        return tr
    if tag == 'let':                                 # ★ let-polymorphism
        t1 = infer(env, e[2], subs)
        sigma = generalize(env, t1, subs)
        return infer({**env, e[1]: sigma}, e[3], subs)
    if tag == 'if':
        unify(infer(env, e[1], subs), 'bool', subs)
        tt = infer(env, e[2], subs)
        unify(infer(env, e[3], subs), tt, subs)
        return tt
    raise ValueError(tag)

def show(t, subs=None):
    subs = {} if subs is None else subs
    names = {}                                   # canonical naming: t0, t1, ...

    def nm(v):
        if v not in names:
            names[v] = f"t{len(names)}"
        return names[v]

    def go(x):
        x = prune(x, subs)
        if x == 'int' or x == 'bool':
            return x
        if isinstance(x, tuple) and x[0] in ('tv', 'qtv'):
            return nm(x[1])
        if isinstance(x, tuple) and x[0] == 'forall':
            return go(x[2])
        if isinstance(x, tuple) and x[0] == '->':
            l = prune(x[1], subs)
            left = go(l)
            if isinstance(l, tuple) and l[0] == '->':
                left = f"({left})"               # ← prune-এর পরেই paren-check
            return f"{left} -> {go(x[2])}"
        return repr(x)

    return go(t)

ID = ('lam', 'x', ('var', 'x'))

tests = [
    ("λx.x",                    ID),
    ("(λx.x) 42",               ('app', ID, ('int', 42))),
    ("λf.λx.f (f x)",           ('lam', 'f', ('lam', 'x',
                                  ('app', ('var', 'f'),
                                   ('app', ('var', 'f'), ('var', 'x')))))),
    ("let id=λx.x in if id True then id 5 else 0",
                                ('let', 'id', ID,
                                 ('if', ('app', ('var', 'id'), ('bool', True)),
                                        ('app', ('var', 'id'), ('int', 5)),
                                        ('int', 0)))),
]

for name, ast in tests:
    try:
        reset()
        subs = {}
        print(f"{name:<46} : {show(infer({}, ast, subs), subs)}")
    except Exception as err:
        print(f"{name:<46} : ERROR {err}")

print("— failure cases —")

LAM_POLY = ('app',                                  # λ-bound id: reject হবে
            ('lam', 'id',
             ('if', ('app', ('var', 'id'), ('bool', True)),
                    ('app', ('var', 'id'), ('int', 5)),
                    ('int', 0))),
            ID)
OMEGA = ('app', ('lam', 'x', ('app', ('var', 'x'), ('var', 'x'))),
                ('lam', 'x', ('app', ('var', 'x'), ('var', 'x'))))

for name, ast in [("λid. if id True then id 5 else 0", LAM_POLY),
                  ("λx. x x applied to itself", OMEGA)]:
    try:
        reset()
        subs = {}
        print(f"{name:<46} : {show(infer({}, ast, subs), subs)}")
    except Exception as err:
        print(f"{name:<46} : ERROR ({type(err).__name__}) {err}")

প্রত্যাশিত output:

λx.x                                          : t0 -> t0
(λx.x) 42                                     : int
λf.λx.f (f x)                                 : (t0 -> t0) -> t0 -> t0
let id=λx.x in if id True then id 5 else 0    : int
— failure cases —
λid. if id True then id 5 else 0              : ERROR (TypeError) cannot unify bool with int
λx. x x applied to itself                     : ERROR (TypeError) infinite type: t0 = t0 -> t1

তিনটা যাচাই:

1. Principal types — identity generic (t0 -> t0), twice-combinator পরিচিত shape; numbering আপনার run-এ আলাদা হতে পারে, shape একই।
2. let-poly চলল, λ-poly আটকাল — হুবহু একই body, শুধু binding mechanism আলাদা; ফল opposite। Concept-section-এর explanation-টা এখন executable।
3. Occurs check — λx. x x-এ error message-টা নিজেই সমীকরণটা ছাপায়: t0 = t0 -> t1। Compiler error আসলে failed equation-এর echo।