worked but was messy: The style is *dispatch by spec* but all the translation work done under the hood was packaged together and ended up being spaghetti code.
I've been redesigning and slowly pulling out subroutines from that spaghetti into meaningful, reusable modules.
3/10
Conversation
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
1
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.
Not sure how one could express dependent function composition in this setting, alas, at least not off the top of my head! 😅
1
1
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
Show replies
Replying to
I've considered that, but if you restrict it to functions which return functions you can also restrict it to compile time only contexts which is sufficient for my purposes.