I was writing some pseudocode, and wanted to specify that the function type Combinator that has an associated arity which is the same as the first Int argument:
F :: Int -> List<Int> -> Combinator
I was thinking that if I had some way of writing a dependent type, then I could write some psuedocode like this:
F :: List<Int> -> (Int(a) -> Combinator<a>)
-- or even
F :: Int(a) -> List<Int> -> Combinator<a>
How should I express this? Is there any established notation for specifying that a function returns a dependent type of its argument?
In Idris the spelling is
F : (arity : Int) -> List Int -> Combinator arity
https://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#dependent-types