Can Python implement dependent types?

Question

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

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]))

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

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

Answer 1

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.

From the docs:

"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]"

But in the footnote for [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."

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.