C＃中的依赖类型：使输出类型取决于输入值

Question

我希望能够在C＃中创建一个方法，其输出类型取决于它的参数值;松散，

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

举个例子，我想编写一个函数，它接受一个整数并返回根据参数许多可能的类型之一：

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

任何帮助将是有用。

Answer 1

这不是一个真正的答案 - 正如我在评论中提到的，我不认为你所要求的是可能的。但是这证明了我认为用户@Douglas Zare的建议。

public void RunTest() 
    { 
    for (int n = 1; n <= 4; n++) 
    { 
     object o = F(n); 

     if (o is int) 
      Console.WriteLine("Type = integer, value = " + (int)o); 
     else if (o is bool) 
      Console.WriteLine("Type = bool, value = " + (bool)o); 
     else if (o is string) 
      Console.WriteLine("Type = string, value = " + (string)o); 
     else if (o is float[,]) 
     { 
      Console.WriteLine("Type = matrix"); 
      float[,] matrix = (float[,])o; 
      // Do something with matrix? 
     } 
    } 

    Console.ReadLine(); 
    } 


    private object F(int n) 
    { 
    if (n == 1) 
     return 42; 

    if (n == 2) 
     return true; 

    if (n == 3) 
     return "forty two"; 

    if (n >= 4) 
    { 
     float[,] matrix = new float[n, n]; 
     for (int i = 0; i < n; i++) 
      for (int j = 0; j < n; j++) 
       matrix[i, j] = 42f; 

     return matrix; 
    } 

    return null; 
    } 

Answer 2

你需要依赖类型来做到这一点。此功能仅存在于少数非主流语言（如Idris和Coq）中。

鉴于您已经正确标记了该标记，我假设您知道c＃没有该功能，那么您为什么特别要问？

Answer 3

最接近的C＃获得您熟习的很酷功能更好像Agda这样的语言是参数多态（泛型）。有很少的类型推断 - 绝对没有类似于更高级的类型，类型类别或隐式术语，更高级/ impandicative类型，存在性量化 *，类型家庭，GADT，任何类型的从属打字或任何其他行话谨慎提及，我不指望会有。

首先，它没有胃口。 C＃专为工业而设计，而不是研究，绝大多数C＃开发人员 - 实际的一群人，其中许多人在00年代逃离了C++ - 甚至从未听说过我上面列出的大多数概念。设计师没有计划添加它们：正如Eric Lippert喜欢指出的那样，a language feature don't come for free当你拥有数百万用户时。

另一方面，它很复杂。 C＃集中了子类型多态性，这是一个简单的想法，它与您可能想要的许多其他类型系统功能之间的意想不到的深刻交互。根据我的经验，少数C＃开发人员能够理解的差异仅仅是这方面的一个例子。 （实际上，具有变异的子类型和泛型的一般情况是known to be undecidable。）有关更多内容，请考虑更高级的类型（Monad m变体，m？），或者当类型族参数可以是子类型时应该如何表现。绝大多数高级类型的系统都不需要分类：账户中的货币数量是有限的，子类型的花费很大一部分。

这就是说，看到你能推多远是件有趣的事情。我有一个题为的谈话，用泛型（slides here,video now available!），它旨在将依赖类型的思想潜意识地引入到C＃用户的毫无戒心的观众。在长时间抱怨正确类型检查程序拒绝的程序，以及使用上限类型做愚蠢的事情之后，我将展示如何滥用泛型来模拟依赖类型的最简单示例。下面是谈话的荒谬结论：

// 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家伙们的发现，将相关类型改装到现有语言上的效果是hard。当语言是一种基于子类型（复杂与参数多态相结合）的命令式面向对象语言（通常很难证明有关定理）时更难。当没有人真的要求它时更加困难。

_{*自写这个答案以来，我对这个主题做了一些更多的思考，并且认识到higher-rank types are indeed present and correct in C#。这使您可以使用higher-rank encoding of existential quantification。}