C# 最接近您在更好 语言（如 Agda）中使用的酷炫特性是参数多态（泛型）。几乎没有类型推断 - 绝对没有类似于更高种类的类型、类型类或隐式术语、更高等级/指示性类型、存在量化*、类型族、GADT、任何类型的依赖类型，或您愿意提及的任何其他行话，我不希望会有。
一方面，它没有胃口。 C# 是为工业而不是研究设计的，绝大多数 C# 开发人员——一群实用的人，其中许多人在 00 年代逃离了 C++——甚至从未听说过我上面列出的大多数概念。并且设计师没有添加它们的计划：正如 Eric Lippert 喜欢指出的那样，a language feature don't come for free 当您拥有数百万用户时。
另一方面，这很复杂。 C# 以子类型多态为中心，这是一个简单的想法，与您可能想要的许多其他类型系统功能具有惊人的深刻交互。根据我的经验，少数 C# 开发人员可以理解的 Variance 只是其中的一个例子。 （事实上，子类型和泛型的一般情况是known to be undecidable。）更多，请考虑更高类型的类型（m 中的Monad m 变体？），或者类型族在其参数时应该如何表现可以进行子类型化。大多数高级类型系统都忽略了子类型，这并非巧合：帐户中的货币数量是有限的，而子类型会花费其中的很大一部分。
也就是说，看看你能推多远很有趣。
// 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!
}
}
不幸的是，如果没有 First 中的运行时强制转换，它就无法完成。 vec 是 Vec<S<N>, T> 的事实不足以向类型检查器证明它是 Cons<N, T>。 （你无法证明它，因为它不是真的；有人可以在不同的程序集中继承Vec。）更一般地说，没有办法折叠任意的Vec，因为编译器不能对自然进行归纳数字。这很烦人，因为即使页面上有信息，类型检查器也太笨了，我们无法获取它。
将依赖类型改造为现有语言是困难，正如 Haskell 人员所发现的那样。当语言是基于子类型（与参数多态性结合起来很复杂）的命令式面向对象语言（通常难以证明定理）时，难度会更大。当没有人真正要求它时，就更难了。
* 自从写了这个答案后，我对这个话题做了更多的思考，并意识到higher-rank types are indeed present and correct in C#。这使您可以使用higher-rank encoding of existential quantification。