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

При создании функций разной степени сложности обычно требуется функция от значений к типам. В данном случае нам нужна функция от 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 и не может быть применен ни к чему.

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

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

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

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