Можете ли вы создать функции, которые возвращают функции зависимой арности на языке с зависимой типизацией?
Из того, что я знаю о зависимых типах, я думаю, что это возможно, но я никогда раньше не видел такого примера на языке с зависимой типизацией, поэтому я не совсем уверен, с чего начать.
То, что я хочу, это функция формы:
f : [Int] -> (Int -> Bool)
f : [Int] -> (Int -> Int -> Bool)
f : [Int] -> (Int -> Int -> Int -> Bool)
так далее...
Эта функция принимает список из nInts
и возвращает предикатную функцию арности n, которая принимает Ints в качестве аргумента. Возможна ли такая вещь в зависимо типизированном языке? Как будет реализовано что-то подобное?