Dependent types in C #: the choice of output type depends on the input value

The closest C # gets the cool features you're used to in better , like Agda - parametric polymorphism (generics). There's very little type of inference out there - and absolutely nothing like higher-grade types, class types or implicit terms, higher rank / unresponsive types, existential quantification *, type families, GADTs, any type of dependent types, or any other jargon that you would like to mention and I do not expect that there ever will be.

First, he has no appetite. C # is for industry, not research, and the vast majority of C # developers are a practical bunch, many of whom hid in C ++ in the 00s - without even having heard of most of the concepts listed above. And the designers are not planning on adding them: as Eric Lippert likes to point out, the language feature doesn't come for free when you have millions of users.

On the other hand, it is difficult. C # centralizes subtyping polymorphism, a simple idea with surprisingly deep interactions with many other system functions you might want. The difference, which is understood by fewer C # developers in my experience, is just one example of this. (In fact, the general case of subtyping and generics with variance is known to be unsolvable .) For more, think about higher types (is a Monad m

variant in m

?), Or how family types should behave when their parameters can be subtypes. It is no coincidence that most advanced type systems leave subtypes: there is a finite amount of currency in the account, and subtyping spends most of it.

However, it's interesting to see how far you can push it. I have a talk called Fun With Generics ( slides here , video available now! ) That is designed to subliminally implement the idea of ​​dependent types for an unsuspecting audience of C # users. After complaining for a long time about correct programs that reject type checking, and doing silly things with top-type constraints, I show you how you can abuse generics to mimic the simplest examples of dependent types. Here's the absurd conclusion:

// type-level natural numbers
class Z {}
class S<N> {}

// Vec defined as in Agda; cases turn into subclasses
abstract class Vec<N, T> {}
class Nil<T> : Vec<Z, T> {}
// simulate type indices by varying
// the parameter of the base type
class Cons<N, T> : Vec<S<N>, T>
{
    public T Head { get; private set; }
    public Vec<N, T> Tail { get; private set; }

    public Cons(T head, Vec<N, T> tail)
    {
        this.Head = head;
        this.Tail = tail;
    }
}

// put First in an extension method
// which only works on vectors longer than 1
static class VecMethods
{
    public static T First<N, T>(this Vec<S<N>, T> vec)
    {
        return ((Cons<N, T>)vec).Head;
    }
}

public class Program
{
    public static void Main()
    {
        var vec1 = new Cons<Z, int>(4, new Nil<int>());
        Console.WriteLine(vec1.First());  // 4
        var vec0 = new Nil<int>();
        Console.WriteLine(vec0.First());  // type error!
    }
}

      

        
        
        
      

    

Unfortunately, this cannot be done without doing it at runtime internally First

. The fact that he vec

is is Vec<S<N>, T>

not enough to prove that he is a Cons<N, T>

. (You cannot prove this because it is not true, someone might subclass vec

in another assembly.) More generally, there is no way to dump an arbitrary vec

one because the compiler cannot do induction on natural numbers. This is because although the information is on the page, the type-checker is too dumb for us to collect.

Reconfiguring dependent types to an existing language is difficult since the guys at Haskell are discovering. It is more difficult when the language is a mandatory object-oriented language (usually hard to prove theorems) based on subtyping (difficult to combine with parametric polymorphism). It's even harder when no one asks about it.

_{* Since writing this answer, I thought a little more on this topic and realized that higher ranked types are indeed present and fixed in C # .This allows for the highest ranking encoding of existential quantification .}