Как мы преодолеем время компиляции и время выполнения во время программирования на зависимом языке?

Мне говорят, что в системе зависимого типа "типы" и "значения" смешиваются, и мы можем рассматривать их как "термины".

Но есть кое-что, что я не могу понять: на строго типизированном языке программирования без Dependent Type (например, Haskell) типы определяются (выводятся или проверяются) во время компиляции, но значения определяются (вычисляются или вводятся) во время выполнения.

Я думаю, что между этими двумя этапами должен быть разрыв. Просто подумайте, что если значение интерактивно считывается из STDIN, как мы можем ссылаться на это значение в типе, который нужно решить AOT?

например, существует натуральное число n и список натурального числа xs (который содержит n элементов), который мне нужно прочитать из STDIN, как я могу поместить их в структуру данных Vect n Nat?

Ответ 1

Предположим, что мы вводим n :: Int во время исполнения STDIN. Затем мы читаем n строк и храним их в vn :: Vect n String (делайте вид, что это можно сделать). Аналогично, мы можем читать m :: Int и vm :: Vect m String. Наконец, мы конкатенируем два вектора: vn ++ vm (упрощая здесь бит). Это может быть тип проверен и будет иметь тип Vect (n+m) String.

Теперь верно, что проверка типа выполняется во время компиляции до того n,m как известны значения n,m, а также до vn,vm. Но это не имеет значения: мы все еще можем условно рассуждать о неизвестных n,m и утверждать, что vn ++ vm имеет этот тип, включающий n+m, даже если мы еще не знаем, что такое n+m.

Это не так уж и отличается от математики, где мы манипулируем символическими выражениями с неизвестными переменными в соответствии с некоторыми правилами, даже если мы не знаем значений переменных. Нам не нужно знать, какое число n чтобы видеть, что n+n = 2*n.

Аналогичным образом, тип проверки может ввести проверку

-- pseudocode
readNStrings :: (n :: Int) -> IO (Vect n String)
readNStrings O     = return Vect.empty
readNStrings (S p) = do
   s <- getLine
   vp <- readNStrings p
   return (Vect.cons s vp)

(Ну, на самом деле может потребоваться дополнительная помощь программиста для проверки типа, поскольку она связана с зависимым совпадением и рекурсией, но я буду пренебрегать этим).

Важно отметить, что средство проверки типов может проверить это, не зная, что такое n.

Обратите внимание, что эта же проблема уже возникает с помощью полиморфных функций.

fst :: forall a b. (a, b) -> a
fst (x, y) = x

test1 = fst @ Int @ Float (2, 3.5)
test2 = fst @ String @ Bool ("hi!", True)
...

Можно задаться вопросом, "как может проверить проверки типов fst, не зная, какие типы a и b будет во время выполнения?". Опять же, рассуждая символически.

С аргументами типа это, возможно, более очевидно, поскольку мы обычно запускаем программы после стирания типа, в отличие от параметров параметров, таких как наш n :: Int выше, которые нельзя стереть. Тем не менее, существует некоторое сходство между универсальной количественной оценкой по типам или по Int.

Ответ 2

Мне кажется, что здесь есть два вопроса:

Учитывая, что некоторые значения неизвестны во время компиляции (например, значения, считанные из STDIN), как мы можем использовать их в типах? (Обратите внимание, что ци уже дал отличный ответ на это.)
Некоторые операции (например, getLine) кажутся совершенно бессмысленными во время компиляции; как мы можем говорить о них по типу?

Ответ на (1), как сказал Чи, является символическим или абстрактным рассуждением. Вы можете прочитать число n, а затем выполнить процедуру, которая создает Vect n Nat путем чтения из командной строки n раз, используя арифметические свойства, такие как факт, что 1+(n-1) = n для ненулевого натуральные числа.

Ответ на (2) немного более тонкий. Наивно, вы можете сказать, что "эта функция возвращает вектор длины n, где n считывается из командной строки". Есть два типа, которые вы можете попробовать дать (извинения, если я получаю Haskell нотации неправильно)

unsafePerformIO (do n <- getLine; return (IO (Vect (read n :: Int) Nat)))

или (в псевдо-Coq-нотации, поскольку я не уверен, что обозначение Haskell для экзистенциальных типов)

IO (exists n, Vect n Nat)

Эти два типа действительно могут быть понятны и сказать разные вещи. Первый тип, для меня, говорит "во время компиляции, считывает n из командной строки и возвращает функцию, которая во время выполнения дает вектор длины n, выполняя IO". Второй тип говорит "во время выполнения, выполнить IO, чтобы получить натуральное число n и вектор длины n ".

Как мне нравится смотреть на это, все побочные эффекты (кроме, возможно, без прерывания) - это монадные трансформаторы, и есть только одна монада: "настоящая" монада. Трансформаторы Monad работают также на уровне типа, как на уровне термина; одна вещь, которая является специальной, run :: M a → a которая исполняет монаду (или стек монадных трансформаторов) в "реальном мире". Есть два момента времени, в которые вы можете вызвать run: один во время компиляции, где вы вызываете любой экземпляр run который отображается на уровне типа. Другая - во время выполнения, где вы вызываете любой экземпляр run который отображается на уровне значений. Обратите внимание, что run имеет смысл только при указании порядка оценки; если ваш язык не определяет, является ли это по умолчанию или по одному по вызову (или по запросу по вызову или по запросу или по вызову-другому), вы можете получить некогерентность, если вы пытаетесь вычислить тип.