On 29/08/13 16:41, John Colvin wrote:
> sadly, yes. We need a release version of them, just like we have enforce and
> assert. Unfortunately in this case it won't be a library solution and will need
> compiler support.

You missed my recent thread here, then, and the responses ... :-)

I was going to add earlier: you could probably handle this with a rewrite of what Proxy does, but adding the constraint check inside the opDispatch code. Still, I think Gour has a point about Ada's attractiveness if those kinds of value safety checks are a first-class part of the language.

On Thursday, 29 August 2013 at 14:50:58 UTC, Joseph Rushton Wakeling wrote:
> On 29/08/13 16:41, John Colvin wrote:
>> sadly, yes. We need a release version of them, just like we have enforce and
>> assert. Unfortunately in this case it won't be a library solution and will need
>> compiler support.
>
> You missed my recent thread here, then, and the responses ... :-)
>
> I was going to add earlier: you could probably handle this with a rewrite of what Proxy does, but adding the constraint check inside the opDispatch code. Still, I think Gour has a point about Ada's attractiveness if those kinds of value safety checks are a first-class part of the language.

opDispatch isn't enough, you need to add to all the operators too. Shouldn't be too hard.

I think there's actually quite a lot more D can do in this regard, it's something I've been playing around with for a while. When I have some free time I might look in to it again.

On 29/08/13 17:03, John Colvin wrote:
> opDispatch isn't enough, you need to add to all the operators too. Shouldn't be
> too hard.

Ahh, you mean all the other op*'s? :-)

I guess as you say not hard, I find it a shame that it seems quite finnicky and there is quite a lot of manual work involved.

> I think there's actually quite a lot more D can do in this regard, it's
> something I've been playing around with for a while. When I have some free time
> I might look in to it again.

That would be great to see, especially if it can be made properly generic -- that is, that the constraints can be arbitrary or even functional (e.g. ensuring initialization of a struct before it is used).

W dniu 29.08.2013 15:33, Gour pisze:
> On Sun, 25 Aug 2013 17:06:27 +0200
> "bearophile" <bearophileHUGS@lycos.com> wrote:
>
>> Probably working even more you can make the D entry a bit more
>> statically safe (eventually you could reach the level of Ada code) but
>> the amount of work and code becomes excessive, and the resulting D
>> code becomes unnatural, and rather not idiomatic.
>
> Still considering whether to focus on Ada or D for my project, I wonder
> if D can do stuff like (from wikipedia page):
>
> type Day_type   is range    1 ..   31;
> type Month_type is range    1 ..   12;
> type Year_type  is range 1800 .. 2100;
> type Hours is mod 24;

These are refinement types (I call them 'views') and I have half-written DIP for this. However, I doubt that it will be accepted.

I would rather enable 'View pattern' by allowing contracts and invariants in release mode.

They still could be prepended with debug directive to establish the old behaviour:

struct S {
    debug invariant() { ... }
}

void fn()
debug in
{
    ...
}
debug out(result)
{
    ...
}
body
{
    ...
}

On Thursday, 29 August 2013 at 14:50:18 UTC, Gour wrote:
> On Thu, 29 Aug 2013 16:13:06 +0200
> "John Colvin" <john.loughran.colvin@gmail.com> wrote:
>
>> just something I whipped up in a few mins:
>
> [...]
>
> Thanks. So, it's possible, but (maybe) it's not as elegant.

Now, let's be fair. While the point you brought up is one that I,
too, do very much like with Ada, it's not magic what Ada does.

Agreed, Ada has it wrapped in nice syntactic sugar, but in the
end such a subtype is just the basic type with range checking
done bhind the curtain, while D does it publicly visible and in
the open (and, yes, less nicely sugared).

In the end it's about the concept, so the relevant question is
not "Does D offer the same sugar and wardrobe?" but "does D offer
a way to implement that (important) concept other than (C-like)
hand inserting range checking code everywhere". The answer is
"yes, it does".

