Mypy: Dependent Types

[mvcisback]

While trying to model the output of product from itertools #358, its become apparent that the mypy type system lacks the strength to model value defined types.

This will happen with any kind of n-vector and is and could be potentially solved statically using dependent types.

This would likely be a massive endeavor, but the conversation is likely worth having.

[gvanrossum]

Can you explain this using an example? I have no idea what "value-defined types" are, not "dependent types".

[mvcisback]

Dependent types in this content refers to a type system similar to that seen in Coq, Agda, and Idris.

The example referenced in #358 is that of the product type.
Ignoring repeat for the moment, the types of product look as follows:

x :: Iterator[T1]
y :: Iterator[T2]
z :: Iterator[T3]
product(x, y) :: Iterator[Tuple[T1, T2]]
product(x, y, z) :: Iterator[Tuple[T1, T2, T3]]
product(x, x, x, x) :: Iterator[Tuple[T1, T1, T1, T1]]

The problem here is the variable number of arguments. (what I referred to as a n-vector).
If the type instead looked like:

def product(*args :Tuple[n]) -> Iterator[Tuple[n]]: pass

where _n_ is the length of the Tuple and the type of the _k_ th element is Tuple[_n_, _k_]

Dependent types solves this and more by generally allowing the _value_ of the type to be part of the type signature. The value for the product example would include the length _n_ of *args.

The common example (which can be shoehorned into non-dependent type systems, but is still a good example) is disallowing 0 in the division function.
This blog post gives a pretty good explanation: http://ejenk.com/blog/why-dependently-typed-programming-will-one-day-rock-your-world.html

[JukkaL]

My impression is that full dependent types are currently only good for pretty specialized applications (mostly research)... and even then they can be very difficult to work with. However, there might be some ideas that could be used in a more mainstream context. Retrofitting existing code (esp. imperative) with dependent types is still an open research problem, I think.

[mvcisback]

Yes, the motivation of the proposal is less to say "lets just implement dependent types" and more "Is there anything we can get out of a simple approximation of dependent types".

By "approximation of dependent types", I mean supporting many common features in one way or another.

For example: Ignoring unpacking using * and *_, the number of arguments is known before runtime.
That said, * and *_ unpacking may prove to be an insurmountable problem....

[JukkaL]

Closing this now, as there hasn't been any updates in a long time. If somebody has a more concrete proposal, feel free to open a new issue.

[pkch]

This issue comes up on google search for mypy dependent types, so I want to link it to #3062 where this discussion continues.