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

最接近的C#可以获得您在更好的语言中习惯的酷炫功能,例如Agda是参数多态(泛型).几乎没有类型推断 - 绝对没有类似高级类型,类型类或隐式术语,更高级别/不可预测类型,存在量化*,类型族,GADT,任何类型的依赖类型,或您关心的任何其他术语提到,我不指望会有.

一方面,它没有胃口.C#是专为工业而非研究而设计的,绝大多数C#开发人员 - 其中许多人在00年代逃离了C++ - 从未听说过我上面列出的大部分概念.设计师没有计划添加它们:正如Eric Lippert喜欢指出的那样,当你拥有数百万用户时,语言功能并不是免费的.

另一方面,它很复杂.C#集中具有子类型多态性,这是一个简单的想法,与您可能想要的许多其他类型系统功能进行了令人惊讶的深度交互.根据我的经验,少数C#开发人员可以理解的差异只是其中的一个例子.(实际上,已知具有方差的子类型和泛型的一般情况是不可判定的.)更多的是,考虑更高级的类型(Monad m变量是m？),或类型族在其参数可以被子类型化时应该如何表现.大多数高级类型系统都不会出现子类型并非巧合:帐户中的货币数量有限,而且子类型占很大比例.

也就是说,看到你可以推动它有多远,这很有趣.我有一个名为Fun With Generics的演讲(这里有幻灯片,视频现在可用!),旨在向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是a Vec<S<N>, T>不足以向类型检查器证明它是a Cons<N, T>.(你无法证明它,因为它不是真的;有人可以Vec在不同的程序集中进行子类化.)更一般地说,没有办法折叠任意一个,Vec因为编译器不能对自然数进行归纳.这很令人痛苦,因为即使页面上有信息,类型检查器也太笨了,无法让我们收获它.

正如Haskell人发现的那样,将依赖类型改造为现有语言很难.当语言是一种基于子类型的命令式面向对象语言(通常难以证明定理)时更难(复杂地与参数多态性结合).当没有人真正要求它时更难.

_{*自从写完这个答案以来,我已经对这个主题做了更多的思考,并意识到更高级别的类型确实存在并且在C#中是正确的.这使您可以使用更高级别的存在量化编码.}

Answer 2

这并不是一个真正的答案 - 正如我在评论中提到的，我认为你所要求的不可能。但这证明了我认为用户@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;
  }