While we were developing shill we devised a useful form of contract
that we called a "bounded parametric polymorphic contract." A bounded
parametric polymorphic contract emulates bounded parametric
polymorphism similar to how existing Racket parametric contracts
emulate parametric polymorphism. Our original implementation was
specialized to a particular set of contracts we used for shill, but I
have developed an experimental library that supports arbitrary
higher-order contracts that I would like feedback on.
Here is a brief example:
> (define (id x) x)
> (define/contract (check fn val)
(bounded-polymorphic->/c ([X (integer? . -> . integer?)]) (X any/c . -> . X))
(fn val)
fn)
> (check id 0)
#<procedure:id>
> (check id 'bad)
check: broke its own contract
promised: integer?
produced: 'bad
in: the 1st argument of
...
the 1st argument of
(bounded-polymorphic->/c
((X (-> integer? integer?)))
(-> X any/c X))
contract from: (function check)
blaming: (function check)
(assuming the contract is correct)
at: eval:3.0
> ((check id 0) 'ok)
'ok
At each application of the contracted function,
bounded-polymorphic->/c creates a fresh contract for each type
variable. Values flowing into the polymorphic function through a
generated contract are wrapped with the bounding contract of the
corresponding type variable. Values flowing out of the function
through a generated contract are required to be wrapped by the
corresponding contract. If so, the contract is removed. If not, a
contract violation is raised.
The effect of this contract is that the contracted function can access
the value only according to the restrictions imposed by the bound, but
values returned from the function can be used without restriction.
For blame correctness, any contracts applied in the body of the
function remain after unwrapping.
This does not quite achieve bounded parametric polymorphism because
there is no check that all values flowing through the same type
variable have the same type. This is also a limitation of
parametric->/c, though solutions are discussed in Guha et al's
"Relationally-Parametric Polymorphic Contracts". It should be
straightforward to create a version of the contract that requires
specialization to a particular type, but we found the current version
adequate for our needs.
contracts with correct blame and contract enforcement requires a new
operation that removes a chaperone or impersonator from a stack of
chaperones around a value. Because this is not something the existing
implementation allows, I had to add a new primitive function as a
Racket extension that accesses private types from the Racket
implementation. This is very much a hack, so some extra compilation
trickiness is required. If the functionality makes sense, perhaps it
makes sense to incorporate into Racket directly.
The new primitive is (remove-impersonator value imp orig), which
returns a new copy of value with the given impersonator removed.
value must itself be an chaperone for imp, and orig nust be the
value that is directly impersonated by imp. This serves as a witness
that the caller already has the ability to invoke the underlying value
without the imp impersonator. My rational for why this method is safe
is that by the chaperone and impersonator properties, an outer
impersonator cannot rely on whether the value it wraps is already
chaperoned or impersonated. (Of course, it is possible to write such
a chaperone using eq? or impersonator? and associated functions, but
I don't think this is done in practice or recommended.) I could see this
primitive also being useful for things like option contracts.
I'd appreciate any thoughts on both the new contracts and the
implementation details.