类型统一算法在python中，如何拒绝统一(a -> b，int -> int)

Question

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

我的问题是:我想使用这个作为类型推断步骤，我调整了上面页面的代码，并添加了Lark解析器来解析和统一X -> Y == W -> Z表达式，意思类似于unify(_(X, Y), _(Y, W))。我还用poly表示多类型，或类型变量，mono表示像int，str，bool这样的单类型。

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

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

这是我的代码，为了执行你需要的Lark pip 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

，但我希望它失败

不过，这是正确的行为。在a -> b中，a和b不必是不同的类型，所以a == b是非常好的。因此，int -> int也很好。

如果你真的需要拒绝int -> int，你可以为这个类型创建一个额外的约束，比如TArrow(a, b, constraints=[NotEqual(a, b)])，然后在树中向下传播它。