Allow return value contract to reference input contract?

[egonSchiele]

Take this function for example:

  Contract Num, Num => ArrayOf[ArrayOf[nil]]
  def twod_array(w, h)
...
  end

This function returns a 2d array of the given width and height. It would be nice if in the contract, you could specify that the 2d array should be of the size specified in the input parameters.

[nixpulvis]

A generic approach that provided complex polymorphism might solve this and other problems.

[waterlink]

Could be something along these lines:

Contract { Num, Num => ArrayOf[ArrayOf[nil, size: @args[1]], size: @args[0]] }
# def ...

[waterlink]

But it will be slower, since contract is more dynamic and basically depends on argument list - means it needs to be evaluated on each call.

[nixpulvis]

Would also love something to handle this:

Contract ArrayOf[:X] -> ArrayOf[:X]

[sfcgeorge]

An example in my project is with my class Node. A node has x and y coordinates and a type (:corner, :curve etc). x and y must be Num and type must be one of the Or[...] except if the type is :mirror then x and y must be nil --- mirror nodes calculate the x and y by reflecting the x and y of the :curve node before the previous :corner node. Currently something like:

Contract Maybe[Num], Maybe[Num], Maybe[Or[%i(corner curve mirror)]] => Node
def initialize(x, y, type: :corner)
  raise "x and y must be nil if type is :mirror" if type==:mirror && (!x.nil? || !y.nil?)
  raise "x and y must not be nil unless type is :mirror" if type!=:mirror && (x.nil? || y.nil?)
  #...
  self
end

It would be nice if contracts could express this kind of conditional requirement between args, but I can't imagine what it would look like let alone how it would be implemented. One of the best things about Contracts is how beautifully simple the syntax is, so I concluded this kind of thing probably can't be added with a nice clear syntax. If you can think of a way that would be great though 🎉

Does Haskell have anything like this, as that's what we're closest to. Any other languages with type annotations this powerful?

[alex-fedorov]

@sfcgeorge I would utilise pattern matching here:

Contract Num, Num, Maybe[{type: Or[:corner, :curve]}] => Node
def initialize(x, y, type: :corner)
  common_initialize(x, y, type)
end

Contract nil, nil, {type: :mirror} => Node
def initialize
  common_initialize(nil, nil, type)
end

private

Contract Maybe[Num], Maybe[Num], Or[:corner, :curve, :mirror] => Node
def common_initialize(x, y, type)
  # .. do stuff ..
end

[alex-fedorov]

If we go back to OO, then what you probably want is Corner, Curve and Mirror classes :)

[sfcgeorge]

@alex-fedorov Polymorphism would be clean but I like the single entrypoint and it makes specifying paths as an array of arrays easier to convert. Pros and cons either way, but you've solved my problem with the pattern matching example perfectly! I love it and it works great. I need to remember to use that more often, ok so I take back my comment about wanting conditional constraints.

[egonSchiele]

From chat: this could be a good way to do it.

In contracts:

Contract Forall(String ...) { Type... => Type ... }

[egonSchiele]

Contract(:a, :b) ArrayOf[a], Func[a => b] => ArrayOf[b]

[nixpulvis]

The a and b in the contract will probubly also need to be symbols.

[sfcgeorge]

I think it's supposed to be as follows, with methods dynamically generated for the types named as values, so no symbols within the block.

Contract(:a, :b) { [ArrayOf[a], Func[a => b] => ArrayOf[b]] }

[nixpulvis]

Ok, I suppose that's an option. I thought we'd have the parameters as symbols to have symmetry with the type variable definitions.

[sfcgeorge]

Symmetry would be nice, but for implementation I can't think how it would work with Symbols, it would likely require changing every built in contract. Dynamic methods would work without change as they'd just return Num or nil or whatever the value ends up being. Also amended above example as it was nonsense syntax, now wrapped in an array.

[badal]

And what about a contract on values like the one for division: (a, b) -> (q,r), with contract a == bq+r ?

[egonSchiele]

Taken from this paper posted by @nixpulvis: http://www.andres-loeh.de/Contract.pdf

Often we want to relate the argument to the result, expressing, for instance, that the result is greater than the argument. To this end we generalise e1 -> e2 to the dependent function contract (x : e1) -> e2. The idea is that x , which scopes over e2, represents the argument to the function. The above constraint is now straightforward to express:

(n : nat) -> { r | n < r }

(i.e. the return value should be greater than the argument).

So the contract for division could be something like:

Contract (a: Nat), (b: Nat) => [q: Nat, r: And[Nat, lambda { |r| r == a - bq }]]

This goes back to the idea of binding names to arguments.

[badal]

@egonSchiele, @nixpulvis : Yes, exactly to the point. Dependent types are what I thought of (I am familiar with them, in proof assistants, like Coq). It would wonderful - and very useful - to have them in the ruby world !

[waterlink]

I have some freaking awesome and simple idea that might work or might not regarding this code example https://github.com/egonSchiele/contracts.ruby/issues/113#issuecomment-87329450

I will try it out soon and post results.

[sfcgeorge]

@waterlink Hooray! I'm not surprised :)