Können Sie Funktionen erstellen, die Funktionen einer abhängigen Arität in einer abhängig typisierten Sprache zurückgeben?
Nach dem, was ich über abhängige Typen weiß, denke ich, dass es möglich sein sollte, aber ich habe noch nie ein Beispiel dafür in einer abhängig geschriebenen Sprache gesehen, daher bin ich nicht genau sicher, wo ich anfangen soll.
Was ich will, ist eine Funktion der Form:
f : [Int] -> (Int -> Bool)
f : [Int] -> (Int -> Int -> Bool)
f : [Int] -> (Int -> Int -> Int -> Bool)
usw...
Diese Funktion nimmt eine Liste von nInts, und gibt eine Prädikatfunktion von arity n zurück, die Ints als Argument verwendet. Ist so etwas in einer abhängig geschriebenen Sprache möglich? Wie würde so etwas umgesetzt?