Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Dependent Types #366

Closed
mvcisback opened this issue Aug 7, 2014 · 6 comments
Closed

Dependent Types #366

mvcisback opened this issue Aug 7, 2014 · 6 comments

Comments

@mvcisback
Copy link
Contributor

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
Copy link
Member

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

@mvcisback
Copy link
Contributor Author

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
Copy link
Collaborator

JukkaL commented Aug 8, 2014

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
Copy link
Contributor Author

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
Copy link
Collaborator

JukkaL commented May 17, 2015

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.

@JukkaL JukkaL closed this as completed May 17, 2015
@pkch
Copy link
Contributor

pkch commented Mar 30, 2017

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

4 participants