Python可以实现依赖类型吗？

Question

在Idris中依赖类型的简单演示是Vector,其类型取决于它的值.

我们可以在Python中定义Type Hints.

from typing import List

def append(a: List[int], b: List[int]) -> List[int]:
    return a + b

print(append([1, 2], [1, 3, 4]))

那么,我们可以实现一个类型Vect,可以使用如下:

def append(a: Vect[m,t], b: Vect[n,t]) -> Vect[(m+n),t]:
    return a + b

m并且n是自然数,t是任何类型的.

Answer 1

是的，但是这太老套了（而且很难让一切都正确）。首先，当对对象进行更改时，您需要修改对象的类型。

\n\n

来自文档：

\n\n

\n

“对象\xe2\x80\x99s 类型决定了该对象支持的操作（例如，\xe2\x80\x9c 它有长度吗？\xe2\x80\x9d），并且还定义了该类型对象的可能值。 type() 函数返回一个 object\xe2\x80\x99s 类型（它本身就是一个对象）。像它的身份一样，object\xe2\x80\x99s 类型也是不可更改的。[1]"

\n

\n\n

但在[1]的脚注中：

\n\n

\n

“[1]在某些情况下，在某些受控条件下，可以更改\n对象\xe2\x80\x99s类型。不过，这通常不是\xe2\x80\x99t\n好主意，因为它可能会导致一些问题如果处理不当的话，行为会非常奇怪。”

\n

\n\n

要更改对象的类型，您需要将对象的__class__属性设置为不同的类。这是一个简单的示例，其中包含两种依赖于值的整数类型：

\n\n

class Integer:                                                                           \n    def __init__(self, value):                                                           \n        self.value = int(value)                                                          \n        self.set_class()                                                                 \n\n    def set_class(self):                                                                 \n        if self.value < 10:                                                              \n            self.__class__ = LessThanTen                                                 \n        else:                                                                            \n            self.__class__ = TenOrMore                                                   \n\n    def add(self, value):                                                                \n        self.value += int(value)                                                         \n        self.set_class()                                                                 \n\nclass TenOrMore(Integer):                                                                \n    def __init__(self):                                                                  \n        pass                                                                             \n        raise ValueError("Use Integer()")                                                \n\nclass LessThanTen(Integer):                                                              \n    def __init__(self):                                                                  \n        raise ValueError("Use Integer()")\n

\n\n

然后，您可以对它们进行标准操作并让它们根据新值进行更改：

\n\n

>>> from dependent import Integer, TenOrMore, LessThanTen\n>>> a = Integer(5)\n>>> print(a.value, type(a))\n5 <class \'dependent.LessThanTen\'>\n>>> a.add(10)\n>>> print(a.value, type(a))\n15 <class \'dependent.TenOrMore\'>\n

\n\n

这种方法需要提前对类进行硬编码。动态生成类是可能的，尽管这需要一些生成体操来确保所有内容都位于同一范围内（例如顶级字典和类生成器函数）。但是，我认为当前的类型提示系统不会支持这种动态生成的类。

\n