Python 可以实现依赖类型吗? [英] Can Python implement dependent types?

问题描述

Idris 中依赖类型的简单演示是 向量，其类型取决于其值.

A simple demo of dependent types in Idris is Vector, whose type depends on its value.

我们可以在 Python 中使用类型提示:

We can use type hints in Python:

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，它可以在

So, can we implement a type Vect, which can be used as in

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

，其中m 和n 是自然数，T 是任意类型?

, where m and n are natural numbers, and T is any type?

推荐答案

是的，但它超级难(而且真的很难把所有事情都做好).首先，当对对象进行更改时，您需要修改对象的类型.

Yes, but it's super hacky (and it would be really hard to get everything right). First, you would need to modify the object's type when a change is made to the object.

来自文档:

对象的类型决定了该对象支持的操作(例如，它有长度吗?")并且还定义了该类型对象的可能值.type() 函数返回一个对象的类型(即一个对象本身.就像它的身份一样，一个对象的类型也是不可改变的.[1]"

"An object’s type determines the operations that the object supports (e.g., "does it have a length?") and also defines the possible values for objects of that type. The type() function returns an object’s type (which is an object itself). Like its identity, an object’s type is also unchangeable. [1]"

但是在 [1] 的脚注中:

But in the footnote for [1]:

"[1] 在某些情况下， 可以更改对象的类型，在某些受控条件下.一般不会不过这是个好主意，因为它会导致一些非常奇怪的行为如果处理不当."

"[1] It is possible in some cases to change an object’s type, under certain controlled conditions. It generally isn’t a good idea though, since it can lead to some very strange behaviour if it is handled incorrectly."

要更改对象的类型，您需要将对象的 __class__ 属性设置为不同的类.下面是一个简单的例子，它有两种与值相关的整数类型:

To change an object's type, you need to set the object's __class__ attribute to a different class. Here's a simple example with two value-dependent types of integers:

class Integer:                                                                           
    def __init__(self, value):                                                           
        self.value = int(value)                                                          
        self.set_class()                                                                 

    def set_class(self):                                                                 
        if self.value < 10:                                                              
            self.__class__ = LessThanTen                                                 
        else:                                                                            
            self.__class__ = TenOrMore                                                   

    def add(self, value):                                                                
        self.value += int(value)                                                         
        self.set_class()                                                                 

class TenOrMore(Integer):                                                                
    def __init__(self):                                                                  
        pass                                                                             
        raise ValueError("Use Integer()")                                                

class LessThanTen(Integer):                                                              
    def __init__(self):                                                                  
        raise ValueError("Use Integer()")

然后您可以对它们执行标准操作，并根据它们的新值更改它们:

You can then do standard operations on them and have them change according to their new value:

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

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

This approach requires hard-coding classes in advance. It would be possible to generate classes dynamically, though it would require some generating gymnastics to ensure everything lived in the same scope (such as a top-level dictionary and class generator function). However, I don't think the current type hinting system would support such dynamically-generated classes.

这篇关于Python 可以实现依赖类型吗?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！