Por lo que sé sobre los tipos dependientes, creo que debería ser posible, pero nunca antes había visto un ejemplo de esto en un lenguaje de tipo dependiente, por lo que no estoy exactamente seguro de por dónde empezar.

Lo que quiero es una función de la forma:

f : [Int] -> (Int -> Bool)
f : [Int] -> (Int -> Int -> Bool)
f : [Int] -> (Int -> Int -> Int -> Bool)

etc ...

Esta función toma una lista de nInts, y devuelve una función predicada de arity n que toma Ints como argumento. ¿Es posible este tipo de cosas en un lenguaje de tipo dependiente? ¿Cómo se implementaría algo como esto?