expressive assertions: the best thing ever

[Paul Phillips]

I have long been very envious of the languages which can do useful things with asserts.  Then came the macros...

I adapted Peter Niederwieser's expecty[1] so it could be used with the signatures of assert/assume/require, then built the compiler with it.  Look![2] I dare you to say there is anything better in this life or the next.

Since I expect gmail will savage the formatting and thereby dampen my enthusiasm, I enclose only a tiny snippet in this email.  See url [2] below for a handful of examples from actual open scala tickets.

assert(fn.tpe != null, tree)
       |  |   |
       g  |   false
          null

[1] https://github.com/pniederw/expecty
[2] https://gist.github.com/3019862

[Paul Phillips]

By the way, obviously I need to eval the second argument, but that's enough macro fiddling for now - I was just going for the proof of wonderfulness.

[Alex Cruise]

On Fri, Jun 29, 2012 at 11:40 AM, Paul Phillips <pa...@improving.org> wrote:

By the way, obviously I need to eval the second argument, but that's enough macro fiddling for now - I was just going for the proof of wonderfulness.

This is spectaculawesome.

-0xe1a 

[Alex Kravets]

Shiny visions of a future Z3 SMT theorem prover integrated with Pedef.assert & friends as a macro library or at worst a compiler stage are now dancing in my head.

http://research.microsoft.com/en-us/um/redmond/projects/z3/ (OSS)

--
Alex Kravets       def redPill = 'Scala
[[ brutal honesty is the best policy ]]

[Daniel Sobral]

On Fri, Jun 29, 2012 at 4:16 PM, Alex Kravets <kra...@gmail.com> wrote:
> Shiny visions of a future Z3 SMT theorem prover integrated with Pedef.assert
> & friends as a macro library or at worst a compiler stage are now dancing in
> my head.
>
> http://research.microsoft.com/en-us/um/redmond/projects/z3/ (OSS)

Why don't you use it now?

https://github.com/psuter/ScalaZ3/

Granted, not macro. And maybe you are aware of it, but since you did
not link it...

>
>
> On Fri, Jun 29, 2012 at 11:52 AM, Alex Cruise <al...@cluonflux.com> wrote:
>>
>> On Fri, Jun 29, 2012 at 11:40 AM, Paul Phillips <pa...@improving.org>
>> wrote:
>>>
>>> By the way, obviously I need to eval the second argument, but that's
>>> enough macro fiddling for now - I was just going for the proof of
>>> wonderfulness.
>>
>>
>> This is spectaculawesome.
>>
>> -0xe1a
>>
>
>
>
> --
> Alex Kravets       def redPill = 'Scala
> [[ brutal honesty is the best policy ]]
>

--
Daniel C. Sobral

I travel to the future all the time.

[Daniel Sobral]

Expecty was on my list from the day you first called attention to it.
I don't see any reason for _not_ having it on the standard library.
Why in the world would we stick to an inferior error message if a
superior alternative exists, if the API doesn't change?

Now, playing as the devil advocate just a bit here, it would disclose
code in error messages. Not a lot of code, granted, but some people
can be picky about it. And some people pick up identifier names they
really shouldn't, and wouldn't if they knew users would see those
names.

[martin odersky]

On Fri, Jun 29, 2012 at 10:09 PM, Daniel Sobral <dcso...@gmail.com> wrote:

Expecty was on my list from the day you first called attention to it.
I don't see any reason for _not_ having it on the standard library.
Why in the world would we stick to an inferior error message if a
superior alternative exists, if the API doesn't change?

Now, playing as the devil advocate just a bit here, it would disclose
code in error messages. Not a lot of code, granted, but some people
can be picky about it. And some people pick up identifier names they
really shouldn't, and wouldn't if they knew users would see those
names.

It's indeed mouth-watering! One concern of course is the code overhead in the assertions. How extra code is that? I assume there's no runtime cost for the success case, right? Even if these rich asserts produce a lot of extra code, I'd still be in favor of having them, but controlled under a compile-time option.

Cheers

 - Martin

On Fri, Jun 29, 2012 at 3:38 PM, Paul Phillips <pa...@improving.org> wrote:
> I have long been very envious of the languages which can do useful things
> with asserts.  Then came the macros...
>
> I adapted Peter Niederwieser's expecty[1] so it could be used with the
> signatures of assert/assume/require, then built the compiler with it.
>  Look![2] I dare you to say there is anything better in this life or the
> next.
>
> Since I expect gmail will savage the formatting and thereby dampen my
> enthusiasm, I enclose only a tiny snippet in this email.  See url [2] below
> for a handful of examples from actual open scala tickets.
>
> assert(fn.tpe != null, tree)
>        |  |   |
>        g  |   false
>           null
>
> [1] https://github.com/pniederw/expecty
> [2] https://gist.github.com/3019862

--
Daniel C. Sobral

I travel to the future all the time.

--
Martin Odersky
Prof., EPFL and Chairman, Typesafe
PSED, 1015 Lausanne, Switzerland
Tel. EPFL: +41 21 693 6863
Tel. Typesafe: +41 21 691 4967

[Fernando Racca]

This is just great ! I'm pretty sure is worth an extra effort to try to include this by default in stdlib :)

Fernando

On Friday, 29 June 2012 21:30:12 UTC+1, martin wrote:

It's indeed mouth-watering! One concern of course is the code overhead in the assertions. How extra code is that? I assume there's no runtime cost for the success case, right? Even if these rich asserts produce a lot of extra code, I'd still be in favor of having them, but controlled under a compile-time option.

Cheers

 - Martin

On Fri, Jun 29, 2012 at 3:38 PM, Paul Phillips <pa...@improving.org> wrote:
> I have long been very envious of the languages which can do useful things
> with asserts.  Then came the macros...
>
> I adapted Peter Niederwieser's expecty[1] so it could be used with the
> signatures of assert/assume/require, then built the compiler with it.
>  Look![2] I dare you to say there is anything better in this life or the
> next.
>
> Since I expect gmail will savage the formatting and thereby dampen my
> enthusiasm, I enclose only a tiny snippet in this email.  See url [2] below
> for a handful of examples from actual open scala tickets.
>
> assert(fn.tpe != null, tree)
>        |  |   |
>        g  |   false
>           null
>
> [1] https://github.com/pniederw/expecty
> [2] https://gist.github.com/3019862

--

[Ismael Juma]

On Fri, Jun 29, 2012 at 9:30 PM, martin odersky <martin....@epfl.ch> wrote:

It's indeed mouth-watering! One concern of course is the code overhead in the assertions. How extra code is that? I assume there's no runtime cost for the success case, right? Even if these rich asserts produce a lot of extra code, I'd still be in favor of having them, but controlled under a compile-time option.

By the way, the right thing to do for runtime conditions is to inline the condition check in the body of the calling method and keep the rest in a separate method. Of course, for compile-time conditions it's even better to elide the check and code.

Best,

Ismael