4 ms·

Will concepts (currently or in the future) be able to constrain on anything other than types? For example in the Number concept, can you have a PositiveNumber

by rawnlq 10y ago

Will concepts (currently or in the future) be able to constrain on anything other than types? For example in the Number concept, can you have a PositiveNumber concept (e.g., require Number > 0)? Or given some container, that it is sorted? Or if you have a binary operator, that it is associative? Maybe with some magical compiler that can tell you that after calling abs() or exp() the "double" type becomes a positive number concept, or that after calling sort on a vector and only doing binary inserts that the vector is still sorted. Basically a lot of contracts on how to use a function correctly is not captured by just type system or whether you can call certain functions on a type. Is there an easy way to attach a "concept" to an output in an ad hoc way?

openasocket 10y ago
What you're talking about is dependent types (https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type). The problem with these is that, in general, determining whether or not an object is of one of these types (PositiveNumber, PrimeNumber, ListWithAtLeastThreeElements, etc.) at compile time is undecidable. This isn't horrible, as template meta-programming already allows you to encode Turing Complete programs into compilation, but unlike templates, where evaluation is somewhat straightforward, evaluating dependent types requires general theorem proving. There are languages with dependent typing, but of them I only know Coq, and Coq sidesteps the issue by the language not being Turing Complete.
- saghm 10y ago
  > There are languages with dependent typing, but of them I only know Coq, and Coq sidesteps the issue by the language not being Turing Complete. There's also Idris, which I haven't really used, but from what I understand, it's sort of like Haskell with dependent types. http://www.idris-lang.org/ http://www.idris-lang.org/
vmarsy 10y ago
What you're describing is more in the domain of program verification, there's already work like this, for instance dafny [1], where you can have functions like this: method Abs(x: int) returns (y: int) ensures 0 <= y { ... } or: method MultipleReturns(x: int, y: int) returns (more: int, less: int) requires 0 < y ensures less < x < more { more := x + y; less := x - y; } [1] https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/ https://www.microsoft.com/en-us/research/project/dafny-a-lan...
openfuture 10y ago
You just described dependent types, they´re available in Idris.
gpderetta 10y ago
The failed C++0x proposal did include axioms that would have allowed the specification of such constraints, but axioms werent supposed to be checked by the compiler itself (other than syntactic correctness). Axioms were intended to be used for documentation and checked by static/dynamic analysers and possibly used for optimisations. The current concept proposal is significantly reduced in scope and doesn't include anything like axioms.
wyager 10y ago
You can do this with coq/agda/idris (fully general dependent types) or Haskell (LiquidHaskell). Not C++. LiquidHaskell is nice because it's all written in comments next to or in a separate file from your Haskell code. This means the Haskell compiler doesn't even have to know about it. On the other hand, when you're using something like Idris for formal programming, you often find your program full of proof witnesses that you aren't actually using for your real code you want to write. You can prove all sorts of things, like that a function only returns negative multiples of 3, or only returns vectors of length 5n+1.
pjmlp 10y ago
Besides what everyone else is replying about dependent typing, you can get that in C++ by a mix of concepts, classes and operator overloading. It isn't as clean, but it does the job. For example you could have a PositiveNumber class, with the mathematical operators overloaded that always validated the invariant of the number being positive.
matt_d 10y ago
I believe the contracts (preconditions, postconditions, assertions) proposal may address this issue. The latest proposal is P0380, "A Contract Design": https://wg21.link/P0380 https://wg21.link/P0380. An earlier work, "Simple Contracts for C++" (https://wg21.link/P0287 https://wg21.link/P0287), gives some further background and motivation. Notably, contracts are currently solely in the proposal stage (and not in the upcoming standard).

by rawnlq 10y ago

openasocket 10y ago

What you're talking about is dependent types (https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type). The problem with these is that, in general, determining whether or not an object is of one of these types (PositiveNumber, PrimeNumber, ListWithAtLeastThreeElements, etc.) at compile time is undecidable. This isn't horrible, as template meta-programming already allows you to encode Turing Complete programs into compilation, but unlike templates, where evaluation is somewhat straightforward, evaluating dependent types requires general theorem proving. There are languages with dependent typing, but of them I only know Coq, and Coq sidesteps the issue by the language not being Turing Complete.

saghm 10y ago
> There are languages with dependent typing, but of them I only know Coq, and Coq sidesteps the issue by the language not being Turing Complete. There's also Idris, which I haven't really used, but from what I understand, it's sort of like Haskell with dependent types. http://www.idris-lang.org/ http://www.idris-lang.org/

vmarsy 10y ago

What you're describing is more in the domain of program verification, there's already work like this, for instance dafny [1], where you can have functions like this: method Abs(x: int) returns (y: int) ensures 0 <= y { ... } or: method MultipleReturns(x: int, y: int) returns (more: int, less: int) requires 0 < y ensures less < x < more { more := x + y; less := x - y; } [1] https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/ https://www.microsoft.com/en-us/research/project/dafny-a-lan...

openfuture 10y ago

You just described dependent types, they´re available in Idris.

gpderetta 10y ago

The failed C++0x proposal did include axioms that would have allowed the specification of such constraints, but axioms werent supposed to be checked by the compiler itself (other than syntactic correctness). Axioms were intended to be used for documentation and checked by static/dynamic analysers and possibly used for optimisations. The current concept proposal is significantly reduced in scope and doesn't include anything like axioms.

wyager 10y ago

You can do this with coq/agda/idris (fully general dependent types) or Haskell (LiquidHaskell). Not C++. LiquidHaskell is nice because it's all written in comments next to or in a separate file from your Haskell code. This means the Haskell compiler doesn't even have to know about it. On the other hand, when you're using something like Idris for formal programming, you often find your program full of proof witnesses that you aren't actually using for your real code you want to write. You can prove all sorts of things, like that a function only returns negative multiples of 3, or only returns vectors of length 5n+1.

pjmlp 10y ago

Besides what everyone else is replying about dependent typing, you can get that in C++ by a mix of concepts, classes and operator overloading. It isn't as clean, but it does the job. For example you could have a PositiveNumber class, with the mathematical operators overloaded that always validated the invariant of the number being positive.

matt_d 10y ago

I believe the contracts (preconditions, postconditions, assertions) proposal may address this issue. The latest proposal is P0380, "A Contract Design": https://wg21.link/P0380 https://wg21.link/P0380. An earlier work, "Simple Contracts for C++" (https://wg21.link/P0287 https://wg21.link/P0287), gives some further background and motivation. Notably, contracts are currently solely in the proposal stage (and not in the upcoming standard).