Posted: Mar 22, 2012 9:23 pm
by VazScep
mizvekov wrote:Nope, it's just impossible to do. C++ templates are far too powerful, they are a turing complete sublanguage inside of c++ itself, and in fact there are whole libraries for metaprogramming built on top of them (boost's MPL for example).
Hmm...could you restrict the inference to the use of concepts though?

I've read (since my last post) that the way you would manually typecheck something like "bar" is to construct an archetype that minimally implements the concept. Hopefully, that could be done automatically, by automatically constructing the archetype. But I'm tempted to think this should just be an option for compiler writers.

And by the way, don't worry, this stuff isn't even in the standard. There is currently no compiler supporting this. There was a patch for gcc a while ago that implemented it partially, but it's development was ceased when the standard committee dropped it.
There's ConceptGCC! It sounds like it's seriously prototype at the moment, though.

PS2: The reverse is possible. If you declare a concept as 'auto', then the compiler can infer which types conform to that concept.
What can't be done is just the opposite, the compiler cannot infer what concepts a template type parameter needs to conform to.
As I understand, if you declare a concept as auto, then no inference actually happens. It just means you don't need a concept map, and so concept-satisfaction will happen at template-expansion time. Is that right?

I don't expect C++ to infer arbitrary concepts without explicit concept annotations, though, since presumably, there could be multiple concepts that a type could satisfy. You can have concepts that overlap right?

VazScep wrote:Like I said above, templates are far too powerful.
I'm not yet convinced :P Many of the GHC extensions give you a Turing complete type-theory too.

And using that power is not necessarily easy. Not only can (shitty) compilers crash if you recurse your templates too deep, but consider an hypothetical case where a compilation error happens at recursive depth 50, can you imagine the size of the error message you will get? :grin:

The template expansion doesn't necessarily give you code bloat though. Compilers will normally implement a final step of merging code of template instances which are similar, but it's just an heuristic anyway.
Ah, this is interesting. Can you point me to some documentation about this?

Well F# sounds cooler by the hour.
It doesn't have the Ocaml module system unfortunately. But it has lots of other cool stuff, such as type-inferred dimensional types, which are awesome. I've had the compiler reject my F# code, and point me to a logic error where I was trying to add a distance to a velocity because of a careless placement of brackets. Without the type-checking, I'm not sure how long I would have spent tracking the bug.

But anyway, c++ allows for separate compilation of 'modules' even where templates are concerned, but it requires manual intervention. Basically you can declare a template instantiation as extern, and then force it to be instantiated at any compilation unit you want.
Again, this is interesting. Do you know what the tradeoffs are? How does use of "extern" mesh with dynamically linked libraries? If there are issues, are they even that big a deal?

VazScep wrote:This ability to state formal properties of one's code is, of course, something I absolutely love. You should be able to carve out whole hierarchies of algebras based on these concepts. And maybe we can start making these axioms more expressive and shoving in some formal verification and theorem proving :whistle:

Hah hold your horses right there. We are just too many years away from being able to even try this :)
Hey, it's a significant advance. Axiomatic constraints are normally just given in documentation, which is not machine-readable. That's the most significant barrier to formal verification.