Может ли тип статически гарантировать, что функция для пар лишь частично зависит от его ввода?

Question

Рассмотрим тип функции от 's к парам b'песок cs,. (Я буду использовать нотацию Haskell для типов и функций, но это не вопрос самого Haskell.) Есть много таких функций, в том числе те, в которых оба, один или ни один из (b, c) выходы зависят от.

Предположим, в частности, что первый выход зависит от a, а второй - нет (например, как в \a -> (a, ())). Можно ли написать тип в полиморфном лямбда-исчислении или Хиндли-Милнера, характеризующий все и только такие функции, другими словами, подпространство которого изоморфно (a -> b, c)? Другими словами, можем ли мы определить f :: d (для какого-то типа d) такие, что f (\a -> (a, ())), f (\a -> (a, 1)), ..., все хорошо напечатаны, но f (\a -> (a, a)), f (\a -> (a, snd a)), ... все не так?

В качестве альтернативы, есть ли какой-либо способ статически гарантировать, что элемент a -> (b, c) есть это свойство?

Answer 1

Нет, это невозможно сделать с помощью полиморфного лямбда-исчисления или Хиндли-Милнера. Для этого вам понадобится тип, который говорит о свойствах вычисления на уровне термина; это называется зависимым типом. Существуют различные логики с зависимой типизацией. Вы можете рассматривать Coq или Agda как примеры языков программирования, основанных на такой логике.

Чтобы проверка типов была разрешимой, вы обычно видите, что такой объект принимает второй аргумент, что является доказательством того, что его первый аргумент функции имеет свойство, о котором вы заявляете. Программист должен написать убедительное доказательство этого свойства, прежде чем он сможет применить fот корки до корки. Придумав некоторый синтаксис, у вас будет что-то вроде

      f :: (g :: a -> (b, c)) -> ((x :: a) -> (y :: a) -> snd (g x) == snd (g y)) -> ...

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