document assertions applying to parameters

[gavinking]

If I have:

Float sqrt(Float float) {
    "argument must be non-negative"
    assert (float>=0.0);
}

Ceylondoc should document that assertion.

[io7m]

I think it'd be nice if the assertions could appear directly in the generated documentation, negating the need to describe the assertion again in english.

[gavinking]

+1

[thradec]

I'm in doubt, how to implement it, when assertions are not so simple like in your example, eg.

shared class Foo() {

     value const = 0;

     shared void bar(Integer? n, String? s) {
         assert(exists n, n < const);
         if( n > 0 ) {
             assert(exists s, s.size == n, validate(s));
         }     
     }

 }

How deep we want to go?

[gavinking]

How deep we want to go?

I think this should only be for toplevel assertions in the method body. Perhaps even only for assertions that appear right at the start of the method body.

[io7m]

I was thinking about these in the context of design-by-contract preconditions, so I'd assume that only assertions that appear before any other statement or expression in the body are considered. Of course, "precondition", "postcondition", and "invariant" annotations would be a nice alternative, too!

[gavinking]

I was thinking about these in the context of design-by-contract preconditions, so I'd assume that only assertions that appear before any other statement or expression in the body are considered.

Yes, this is also my thinking.

[tombentley]

It would be helpful to document on a class the assertions inherited from the superclass initializer (a link to the super class preconditions would do). Otherwise you'll end up having to trawl the whole inheritence hierarchy to figure out what the complete set of assertions is.

That raises the question of refined members, for something like this:

class Foo() extends Bar() {
    void m() {
        assert(/*whatever*/);
        super.m();
    }
}

the same argument could be made: It would be helpful to document the inherited preconditions, because we know they'll be evaluated.

[gavinking]

@tombentley How about we take this one step at a time? :)

[tombentley]

Sure, sure. One step at a time down the slippery slope. You go first ;-)

[gavinking]

:-)

[thradec]

Could it be visually like this ?

[tombentley]

I think you should just lump all the preconditions together, as an extra bit of information about the method (like the Parameters subheading), rather than trying to make them per-parameter. After all, what about things like

void m(Integer i, Integer j) {
    assert(0<i<j);
    // ...
}

[tombentley]

Answering the question you actually asked, imo the version where you just show the code is fine; no need to translate the assertion into prose.

[thradec]

New "assertions" section, was my first attempt, but it doesn't look good. I think that it is part of parameter documentation, so it should be close.

In your example, the condition will be by both parameters (but I think it won't be common case).

[thradec]

no need to translate the assertion into prose.

no no, I wouldn't have courage to translate it to prose :-), it is documentation over assertion

"parameter n should be in range 0..255"
assert(n >= 0 && n <=255);

[tombentley]

it is documentation over assertion

Oh, of course! I think you should still show the code when when there is such doc annotation on the assertion. After all, the doc could be unhelpful rubbish.

[thradec]

yes, it's dilemma, because the code can be unhelpful rubbish also

[thradec]

btw. with assumption that in doc can be unhelpful rubbish, we can delete whole ceylondoc, and all issues will be done :-)

[tombentley]

Haha. But what I mean is that the doc might not capture exactly what is being asserted:

"must be positive"
assert(i>0);

Oops, we forgot to say what must be positive, and anyway "positive" is a bit ambiguous, do we mean "strictly positive" or "non-negative". If the code is available I know exactly what's going to be enforced at runtime.

How about <code> (<doc>), e.g. i > 0 (must be positive)

[thradec]

I don't have strong opinion, what is less evil.

@gavinking @FroMage WDYM ?

[thradec]

But in all case, I would add new option, which will disable adding assertions into documentation, because it can cause more harm than benefit, if they aren't written with documentation purpose.

[pthariensflame]

I think it's worth noting that, conceptually, the preconditions are part of the type of each parameter, or else are the types of some extra parameters, and the postconditions are part of the type of the return value. Obviously, Ceylon cannot support this directly (being neither dependently typed nor completely pure), but I think it's still something worth thinking about with regards to how assertions are treated, both in documentation and in code.

[io7m]

I'd love to see a full contract system in Ceylon (because so few languages have it, and so few of those that do actually do it well).

I personally think that most of the value is in preconditions as, when working with immutable data, invariants and postconditions tend to collapse into preconditions on the constructors of the types in question. If there isn't going to be a contract system in Ceylon, I think I'd prefer just having assertions that can be annotated to become preconditions:

void m (int x, int y)
{
  precondition assert (x > 0);
  precondition assert (y > x);
  ...
}

Only the explicitly marked assertions would appear as preconditions. This would obviously apply to the constructors of any given class too. This is a pretty low-cost solution, I think, and should satisfy those that don't like the idea of all assertions becoming externally visible (due to the fact that some of them may essentially be gibberish outside of the code), and should make it clear to tools exactly what should appear in documentation.

