Proposal: Dependent Types

[elephantpanda]

We can already make a lot of types like $int\rightarrow string \rightarrow char$ as

Func<int,Func<string,char>>

The next logical step is to introduce the full dependent types. Such as $\forall_{n:int} Vec(n) \rightarrow float$

My proposal would be the following syntax which is similar to Agda notation:

Forall<(x:int)=>f(x)>

e.g. the type of a function len that gets the length of a generic list would be:

Forall<(t:Type)=>Func< List<t> , int >> len

Then it would allow you to have types dependent on other types and variables. It would also need some type inference to make it useable.

It is kind of like templates but a more advanced version.
Some advantages would be compile time checking of certain things you can't do now, like checking two lists are the same length. You can also write proofs in the type system which is quite interesting thing to do.

[En3Tho]

It's better to propose such things concrete examples of problems and solutions, how that will look in the end used code and how that will be encoded.

Your proposal is way too vague

[siegfriedpammer]

would be compile time checking of certain things you can't do now, like checking two lists are the same length

I seriously doubt that this would be feasible using types that themselves don't implement a list and enforce such properties on all operations at runtime.

I think #7508 is close to what you are looking for.