Dependent Types in C#: making the output type depend on the input value

Question

I want to be able to make a method, in C#, whose output type depends on its argument value; loosely,

delegate B(a) DFunc<A,B>(A a);

As an example, I'd like to write a function which takes an integer and returns one of many possible types depending on the argument:

f(1) = int
f(2) = bool
f(3) = string
f(n), where n >= 4 = type of n-by-n matrices

Any help would be useful.

Answer 1

The closest C# gets to the cool features you're used to in better languages like Agda is parametric polymorphism (generics). There's very little type inference - and absolutely nothing resembling higher-kinded types, type classes or implicit terms, higher-rank/impredicative types, existential quantification*, type families, GADTs, any sort of dependent typing, or any other jargon you care to mention, and I don't expect there ever will be.

For one thing, there's no appetite for it. C# is designed for industry, not research, and the vast majority of C# developers - a practical bunch, many of whom fled C++ in the '00s - have never even heard of most of the concepts I listed above. And the designers have no plans to add them: as Eric Lippert is fond of pointing out, a language feature don't come for free when you have millions of users.

For another, it's complicated. C# centrally features subtype polymorphism, a simple idea with surprisingly profound interactions with many other type system features which you might want. Variance, which is understood by a minority of C# developers in my experience, is but one example of this. (In fact, the general case of subtyping and generics with variance is known to be undecidable.) For more, think about higher-kinded types (is Monad m variant in m?), or how type families should behave when their parameters can be subtyped. It's no coincidence that most advanced type systems leave subtyping out: there's a finite amount of currency in the account, and subtyping spends a large proportion of it.

That said, it's fun to see how far you can push it.

// 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 it can't be done without the runtime cast inside First. The fact that vec is a Vec<S<N>, T> is not enough to prove to the type checker that it's a Cons<N, T>. (You can't prove it because it isn't true; someone could subclass Vec in a different assembly.) More generally, there's no way to fold up an arbitrary Vec because the compiler can't do induction over natural numbers. It's galling because even though the information is there on the page, the type-checker is too dumb to allow us to harvest it.

Retrofitting dependent types onto an existing language is hard, as the Haskell guys are discovering. Harder when the language is an imperative object-oriented language (typically hard to prove theorems about) based on subtyping (complicated to combine with parametric polymorphism). Even harder when no one's really asking for it.

_{* Since writing this answer, I've done some more thinking on this topic and realised that higher-rank types are indeed present and correct in C#. This enables you to use a higher-rank encoding of existential quantification.}