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。}