Posted: Mar 22, 2012 6:56 pm
by mizvekov
VazScep wrote:Whoops! Sorry.
Nah, don't worry.

VazScep wrote:Right. Sounds cool to me.

It's related to type-classes it seems, except that concepts can both be instantiated explicitly using concept maps, and they can be left implicit, which is a nice property.

There are interesting tradeoffs in the C++ approach to this stuff. Can concept requirements be inferred? So, if I write (I'm rusty, so I'm not sure if this is the right syntax):
Code: Select all
template<typename T> requires FooConcept
T foo() {
}

template<typename T>
T bar() {
   foo();
}
Can the FooConcept requirement on bar be inferred?

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).
Consider that you can do something like this:
Code: Select all
template<int N> struct factorial { enum { result = factorial<N - 1>::result * N }; };
template<> struct factorial<0> { enum { result = 1 }; };
int main() { std::cout << factorial<5>::result << std::endl; }

And this will calculate the factorial of 5 in compile time.
Now if you tried to write a code that analyzed a template and tried to derive the requirements on it's types, I think you would run into some variant of the halting problem :grin:

PS: The right syntax is
Code: Select all
template<typename T> requires FooConcept<T>

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.

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.

VazScep wrote:Anyway, the fact that C++ templates are required to be fully expanded gives you quite a bit of expressive power over Haskell here. Do you have any thoughts on this? Full template expansion, in the worst case, is going to lead to code bloat, and longer compilation times. But you gain because the compiler can make much more aggressive optimisations.
Like I said above, templates are far too powerful. 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.

This excessive power of templates tends to be looked down by the designers of supposed c++ successors, like java, c# and D.
I know that D's templates are severely castrated, and you can't do with them the sort of stuff you can with the MPL.
They do this so that templates are more tractable, and it's easier to write code that analyzes their properties.

VazScep wrote:The tradeoff is still debated in the functional world. Ocaml doesn't fully expand calls to polymorphic functions at compile time, because they want to allow separate compilation of modules. However, the Standard ML compiler MLton does fully expand (it's called "monomorphisation"), and they seem to think that the increased build times and code size isn't too big a deal. Then there's F#, which has separate compilation at the level of bytecode, and then monomorphises in JIT compilation.

Well F# sounds cooler by the hour.
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.

VazScep wrote:
That's cool. I take it that the compiler doesn't try to prove this sort of thing? It's just there as a context sensitive rewrite rule?

Yeah that's probably right. Although I have never tried them myself yet. Would love to though.

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 :)

VazScep wrote:Thinking about this again, I think I might have understood how concept checking works.

I guess the idea is this: when I come to instantiate bar with something that is not a FooConcept, it will fail during instantiation of foo and report this. If I put the requirement on the bar template, then it will fail during instantiation of bar with the same error?

They will fail at both times, but not the same error. Like I said before, if there are no concepts involved, the error message will happen at the point of code that tries to do something illegal with the type in question. This can happen many layers deep in a more complex template, and will spew a large error message, which will also expose the user to implementation details.
Whereas if you use concepts, the error message will be something a lot simpler, maybe even a one-liner, informing that the type in question does not conform to the required concept.