If Ceylon was going to grow a contract system, I think Racket currently has the most carefully designed one. It could most likely be borrowed with extreme prejudice.

Edit: That's Racket as in http://racket-lang.org

[pthariensflame]

@io7m I would also recommend Agda (for an example of the "contract system" being subsumed fully into the language's core semantics, as well as just of overall good design).

[pthariensflame]

See, e.g., my simple implementation of the residual representation of lenses and related things in Agda for an example of what I mean by "the contract system is subsumed into the language".

[io7m]

Yeah, I am quite familiar with Agda (and dependently typed languages in general; I've done quite a bit of work in Coq). I think there's a fair gap between a traditional contract system that just evaluates predicates and dependently typed systems where the contracts are implied by the structures of the types themselves, though. I'd think the former would be more likely to be possible to implement in Ceylon without pain and without intruding on the current design too much.

[pthariensflame]

@io7m I would normally agree, but Ceylon already has a kind of "encoded" dependent typing scheme with its metamodel.

[gavinking]

I personally think that most of the value is in preconditions as, when working with immutable data, invariants and postconditions tend to collapse into preconditions on the constructors of the types in question. If there isn't going to be a contract system in Ceylon, I think I'd prefer just having assertions that can be annotated to become preconditions:

To be honest I have never really understood the difference between a "precondition" and an assertion that happens to occur at the start of the function body.

Well, OK, I can think of one thing, that when refining a method you should not be able to strengthen its preconditions (they should be strictly weaker). But for the language to enforce this means having a pretty complex and sophisticated definition of "stronger" and "weaker" for something that is essentially an arbitrary expression.

[gavinking]

FTR, I would love to have a kind of limited system of dependent typing in Ceylon. Not a full-blown thing like what you see in some research languages, but just something more limited for dealing with numeric values, perhaps even just specifically for integers.

[io7m]

To be honest I have never really understood the difference between a "precondition" and an assertion that happens to occur at the start of the function body.

Oh, I think that's just an implementation issue. I don't think there's any conceptual difference.

When I said annotating an assertion to make it a precondition, I just meant marking an assertion so that it's understood to be an externally visible condition that should appear in documentation. There was concern expressed here about making all of the assertions appear in documentation unconditionally.

Most of the Java contract systems fail on this point actually; one of the major points of "design by contract" was that contracts should appear in documentation. All of the Java systems I tried (and most other language's systems) require reading the implementation

[pthariensflame]

@gavinking It could potentially be very useful to have such a thing, yes, but why restrict it to numeric values in particular? Something like GHC's DataKinds feature, as integrated with Ceylon's version of algebraic types, could be extremely handy, especially in making the metamodel even more type-safe.

[io7m]

I'd advise against integrating dependent typing.

I think it has to be something built into the language from the very beginning, and there has to be extensive tool support to make it workable. It's hard enough to get work done even with tactics-based theorem proving. Also, once you have dependent types, you immediately run into the problem of consistency: You want to use dependent types to ensure correctness, but in order to really ensure correctness, you want proofs. If you want proofs, you'd better be sure your type system/logic is sound and consistent, otherwise the proofs don't mean a thing. Trying to implement that into a system that already has the kind of complexity that Ceylon has (that's a relative term, I mean complex compared to the spartan types/terms that Agda and Coq have) sounds like a nightmare.

[gavinking]

but why restrict it to numeric values in particular?

Well, only because that was something that struck me as tractable without buying into a whole lot of undecidabilities, and without having spent much time studying the whole field, or really even knowing what I'm talking about. :)

As I understand it, a full dependent type system is going to be by nature undecidable because you have the expressiveness to be able to write programs in the type system. I'm wondering if there's something much more limited, that can give you a small part of the advantages of dependent typing, in some special cases.

Something like GHC's DataKinds feature

I don't know anything about this. I will try to read up on it.

[gavinking]

@io7m Yes, right, we're definitely not trying to build a languague like Coq or Agda here. That's not a goal of the project and trying to retrofit something like that would surely be impossible.

However, I definitely would like to be able to express types like Vector<3> and Matrix<X1+X2,Y>. And that's something that @RossTate and I think is likely to be tractable.

[gavinking]

However, I definitely would like to be able to express types like Vector<3> and Matrix<X1+X2,Y>.

Of course, that's a pretty different thing to the kind of preconditions we're discussing here.

[pthariensflame]

@gavinking Right. I'll shut up about it on this issue. :)

[loicrouchon]

When I said annotating an assertion to make it a precondition, I just meant marking an assertion so that it's understood to be an externally visible condition that should appear in documentation.

What about a shared assert to make distinction between what should be documented and not documented:

void foo(Integer x, Integer y) {
    "`x` must be strictly positive"
    shared assert(x > 0); // will be documented
    "`y` must be strictly positive"
    assert(y > 0); // will not be documented
}

[thradec]

Done, via 93f15c8 (at least first basic implementation). For further requirements, please open new issue.