Зависимые типы в C#: создание зависимости типа вывода от входного значения

Ближе всего C# приближается к классным функциям, к которым вы привыкли в лучших языках, таких как Agda, — это параметрический полиморфизм (дженерики). Здесь очень мало вывода типов — и абсолютно ничего похожего на типы более высокого порядка, классы типов или неявные термины, высокоранговые/непредикативные типы, экзистенциальную квантификацию*, семейства типов, GADT, любой вид зависимой типизации, или любой другой жаргон, который вы захотите упомянуть, и я не ожидаю, что он когда-либо будет.

С одной стороны, нет никакого аппетита к этому. C# предназначен для промышленности, а не для исследований, и подавляющее большинство разработчиков C# — группа практиков, многие из которых ушли из C++ в 2000-х годах — никогда даже не слышали о большинстве концепций, которые я перечислил выше. И дизайнеры не планируют их добавлять: как любит указывать Эрик Липперт, языковая функция не предоставляется бесплатно, когда у вас миллионы пользователей.

Для другого это сложно. В C# центральным элементом является полиморфизм подтипов — простая идея с удивительно глубоким взаимодействием со многими другими функциями системы типов, которые могут вам понадобиться. Вариантность, которую, по моему опыту, понимает меньшинство разработчиков C#, является лишь одним из примеров этого. (На самом деле, общий случай создания подтипов и дженериков с дисперсией — это известно, что они неразрешимы.) Для получения дополнительной информации подумайте о типах более высокого порядка (является ли Monad m вариантом в 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. Сложнее, когда язык является императивным объектно-ориентированным языком (о котором обычно трудно доказать теоремы), основанным на подтипах (сложно сочетать с параметрическим полиморфизмом). Еще сложнее, когда никто об этом не просит.

_{* После написания этого ответа я еще немного подумал по этой теме и понял, что /34623859#34623859">типы более высокого ранга действительно присутствуют и корректны в C#. Это позволяет вам использовать более высокий ранговое кодирование экзистенциальной квантификации.}

Для этого вам понадобятся зависимые типы. Эта функция существует только в нескольких неосновных языках, таких как Idris и Coq.

Учитывая, что вы правильно пометили это, я предполагаю, что вы знаете, что в С# нет этой функции, так что/почему конкретно вы спрашиваете?

На самом деле это не очень хороший ответ - как я упоминаю в комментарии, я не думаю, что то, о чем вы просите, возможно. Но это демонстрирует то, что, как мне кажется, предлагает пользователь @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;
  }