"Oliver Dathe" wrote
> The following is some kind of superset of what I have proposed in [1]
>
> Example for syntax (*):
>
>     char[] f(char[] p : const(char)[]) { }
>                 ^               ^
>    Least restrictive type Tmin  |
>                      Contract type Tcontract
>
> Basic discussion:
> a.) f may only compile if it accomplishes the contract regarding p.
> b.) It is an error if Tmin is not implicitly castable to Tcontract.
> c.) For the syntax regarding the contract I used ":" at the moment. For
> further syntax proposals, see (*)
> d.) At the moment we may call the example f with parameters of type char[]
> and const(char)[]. const(char[]) is not covered by the contract and
> therefor may have to be rejected. More on that (**)
> e.) It is still nothing said what the typeof(p) is inside the function. I
> assume it has to be the type of the passed parameter.
> f.) If we want to return some slice of p, we get stuck again. Walter and
> Andrei have presented a solution in [2] up to some degree (***).
>   char[] f(return char[] p : const(char)[]) { return p[17..42]; }
> g.) f can be virtual, because no templates are required.

I'm not exactly sure what this accomplishes, because of point f) above, this seems like it is the same as:

char[] f(const(char)[] p) {...}

Meaning, f cannot modify p or return a slice of p.

-Steve

"Steven Schveighoffer" wrote
> I have found there are more issues that my solution doesn't solve exactly, so these need to be figured out.
>
> For example, a linked list of mutable classes might be a template defined as:
>
> LinkList(T)
> {
>   void append(T t) {...}
> }
>
> for the append function, the t argument is not modified during the function, but the link list node added should be not const.  So if a LinkList node is Node(T), then how do you write the signature and body of this function?  Is it important to declare t as an 'in' parameter?  I'm almost thinking that there is no real way to have the compiler be able to prove that an argument is not modified for all types of functions.
>
> In addition, going back to the same example, append should only accept a mutable object for t, otherwise, it cannot construct a proper node to add to the list.  So how is this information communicated to the compiler?  If we use:
>
> void append(in(T) t);
>
> Then a const or invariant t could be passed to the function, which would be no good.
>
> Is this even a concern that we should worry about?

This is a great case of over-analyzing :)

I now realize that this is a non-issue, because the append function cannot use an in modifier for t, because t might be modified later as a result of it being added to the list through append.  So append should not be modified.

I think this whole scheme should really be restricted to returning a subset of a given input type, not building something out of the input type.

-Steve

Steven Schveighoffer wrote:
>> Example for syntax (*):
>>
>>     char[] f(char[] p : const(char)[]) { }
>>                 ^               ^
>>    Least restrictive type Tmin  |
>>                      Contract type Tcontract
>> [...]
>> f.) If we want to return some slice of p, we get stuck again. Walter and Andrei have presented a solution in [2] up to some degree (***).
>>   char[] f(return char[] p : const(char)[]) { return p[17..42]; }
>> g.) f can be virtual, because no templates are required.
> 
> I'm not exactly sure what this accomplishes, because of point f) above, this seems like it is the same as:
> 
> char[] f(const(char)[] p) {...}
> 
> Meaning, f cannot modify p or return a slice of p.

The very first example was just to illustrate the syntax proposal for parameter const contracts. The aim is to provide the desired levels of const between Tmin and Tcontract. The passed parameter

Imho some more central problem is to apply the const level of the parameter (if desired) to the return value. I think in 90% of the time this could be solved by Walter/Andreis return storage class (if I got that thing right).

Examples:

  char[] f(return char[] p : const(char)[]) {  // p with return&contract
    static if (is(typeof(p)==const(char)[]))
      writefln("const(char)[]");
    else static if (is(typeof(p)==char[]))
      writefln("char[]");
    else
      static assert (false);
    return p[17..42];
  }
  ...
  char[] x = ...;
  auto y = f(x);                               // prints char[]
  static assert (is(typeof(y)==char[]);        // see p's return decl.
  ...
  char[] x = ...;
  auto y = f(cast(const(char)[])x);            // prints const(char)[]
  static assert (is(typeof(z)==const(char)[]); // see p's return decl.
  ...
  const(char)[] x;
  auto y = f(x);                               // prints const(char)[]
  static assert (is(typeof(y)==const(char)[]); // see p's return decl.
  ...
  const(char[]) x;
  auto y = f(x);              // error, f cannot sign the contract
  ...
  void g(int[] p : const(int)[]) {
    p.length = 17;            // ok
    p[42] = '17';             // error, breaks contract, may not compile
  }
  ...
  void h(char[] p const) {...}// short for Tcontract is const(char[])
                              // full contract, p is left invariant by h
  ...
  void i(char[] p) {          // some D1 code, does not know of const
    if (p.length)
      p.length=p.length-1;
  }
  ...
  char[] x = ...;
  i(x const(char)[]);         // call+request4contract => proven&signed
  i(x const(char[]));         // call+request4contract => fails