I'd like to see someone relate c++ metaprogramming to something like
"dependent types", as in Nuprl:
(BTW, "function and dependent product constructors" in that file
should be "dependent function and product constructors").
There's also mention of "dependent types" in Pierce's recent _Advanced
Topics in Types And Programming Languages_ (ATTAPL) . In particular,
I'm fascintated by the way Nuprl defines record as a "dependent
function"; yet, ATTAPL calls this (p. 46) a "dependent product".
OTOH, Nuprl what Nuprl calls a "dependent product", ATTAPL calls
a "dependent sum" (p. 61). The reason this is relevant to c++
template metaprogramming is that there *appears* to be a close
correspondence between Numprl's expression of the "dependent function":
where B has x as a free variable and hence is a function from
elements of a type, A, to elements of the U_k, for some k=1...,
and where U_k is "universe of types at level k:
This close correspondence is illustrated by file,
where the comments after enum_map<NestingLevel>::field_map describe the
I'm wondering if someone could maybe use the concepts in Nuprl or
Benjamin's book to give a more formal description of template
metaprograming and this might provide more insight and ideas.
[ See http://www.yqcomputer.com/
[ comp.lang.c++.moderated. First time posters: Do this! ]