[Type Theory; C++]
Hey type theorists,
Do any of you know good reading materials on dependent functions? Notably anything on ideas of composition, forming an algebra?
My application of interest is C++. Backstory: Over the years I've had the most success with C++ by
1/10
Conversation
loosely translating C++ grammar into formal type theory. Granted C++ has its own type system, but because it's incrementally designed by a community it's ad hoc and kind of all over the place.
Right now I'm adding a *generics* module to my personal library and version 1.0
2/10
1
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
1
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
Replying to
In this example, how do you ensure that `x` and `v` are the same input? Is it right to assume that you are translating from something like this:
λx. ? : (x : A) → B x
…where `?` is the stuff in `/*insert code*/`?
I'd imagine that if your language supported multistage programming as a way to do template style stuff, you could do:
λx. '(?) : (x : A) → Code (B x)
…so this is now a function that takes `x` and returns you some quoted code of type `B x`.
1
I'm not sure it makes sense, or is safe to have `v` be a runtime parameter here, but I could be wrong, and might be missing something in your approach!
2
Show replies
Replying to
In terms of the thread, I was focusing on the narrative explanation so the example pseudo code was a lazy explanation on my part.
The idea was if you're returning a function, v was input for the returned function, while x for the dependent function.