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 ?