Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Are C++ concepts a form of existential type?

I was looking at the definition of existential types on Wikipedia (Existential_types) and it feels similar in some way to concepts in C++ (particularly to concepts lite).

Are C++ concepts a form of existential type?

If not, what are the differences between the two?

like image 380
Rexxar Avatar asked Apr 08 '14 23:04

Rexxar


2 Answers

TL;DR: Yes, Concepts are (or at least allow you to define) existential types.


Here's my reasoning, though be warned; I'm not a type theorist:

Consider Wikipedia's definition of abstract data type (emphasis mine):

In computer science, an abstract data type (ADT) is a mathematical model for a certain class of data types of one or more programming languages that have similar semantics. An abstract data type is defined indirectly, only by the operations that may be performed on it and by mathematical constraints on the effects (and possibly cost) of those operations.

Existential types, as described by these two Stack Overflow questions and the Wikipedia article you linked, seem to be a way of modelling abstract data types using parameterized definitions. Importantly, those parameters are not part of the resulting existential type.

At face value, a concept on the other hand is a predicate on one (zero?) or more types, which can be used to restrict templates. It's not obvious that they bear any relation to existential types— until you consider requires clauses.

Basically, requires allows you to test for certain properties of types. Among these are whether they define a certain member type, have a certain member function, are convertible to certain types, etc. This observation (the main point of design, really) is where the meat of the matter lies.

It seems to me, at least, that what concepts fundamentally are is a mechanism for defining abstract data types. This is where we begin to see the similarity to existential types: they model ADTs by parameterization, and more importantly, allow you to define the ADT without exposing the parameters.

Take the Container concept, for example. You may, with Concepts Lite, write something like

void print (Container c) {
    for (const auto& e : c)
        print (e);
}

// Later
print (std::vector <int> {1, 2, 3, 4});

This works because there exists some type I such that the expressions begin (c) and end (c) return objects of type I, along with Container's other constraints. That's existential quantification; Container is an existential type.

like image 56
Stuart Olsen Avatar answered Oct 04 '22 09:10

Stuart Olsen


As far as I know, C++ concepts are arbitrary type predicates. The work on C++ concepts concentrates more on how these predicates integrate into the language rather than on giving a particular meaning or specifying a mathematical / logical model. The idea is that exactly as a function

void f(double x);

is clearly expecting a parameter of type double, in such a simple way

template <Container C>
void f(const C& c);

is expecting not just a typename but a Container. Now, how is Container defined? It could be e.g.

template <typename T>
struct Container: std::false_type { };

template <typename T, size_t N>
struct Container <std::array<T, N> >: std::true_type { };

template <typename T, typename A>
struct Container <std::vector<T, A> >: std::true_type { };

and so on. Predicates like Container exist now, but to integrate them into a template function requires inconvenient constructs like std::enable_if. Concepts will make this cleaner and easier to use.

This again, is just roughly my understanding.

like image 42
iavr Avatar answered Oct 04 '22 11:10

iavr