Hacker News Reader

Comment by rawnlq | Hacker News Reader

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?

View on HN

What you're talking about is dependent types (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.

> 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/

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-lan...

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.

I believe the contracts (preconditions, postconditions, assertions) proposal may address this issue.

The latest proposal is P0380, "A Contract Design": https://wg21.link/P0380.

An earlier work, "Simple Contracts for C++" (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).

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.

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.

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

Reply on news.ycombinator.com