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?

Aggie

What are you trying to do that you think this will solve? – Lise

@Lise we can write less unit test with the help of type system. If I do something wrong such as return a + a . It will throw a error :"(m+m) is not equal to (m+n)" – Aggie

@Shersh Dynamic languages can and do benefit from static type analysers and PEP 484 is a testament to that. The whole 'it's better to ask for forgiveness' line of thinking is more radical than practical: if there are any errors that can be detected before execution, they should be detected. And sometimes people are forced to use dynamic languages. The reason I develop most of my projects in Python has more to do with available dependencies and language-adoption in my domain than with my (truly boundless) adoration for Python. – Spinelli

@EliKorvigo Dynamic typing vs. static typing is a very long and ongoing holy war. I can't imagine writing big project in dymanic language because it becomes unmaintainable pretty quickly. The reason I develop all of my projects in Haskell is because I still can return back to my code after 1 year and understand what's going on. And compiler will warn me about stupid mistakes. I still need to write tests. But at least I don't need to write tests for trivial things. This increases productivity a lot. – Unapproachable

@Unapproachable I was not going to start a debate on dynamic and static typing, I was simply responding to some of your statements. "If you want to avoid some classes of errors at runtime ... use some statically typed languages" – PEP 484 (mypy) have added serious support for generic static type annotations with ahead-of-time type error detection (support for dependent types is under development at the moment). *"Dependent types in dynamically typed language ... is something weird," – once again, PEP 484 proves there is nothing weird in bringing optional static annotations to a dynamic language. – Spinelli

@EliKorvigo Is it really ahead of time? Last time I've used explicit type hints in Python I got runtime fail in case of type mismatch. – Unapproachable

@Unapproachable that can't be, the type-hints are transparent to the python VM and are almost treated as comments. if you got runtime fails then you must've been using a library or something that read the __annotations__ attributes and did something based on it in run-time. – Wool

With dependent types you can write a spec (logic/relational / constraint programming) of what you want your function to do and it can auto-complete the complete definition for you using an SMT solver (Refinement Types). Also if you give it a program it might be able to infer the dependent types to you. – Budde

Note that python can implement dependent types just fine (since types are first class and can have any value semantics). Whether your static type checker (mypy, PyCharm, ...) or type dispatch/logic (functools.singledispatch,...) understands them is another question. In which context do you want to actually use these types? – Clariceclarie

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.

Firman

Answer 2

PEP 646 suggests we can. Here's their summary example

... this PEP allows an Array class that is generic in its shape (and datatype) to be defined using a newly-introduced arbitrary-length type variable, TypeVarTuple, as follows:

from typing import TypeVar, TypeVarTuple

DType = TypeVar('DType')
Shape = TypeVarTuple('Shape')

class Array(Generic[DType, *Shape]):

   def __abs__(self) -> Array[DType, *Shape]: ...

   def __add__(self, other: Array[DType, *Shape]) -> Array[DType, *Shape]: ...

Such an Array can be used to support a number of different kinds of shape annotations. For example, we can add labels describing the semantic meaning of each axis:

from typing import NewType

Height = NewType('Height', int)
Width = NewType('Width', int)

x: Array[float, Height, Width] = Array()

We could also add annotations describing the actual size of each axis:

from typing import Literal as L

x: Array[float, L[480], L[640]] = Array()

As for shape arithmetic, which would be required for your example, they say

Considering the use case of array shapes in particular, note that as of this PEP, it is not yet possible to describe arithmetic transformations of array dimensions - for example, def repeat_each_element(x: Array[N]) -> Array[2*N]. We consider this out-of-scope for the current PEP, but plan to propose additional mechanisms that will enable this in a future PEP.

Uneventful