Discussion: dependent types

[orthoxerox]

If CLR is ever to be updated (#317) to include higher-kinded generics (#339), why not update it to support dependent types as well? It will be easier to do both at the same time.

A lot of work has been done by the F* team (https://fstar-lang.org/), but reification of dependent types into the CTS is not in their scope.

[louthy]

I think this would be a superb idea. It would future-proof the CLR even if these features don't immediately make it into C#.

[be5invis]

I think porting Idris into CLR would be easier...

[ymassad]

What are dependent types? What would they look like in C#?

[gafter]

The book “The Little Typer” is on my reading list to learn about dependent types.

[YairHalberstadt]

Is there any need for dependant types in the CLR? Aren't they a compile time feature?

[orthoxerox]

@YairHalberstadt depends on how far you're willing to go with them. Java's generics are a compile-time feature, CLR generics have runtime support. Dependent types can also be encoded as attributes or as CLR metadata.

[YairHalberstadt]

In F* for example, dependant types are done purely at compile time. The final program is OCaml, F#, or c, so clearly compile time dependant types are quite powerful.

I would suggest it would be worth doing a research project adding dependant types purely at compile time. That should indicate if
a) runtime support is necessary
b) the feature is doable,
c) what runtime features would dependant types most benefit from.

I think without that, any work on the runtime is unlikely to happen.

[YairHalberstadt]

Dependant types work best in functional languages, where objects are immutable.

However mutable objects make it almost impossible for a type checker to be able to prove anything about the state of an object.

Take a look at this paper:

https://www.google.co.uk/url?sa=t&source=web&rct=j&url=http://drops.dagstuhl.de/opus/volltexte/2018/9218/pdf/LIPIcs-ECOOP-2018-13.pdf&ved=2ahUKEwj27tHC9sveAhUpLsAKHRiwB4UQFjAAegQIBBAB&usg=AOvVaw3cUw88ELS2ROyQu34OJbJw

It implements a subset of dependant types in a mutable object oriented language. However it does so by keeping track of aliases, and using move semantics. As such the approach seems more suitable to Rust than to C#.

Do you know of any approach that could merge dependant types with a language like C#?

[avestura]

C# with dependent types? Hmm....

public Type StringOrInt(bool isString) => (isString) ? typeof(string) : typeof(int);

public int LengthOrSquare(bool isStr, <StringOrInt(isStr)> T, <T> value)
{
    return T switch {
        string s => s.Length,
        int i => i * i
    }
}

var length = LengthOrSquare(typeof(string), "hello"); // returns 5
var square = LengthOrSquare(typeof(int), 10); // returns 100

public <T> The(Type <T>, <T> value) => value;
var theString = The(typeof(string), "hi");
var theInt = The(typeof(int), 100);