Можете ли вы создавать функции, которые возвращают функции зависимой арности на языке, зависящем от языка?

Ответ 1

При создании функций различной ясности вам обычно нужна функция от значений к типам. В этом случае нам нужна функция от List ℕ (или просто ℕ - длина списка) до Set:

Predicate : ℕ → Set
Predicate zero    = Bool
Predicate (suc n) = ℕ → Predicate n

Это позволяет нам создавать разные типы для каждого номера:

Predicate 0 = Bool
Predicate 1 = ℕ → Bool
Predicate 2 = ℕ → ℕ → Bool
-- and so on

Теперь, как мы используем Predicate для выражения типа f? Поскольку мы находимся в зависимом от типизированного языка, мы можем свободно использовать функции уровня ценности в типах. Итак, length кажется естественным:

f : (l : List ℕ) → Predicate (length l)

Теперь вы не указали какой-либо конкретный f, но, ради примера, я собираюсь его реализовать. Скажем, что мы хотим проверить, равны ли все числа в соответствующих позициях (т.е. 1-й аргумент функции с 1-м элементом списка и т.д.).

Я выбрал довольно простую функцию, поэтому реализация будет довольно простой. Но обратите внимание, что эти функции используют различные трюки, не похожие на те, которые используются для реализации вариационных функций с типами классов (в Haskell).

При заданном пустом списке мы просто вернем true:

f []       = true

Для случая непустого списка мы создаем функцию, принимающую один аргумент с именем n, а затем сравниваем ее с заголовком списка (m). Если эти числа не равны, мы будем сокращать оставшуюся часть f и возвращать функцию, которая игнорирует все остальные числа и просто возвращает false; если эти числа равны, мы просто продолжим с остальной частью списка:

f (m ∷ ms) = λ n → case m ≟ n of λ
  { (yes _) → f ms
  ; (no  _) → always-false
  }

И вспомогательная функция always-false:

always-false : ∀ {n} → Predicate n
always-false {zero}  = false
always-false {suc _} = λ _ → always-false

И вот как вы его используете:

test : Bool
test = f (1 ∷ 2 ∷ 3 ∷ []) 1 2 4  -- false

В качестве заключительного замечания: эти функции не очень полезны, когда у вас нет информации об аргументе, к которому вы его применяете. Например, если вы используете f в списке неизвестной длины (который был указан как аргумент другой функции), вы даже не можете применить "предикат" к числу. Вполне возможно, что список пуст, в этом случае предикат Bool и не может быть применен ни к чему.

Ответ 2

@Vitus уже предложил решение Agda с использованием зависимых типов. Здесь я комментирую Haskell, так как вы добавили его тег.

В Haskell у нас нет зависимых типов, как в Agda, поэтому мы не можем писать length l в типе. Тем не менее, мы можем использовать настраиваемый список GADT, который предоставляет длину списка на уровне типа, используя натуральные пиано.

data Z
data S n

data List n a where
   Nil :: List Z a
   Cons :: a -> List n a -> List (S n) a

Затем мы можем использовать семейство типов для вычисления типа (a -> a -> ... -> Bool) с аргументами n, где n - заданный естественный тип уровня.

type family Fun n a
type instance Fun Z     a = Bool
type instance Fun (S n) a = a -> Fun n a

Вот как вы его используете. Следующее сравнивает список с представленным "списком аргументов".

equalityTest :: Eq a => List n a -> Fun n a
equalityTest = go True
  where go :: Eq a => Bool -> List n a -> Fun n a
        go b Nil = b
        go b (Cons x xs) = \y -> go (x==y && b) xs

-- *ListGADT> equalityTest (Cons 1 (Cons 2 Nil)) 1 2
-- True
-- *ListGADT> equalityTest (Cons 1 (Cons 2 Nil)) 1 3
-- False

Ответ 3

Я помню paper от Stephanie Weirich по программированию arty-generic в Agda, который вы можете найти релевантным. Это идет немного дальше, чем то, о чем вы просите, но вступительные разделы могут дать хорошее объяснение.