Proposal: Dependent arguments and ForAll<...> type constructor.

[elephantpanda]

Inspired by languages such as Agda and Lean. First we can write a function which takes two functions and combines them to demonstrate the syntax:

using System

(A->C) Combine(Type A, Type B, Type C, (A->B) f, (B->C) g){
    return  x=>g(f(x))
}

This can already be done using templates and writing Func<A,B> for A->B. But now, what is the type of Combine? We should have:

typeof(Combine) = ForAll<Type A, ForAll<Type B, ForAll<Type C, (A->B)∧(B->C)->(A->C) >>>

Now we can use this type as arguments of other functions and it will be properly type checked.

Why do we want to do this?

• Get's rid of templates and makes types first class citizens
• Can be used to verify functions by providing longer types
• The type of any argument can depend on any of the previous arguments.
• We can still use the notation <A> to refer to implicit arguments.
• The ForAll<..> syntax is used for when later types depend on former.
• Lots of other uses (If you know dependent type theory then you will know the uses.)
• It allows you to build libraries in C# which are proof checked so it guarantees they won't fail. (Though you aren't forced to use these).

P.S. Notice that the typeof(Combine) is actually the proposition of logic called "Hypothetical syllogism". The function is like a proof of the proposition. This is an interesting consequence.

We should also have numbers in types. Such as typeOf(Vect) = Type->uint->Type.

[HaloFour]

Can you give some real use cases? Your example is very easily accomplished in C# today:

Func<A, C> Combine<A, B, C>(Func<A, B> f, Func<B, C> g) => x => g(f(x));

[elephantpanda]

Yes indeed.
The example you gave fixes all the types at compile time. But with dependent types you can have types that depend on numbers.

The typical example is the Vector type: Vec(float,5). (e.g. this is the type of 5 dimensional float vectors). Now there is an infinite number of these types so it would not be practical to fix the types at compile time. Why you would use this type in particular is for example when adding two vectors of the same type, the type checker can check you are adding two vectors of the same dimension. (This becomes very useful when doing things like neural network programming with n-dimensional arrays of various types). This is a trivial example but there are better ones. For example you can put things like ranges and domains in types and all sorts of things. Another type might be Bitmap(width,height).

Usually in proof checkers, for example, you may have to provide a "proof" for example which is a function or term which has a particular type required. (Such as proving a function result is in the correct range). But for a practical language like C#, we could just use a null which shows although we haven't proved the condition just "trust me". But in standard libraries we could have proven functions.

I think dependent types is one of those things which is not easily understood at first glance why it's useful (so it'll be hard to convince anyone). You either like it or hate it.

[Richiban]

I'm not debating the pros or cons of dependent typing, but surely it's near-impossible to retrofit into an existing language with its own type system? I've never seen it done before without creating a new, forked language.

[elephantpanda]

That's true. A lot has been retrofitted to C# though. My proposal would be just see if we can do a first step. Maybe not allowing numbers in the first edition.

For syntax, not much would have to change I think except for adding a ForAll construct. e.g. for a type:
ForAll<Type A, ForAll<UInt B, Func<A,Func<Vec(B),A>>>

Then we might need a special keyword to say when our templates need to be resolved at compile time or runtime.

Finally, we might (?) need some way to resolve if two types are "definitionally equal". But that could come at a later date.

We can already do a lot with types, even returning them from functions e.g

	static Type GetGenericFuncType(Type A, Type B)
	{
		return typeof(Func<,>).MakeGenericType(A, B);
	}

[It would be nicer if we could just write GetGenericFuncType = (Type A, Type B)=>Func<A,B>. But that's another story.]

IMO. The template system is kind of a "hack" left over from C++ to give C# a partial implementation of dependent types. To do away with templates means we need a way to express the template parameters in the type itself, which is what the ForAll construct does. Basically it would turn the template system from a bit of a hack into a fully complete dependent type system.

Why would we want this? Well, partly it might be useful. But also, because lots of people use C# and it will introduce a generation to dependent types which will be useful for the AI information age.

If one prefers one could use a different word than ForAll to make is closer to C# language. Perhaps even Generic. e.g.

Generic<Type A, Generic<UInt B, Func<A,Func<Vec(B),A>>>

Or syntactic sugar like:

(Type A)->(UInt B)->A->(Vec(B)->A)

BTW: If anyone has better ideas of why this might be useful feel free to add them!

[mattwar]

Your notation is still hard to follow. Your ForAll/Generic thing just seems like an open generic type to me. For example, typeof(Func<,>) is the type of a delegate/function from any type to any type.

[TahirAhmadov]

I'm struggling to understand what is being requested. None of the snippets make any sense to me. C# doesn't have templates - it has generics - a very different feature.

[elephantpanda]

I'm struggling to understand what is being requested. None of the snippets make any sense to me. C# doesn't have templates - it has generics - a very different feature.

Yes, dependent type theory is a little hard to grasp!

Think of the function A foo<A>(A x).

[edited:]Now in normal C# we could ask for (foo<int>).GetType() for example. Which would give the type Func<int,int>. In dependent type theory we could simply ask for foo.GetType() which would give the type ForAll<Type A, Func<A,A>>. Which you may think of as a "Generic Type" if you wish. Since the ForAll makes A a generic variable within the type. This allows for construction of all sorts of elaborate types far greater than is allowed by the simple generic system.

Having not just the function definitions as generic but the types themselves is extremely powerful. Unfortunately the reason why they are so powerful is hard to explain in a short post.

[TahirAhmadov]

Now in normal C# we could ask for typeOf(foo<int>) for example.

We can't, though, if foo is a function, then typeOf(foo<int>) is invalid; what goes inside of typeof has to be a type, you can't put a function name there.

In dependent type theory we could simply ask for typeOf(foo) which would give the type ForAll<Type A, Func<A,A>>.

What would that type allow you to do? You can already store a MethodInfo of a generic method, then call MakeGenericMethod on it, and wrap all that in a helper class which provides a "nice" surface area:

class GenericDelegate
{
  public GenericDelegate(MethodInfo genericMethodInfo, object? instance) { ... }
  public Func<T, T> CreateDelegate<T>() { ... }
}

Having not just the function definitions as generic but the types themselves is extremely powerful.

In C#, types can already be generic. Again, I'm thoroughly confused by your statements.

[elephantpanda]

Yes indeed you can program anything in C# because it is Turing Complete. The type system is there for checking consistency at compile time.

I edited the above post. I meant GetType() instead of typeof. Thankyou for spotting that.

Sorry I can't help with your confusion. Here is some info on dependent types.

[TahirAhmadov]

I can't find the discussion, but I think what you're asking for is "value generic arguments", at least that's what I understood from that Agda page. Something like Vector<int, 5> etc. Maybe somebody can post a link to a discussion about that.
Personally, while I like compile safety, I'm not sure how that works in practice. Yes, you can compile-time check for integer literals, but once you introduce a variable, then the compiler cannot guarantee it anyway.
Or it's possible I'm misinterpreting that page altogether.

[elephantpanda]

Yes, that is part of it. BTW we would have Vector.GetType() == typeof( ForAll<Type A, Func<A, int, Type> >> ) for your example.

TBH I don't know how well this would work for C#. It's just a proposal which is unlikely to be taken any further.