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. I've posted the library on github.com/thinkmoore/bounded with documentation at thinkmoore.github.io/bounded. Implementing the 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. -- You received this message because you are subscribed to the Google Groups "Racket Developers" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-dev/etPan.56a914e6.112e6f82.124%40Scotts-MacBook-Pro.local. For more options, visit https://groups.google.com/d/optout.
