Você pode criar funções que retornam funções de uma aridade dependente em um idioma de tipo dependente?
Pelo que sei sobre tipos dependentes, acho que deveria ser possível, mas nunca vi um exemplo disso antes em uma linguagem de tipo dependente, por isso não sei exatamente por onde começar.
O que eu quero é uma função do formulário:
f : [Int] -> (Int -> Bool)
f : [Int] -> (Int -> Int -> Bool)
f : [Int] -> (Int -> Int -> Int -> Bool)
etc ...
Esta função faz uma lista de nInts, e retorna uma função predicada de arity n que usa Ints como argumento. Esse tipo de coisa é possível em uma linguagem tipicamente dependente? Como algo assim seria implementado?