在python中键入统一算法，如何拒绝统一（a>b，int>int）

Question

我在玩类型统一，我从这里得到了算法，https://eli.thegreenplace.net/2018/unification/

我的问题是：我想将此用作类型推断步骤，我调整了上面页面中的代码，并添加了Lark解析器来解析和统一X -> Y == W -> Z表达式，意思是类似unify(_(X, Y), _(Y, W))。此外，我使用poly表示poly类型或类型变量，mono表示int、str、bool等mono类型

我以为a -> b == int -> int会被拒绝。我能理解为什么没有被拒绝，因为unify(f(A, B), f(1, 1))是完美的。但我希望它失败。我不知道这是否应该在以后的步骤中进行，在类型检查类型时，这将在类型推断时间之后发生，但对于我的应用程序来说，这似乎是错误的

我用于类型推断的统一算法正确吗？ 如果没有，如何解决统一unify(a -> b, int -> int)问题，使其被拒绝？（任何关于这个主题的论文都很好） 或者我只是在混合球，这应该在后面的类型检查中完成

这是我的代码，要执行，您需要Larkpip install lark-parser，我使用Python3.8进行测试

from typing import (
    Dict,
    Any,
    NamedTuple,
    Optional,
    Callable,
    TypedDict,
    Generic,
    TypeVar,
    Iterable,
    Sequence,
    Tuple,
    Union,
)
from lark import Lark, Transformer as LarkTransformer

Subst = Dict[str, "TTerm"]


class TTerm:
    "Type term"

    def unify_eq(self, other) -> bool:
        pass


class TArrow(TTerm):
    def __init__(self, t1, t2):
        self.t1 = t1
        self.t2 = t2

    def unify_eq(self, other) -> bool:
        return (
            other.__class__ is TArrow
            and self.t1.unify_eq(other.t1)
            and self.t2.unify_eq(other.t2)
        )

    def __repr__(self):
        return f"({self.t1} -> {self.t2})"


class TPoly(TTerm):
    def __init__(self, name):
        self.name = name

    def unify_eq(self, other):
        return other.__class__ is TPoly and self.name == other.name

    def __eq__(self, other):
        return other.__class__ is self.__class__ and self.name == other.name

    def __repr__(self):
        return self.name


class TMono(TTerm):
    def __init__(self, val):
        self.val = val

    def unify_eq(self, other):
        return self.__class__ is other.__class__ and self.val == other.val

    def __eq__(self, other):
        return other.__class__ is self.__class__ and self.val == other.val

    def __repr__(self):
        return self.val


class TUnification:
    def __init__(self, t1: TTerm, t2: TTerm):
        self.t1 = t1
        self.t2 = t2

    def unify(self):
        return unify(self.t1, self.t2, {})

    def __repr__(self):
        return f"unify({self.t1}, {self.t2})"


def unify(x: TTerm, y: TTerm, subst: Optional[Subst]) -> Optional[Subst]:
    print(f"unify({x}, {y}, {subst})")
    if subst is None:
        return None
    elif x.unify_eq(y):
        return subst
    elif isinstance(x, TPoly):
        return unify_var(x, y, subst)
    elif isinstance(y, TPoly):
        return unify_var(y, x, subst)
    elif isinstance(x, TArrow) and isinstance(y, TArrow):
        subst = unify(x.t1, y.t1, subst)
        subst = unify(x.t2, y.t2, subst)
        return subst
    else:
        return None


def unify_var(v: TPoly, x: TTerm, subst: Subst) -> Optional[Subst]:
    print(f"unify_var({v}, {x}, {subst})")
    if v.name in subst:
        return unify(subst[v.name], x, subst)
    elif isinstance(x, TPoly) and x.name in subst:
        return unify(v, subst[x.name], subst)
    elif occurs_check(v, x, subst):
        return None
    else:
        return {**subst, v.name: x}


def occurs_check(v: TPoly, term: TTerm, subst: Subst) -> bool:
    if v == term:
        return True
    elif isinstance(term, TPoly) and term.name in subst:
        return occurs_check(v, subst[term.name], subst)
    elif isinstance(term, TArrow):
        return occurs_check(v, term.t1, subst) or occurs_check(v, term.t2, subst)
    else:
        return False


grammar = r"""
    unification : term "==" term
    ?term       : tarrow | POLY -> poly | MONO -> mono
    ?tarrow     : term "->" term | "(" term ")"
    POLY        : /[a-z]/
    MONO        : /(int|str|bool)/

    %import common.WS
    %import common.SH_COMMENT
    %import common.INT
    %ignore WS
    %ignore SH_COMMENT
"""

parser = Lark(grammar, start="unification", parser="lalr")


class Transformer(LarkTransformer):
    def unification(self, tree):
        return TUnification(tree[0], tree[1])

    def poly(self, tree):
        return TPoly(tree[0].value)

    def mono(self, tree):
        return TMono(tree[0].value)

    def tarrow(self, tree):
        return TArrow(tree[0], tree[1])


def parse(input_):
    return Transformer().transform(parser.parse(input_))


print(parse("a -> b == int -> int").unify())

输出

unify((a -> b), (int -> int), {})
unify(a, int, {})
unify_var(a, int, {})
unify(b, int, {'a': int})
unify_var(b, int, {'a': int})
{'a': int, 'b': int}

Answer 1

But I want it to fail

不过，这是正确的行为。在a -> b，a和b不必是不同的类型，因此a == b是完全正确的。因此，int -> int也可以

如果确实需要拒绝int -> int，则可以为该类型创建一个附加约束，如TArrow(a, b, constraints=[NotEqual(a, b)])，然后将其传播到树下