A by far bigger concern in my minds eye is D's somewhat unlucky
DbC mechanism or, more precisely, the somewhat step-son treating
by disabling DbC in realease code.
I strongly feel that something like "@DbC" (and @noDbC) would be
far more satisfying.

A+ - R

Piotr Szturmaj:

> These are refinement types (I call them 'views') and I have half-written DIP for this. However, I doubt that it will be accepted.

I'll be quite interested by such DIP. Even if your DIP will be refused, it could still produce several useful consequences.

Bye,
bearophile

On 08/29/2013 09:17 PM, bearophile wrote:
> Piotr Szturmaj:
>
>> These are refinement types (I call them 'views') and I have
>> half-written DIP for this. However, I doubt that it will be accepted.
>
> I'll be quite interested by such DIP. Even if your DIP will be refused,
> it could still produce several useful consequences.


Why not build something rather general?

struct Hour{
    int hour;
    IsTrue[0 <= hour && hour <= 23] proof;
}


@terminating @correct pure nothrow @safe{ // additional attributes
// allow the compiler to erase proofs at run time in a modular fashion
// to maintain efficiency.

    alias IsTrue[bool a] = Prop[a === true];

    // (selection of intrinsic facts about built-in operators)
    IsTrue[a && b] conj[bool a,bool b](IsTrue[a] x, IsTrue[b] y);
    IsTrue[a] projA[bool a,bool b](IsTrue[a && b] ab);
    IsTrue[b] projB[bool a,bool b](IsTrue[a && b] ab);

    IsTrue[a <= c] letrans[int a,int b,int c]
        (IsTrue[a <= b] aleb, IsTrue[b <= c] blec);
}

struct WorkingHour{
    int hour;
    IsTrue[0 <= hour && hour <= 12] proof;

    @correct // meaning does not throw an error or segfault
    Hour toHour()out(r){assert(r.hour==hour);}body{// compile-time check
        return Hour(hour,
            // an explicit proof that the hour is actually in range
            conj(projA(proof),
                 letrans(projB(proof), IsTrue[12 <= 23].init))
        );
    }
    alias toHour this;
}

(Maybe there is a better choice for the syntax.)

The basic idea is to extend the type system slightly such that the compiler becomes able to type check proofs talking about program behaviour. A flow analysis ensures that proofs are properly updated.

It would then become possible to build arbitrary refinement types:

bool isPrime(int x){ return iota(3,x).all!(a=>!!(x%a)); }

struct Prime{
    int prime;
    IsTrue[isPrime(prime)] proof;
}

Prime seven = Prime(7,IsTrue[isPrime(7)].init); // proof by CTFE

assert(isPrime(x));
auto foo = Prime(x,IsTrue[isPrime(x)].init); // proof by runtime check and flow analysis

auto bar = Prime(y,IsTrue[isPrime(y)].init); // error, disabled @this


This could also be used without runtime overhead eg. inside a correctness proof for a prime sieve, though this necessitates a slightly larger apparatus than presented here.

On 08/30/2013 01:35 AM, Timon Gehr wrote:
>
> bool isPrime(int x){ return iota(3,x).all!(a=>!!(x%a)); }

bool isPrime(int x){ return 1<x && iota(3,x).all!(a=>!!(x%a)); }

On Friday, 30 August 2013 at 08:10:24 UTC, Timon Gehr wrote:
> On 08/30/2013 01:35 AM, Timon Gehr wrote:
>>
>> bool isPrime(int x){ return iota(3,x).all!(a=>!!(x%a)); }
>
> bool isPrime(int x){ return 1<x && iota(3,x).all!(a=>!!(x%a)); }

iota(3, to!int(sqrt(x)))

On 26/08/13 18:17, Zach the Mystic wrote:
> I'm kind of glad I didn't know this until now. Too much information can get in
> the way of a good metaphor, in my opinion!

That one about the boiling frog is a bit dodgy as well ... :-)