Contracts?

[jackfirth]

Sanctuary strives to complement Ramda with safe, total functions providing strong guarantees about their behavior. Enforcement is via first-order type checking, e.g. throwing TypeError when given a Number where a String is expected. However, higher-order properties are more difficult to enforce - how does one verify that the function given to Maybe.filter returns a boolean? You can check that the given value is a function but that's not enough, you'd have to check that it returns a boolean every time it's called in the implementation of Maybe.filter.

Contracts are designed to solve this problem:

import @ from "contracts.js"
@ ((Num) -> Num) -> Num
function runNumberFunc(numberFunc) {
    return numberFunc(10) + 1;
}
runNumberFunc(x => 2 * x); // valid, produces 21
runNumberFunc("foo"); // first order error, didn't provide a function
runNumberFunc(x => "foo"); // higher order error, function returned the wrong result

And just look at the error messages!

> runNumberFunc("foo");
Error: runNumberFunc: contract violation
expected: a function that takes 1 argument
given: 'foo'
in: the 1st argument of
    ((Num) -> Num) -> Num
function runNumberFunc guarded at line: 3
blaming: (calling context for runNumberFunc)

> runNumberFunc(x => "foo");
Error: runNumberFunc: contract violation
expected: Num
given: 'foo'
in: the return of
    the 1st argument of
    ((Num) -> Num) -> Num
function runNumberFunc guarded at line: 3
blaming: (calling context for runNumberFunc)

That funny looking @ ... line, as careful readers might note, isn't valid javascript. It's a sweet.js macro, a rule for transforming code from arbitrary syntax into valid javascript. The Sweet JS macro and build system provides a framework for defining these macros, and tools to generate "normal" javascript from "sweet" javascript. Using these contracts in Sanctuary would therefore imply some nontrivial wrangling of its current build system and release process, but it would be invisible to clients of the library. I would argue it falls well within the philosophy of Sanctuary to provide this.

[davidchambers]

Thank you for opening this issue, @jackfirth, and for going into quite a bit of detail! Apologies in advance for going off on a slight tangent. :)

Let's consider a familiar function, map, whose type signature is difficult to express in many languages:

map :: Functor f => (a -> b) -> f a -> f b

With sanctuary-def, the closest we can currently get is [$.Function, a, b], which is not very useful at all. However, I've been letting this "scary" case deter me from making steps in this direction. Let's replace a, b, and f with concrete types to simplify matters:

(String -> Integer) -> Array String -> Array Integer

Now, sanctuary-def gets us closer:

[$.Function, $.Array($.String), $.Array($.Integer)]

What if we could write $.Function([$.String, $.Integer]) as the first argument? We'd then need to decorate the provided function like so:

function(x) {
  if (/* `x :: String` not satisfied */) {
    throw new TypeError('…');
  }
  var result = f(x);
  if (/* `result :: Integer` not satisfied */) {
    throw new TypeError('…');
  }
  return result;
}

This is achievable.

Dealing with type variables is more involved. Let's take another step:

[$.Function([a, b]), $.Array(a), $.Array(b)]

We'd first determine the set of types common to the a values of the second argument. We'd then need to decorate the provided function such that it:

• asserts that each value to which it is applied is a member of at least one of the common types; and
• refines the set of common types as we encounter more a values.

This is achievable, though not straightforward.

The final step is to support "higher" type variables such as the f in map :: Functor f => (a -> b) -> f a -> f b (if you know the correct term for this please let me know). I imagine the logic would be similar to that which currently exists for handling type variables, but would not be recursive, and would limit the search space to (in this case) unary types.

I'll spend some time playing with sweet.js to see whether it supports bounded parametric polymorphism. If it does, I'll study the code it generates to do so. I'd love to add this functionality to sanctuary-def. Another option is to use sweet.js itself, of course, though I'm keen to avoid a build step if possible.

[jackfirth]

Contracts.js includes support for enforced parametric polymorphism out of the box. This is implemented via opaque wrappers and a notion of blame. For example in the case of filtering an array, which has type filterArray : (a -> Boolean) -> [a] -> [a]. To enforce parametricity, a contract system constructs a type of opaque object wrapper that only it can inspect - for example an object with a random key containing the actual value - and wraps each parametric input upon entrance to the filterArray function, and upon passing anything back to the calling context (either through returning a value or passing a value to a given function) unwraps the value.

When filtering for odd numbers, [1, 2, 3, 4] would be transformed by a hypothetical parametricity-enforcing contract system to [{key2487: 1}, {key2487: 2}, {key2487: 2}, {key2487: 3}], and the isOdd predicate given to the filtering function would be wrapped to a function like (opaque) => isOdd(opaque.key2487).

If you're looking to adding this behavior to sanctuary-def, I recommend heavily researching contracts. Of note, in no particular order:

• The contracts.js documentation on parametric polymorphism (can't link due to what looks like a weird Angular issue with the docs)
• The original paper on higher order function contracts
• The rho-contracts library, another javascript contracts library that does not require sweet js macros. The syntax is clunkier, but you wouldn't need macros.
• The Racket Guide chapters on contracts. Higher order contracts were originally developed for the Racket programming language, and their most exemplary implementation is in the Racket language.
• The ICFP 2014 talk on higher order and dependent contracts in Racket.

I am not sure how to extend contracts to higher kinded types like Functors. Asking the Racket mailing list / users group about this would be a very good idea.

[davidchambers]

This is fascinating, @jackfirth. I will make time to read and watch these various resources.

[davidchambers]

Closing in favour of sanctuary-js/sanctuary-def#63.