This is where dependent functions come in.
To review (for those readers who don't fully know), to arrive at a dependent function as an idea think of it like this: We start with a regular function:
f : A --> B
Notice the domain and range (codomain) are predefined?
4/10
Conversation
We generalize this idea by weakening this constraint:
f(x) : A --> B[x]
which is to say we still predefine the domain, but now the range (codomain) is ***dependent*** on the input value. We compute the output in two rounds. Round one we take 'x' and figure out B[x],
5/10
1
then in round two we figure out the output because we at least now know which type the output is even a part of.
C++ comes in because the grammar that's most similar to dependent functions is *templated functions*:
template<auto x>
B<x> f(A v) { return /*insert code*/; }
6/10
2
They're not identical concepts, but there's a large overlap when it comes to "higher order functions" (in the computing science sense).
Notably, if the output of your dependent function is always a function, then that's a templated function: The input is the template
7/10
1
parameter where when you apply you resolve to a specialization (in C and C++ a function with known domain/codomain is called a "procedure").
If you take it in the other direction, although the grammar itself is subtly different it's the same idea.
Long story short:
8/10
1
As for my *generics* module, the parts I've pulled out notably form their own dependent functions module. To this end I'd like to take a step back and complete this module independent of generics to be added to my library.
The first higher order operator I can think of
9/10
1
adding that would be generally useful is a "composition" operator for templated functions.
So I ask: Is there anything like that already for dependent function theory so I don't have to reinvent wheels?
That's all for now. Thanks!
10/10
1
Not really sure about your translation from dependent functions to templates, but this is Agda's definition of dependent function composition: agda.github.io/agda-stdlib/Fu
1
1
You might find 's list of resources github.com/jozefg/learn-tt helpful. “Programming In Martin-Löf's Type Theory” is pretty nice in my opinion!
2
1
One thing you might find tricky is that C++'s level of dependency doesn't fully map to full-spectrum dependent types. You have two 'levels' of language - the dynamically typed macro language of templates, and the typed runtime language.
2
2
Not sure how one could express dependent function composition in this setting, alas, at least not off the top of my head! 😅
Replying to
I accept that I likely won't achieve the full scope, but I like to observe what ideas are already out there.
At the moment my approach is to wrap function templates in structs (in C++) so that can be passed as params. Then to use the compiler's deduction system as in the images.
1
1
Unburying this realisation from a subthread, as I think it might be useful for some folks reading along:
Quote Tweet
Replying to @Daniel_Nikpayuk
Ohhh wait, so the dependent part is the type parameter?! Like:
λT. λx. x * x : (T : Type) → T → T
Yeah, that absolutely works… sorry, I was misunderstanding! This makes much more sense to me now! 