In dynamically typed languages I can create a function that takes a function as an argument and returns a function.
For example the memoize function in Clojure.
(def memoized-fn
(memoize any-function))
In this example, memoize does not care what function any-function refers to or how many arguments it accepts*.
* Actually, it doesn't care what is passed in, (memoize 10) is valid Clojure but then trying to use the returned value will just throw an exception.
In a previous life I wanted to create something similar in a statically typed language, in my case I was working with Scala and Scala has many FunctionN types (1 arg up to 23 I believe), but without any relation between the functions there appeared to be no way to take advantage of their function-ness and create a single generic function.
In the end I had something like this *
def m(fn: Function1[A,Z]) : Function1[A,Z]
def m(fn: Function2[A,B,Z]) : Function2[A,B,Z]
....
def m(fn: Function23[A,B,....,Z]) : (fn: Function23[A,B,....,Z])
(Actually, I stopped around Fn 4 or 5 because, while I'm happy for Function23 to exist, I never want to actually have to use it.)
* This is also probably psuedo-Scala code, it's a while since I wrote any.
Back to the present day: I understand that with dependent types I can create a function that accepts an argument parameterized with a value. The well worn example for this seems to be a function that takes a list of any kind and size n and returns a list of the same size n.
I can understand this with homogenous lists (a list of kind A with size n), but I don't know if it's a possibility with heterogenous lists yet.
And from this I assume that I could create a function that takes n arguments of the same type. Something along the lines of:
def m(fn: Function[n,A]): Function[n,A]
I guess that my actual question is: Can the dependent value influence the number of types in a heterogenous way?
Also note: Please treat the memoize examples and the languages used above as examples of my idea only, I'm not asking how to memoize in a statically typed language but, rather, asking a higher level question with the memo code as an example.
* Please excuse my lack of better vocabulary in this question, I'm still learning many of this. Suggestions for edits/improvements are also welcome.
Dependent types (pis) are basically "beefed up" forms of function spaces (arrows).
If you see:
Pi x : T. T(x)
Then it's a type that's basically saying "give me an x of type T, I'll give you something of type T(x)"
In the degenerate case where T does not have any instances of x in it's body, this is equivalent to T1 -> T2 in other languages (substituting T1 for the thing in x above). The simple answer to your question is that, no, you cannot in general increase the "number of arrows" in a type, but you can do something that's basically that, if you have this.
Pi x : nat. listoflength(x)
where listoflength is something that generates a list (of some type, possibly another parameter) of length x. You could, for example, implement it using a sigma type (e.g., list with a length as it's prop argument ala this technique). The problem there is that the arguments would have to be homogenous type. The alternative is to create a function that, given an argument, gives you back a tuple of n things, which each have some type.
The basic problem is that if you give a specific n, then you need to be able to say, "I accept n arguments, here are their types," to make all of the type arithmetic work out.
So while you can't create any number of arrows, you can create something that generates a function that takes a tuple as its input (and I suppose if you knew n, you could uncurry it at the places it was being used).
In practical dependently typed programming I don't know how useful this would be (I don't have evidence to say it wouldn't be useful) but I could see the case for functions that took lists of a specific size, where the size has to have some static computation to prove they "match up." In cases where you want to accept heterogenous input types, reasoning about this in practice might be complicated, and I'd generally try to avoid that as a matter of coding practice. In dynamic languages where you can have variable numbers of arguments it seems like the use case is probably that it lets you morally "overload" a function easily, but in dependently typed languages it just seems like any notational convenience you gained from that would be lost because you'd have to prove that you were using instances correctly.