Bounded parametric polymorphic contracts

[Scott Moore]

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.

[Asumu Takikawa]

Hi Scott,

This is cool!

On 2016-01-27 14:05:10 -0500, Scott Moore wrote:
> 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.

I think there is another sense in which it's not quite parametric (or at least
it's different from parametric->/c). Here's an example:

Welcome to Racket v6.4.0.4.
-> (require bounded)
-> (struct foo (x) #:property prop:procedure 0)
-> (define/contract (check fn val)

(bounded-polymorphic->/c ([X (integer? . -> . integer?)]) (X any/c . -> . X))

;; I thought this would error rather than succeeding
(displayln (foo-x fn))
fn)
-> (check (foo (lambda (x) 3)) 3)
#<procedure>
#<procedure>

How I imagined this might work is that you would wrap the value so that you can
only make observations corresponding to the bound. So here you force the `foo`
to act only as an int function, masking its structness since that's a finer
distinction than the bound gives you.

Also it's interesting that only higher-order contracts are accepted as bounds.
I guess because you need to stamp the value as belonging to X while still
allowing operations on it? (which you couldn't do on a symbol, say)

Cheers,
Asumu

[Scott Moore]

 
Thanks for taking a look, and for your help getting it set up to build using the package system!

On January 28, 2016 at 12:38:00 AM, Asumu Takikawa (as...@ccs.neu.edu(mailto:as...@ccs.neu.edu)) wrote:
> Hi Scott,
>
> This is cool!
>
> On 2016-01-27 14:05:10 -0500, Scott Moore wrote:
> > 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.
>
> I think there is another sense in which it's not quite parametric (or at least
> it's different from parametric->/c). Here's an example:
>
> Welcome to Racket v6.4.0.4.
> -> (require bounded)
> -> (struct foo (x) #:property prop:procedure 0)
> -> (define/contract (check fn val)
> (bounded-polymorphic->/c ([X (integer? . -> . integer?)]) (X any/c . -> . X))
> ;; I thought this would error rather than succeeding
> (displayln (foo-x fn))
> fn)
> -> (check (foo (lambda (x) 3)) 3)
> #

> #

>
> How I imagined this might work is that you would wrap the value so that you can
> only make observations corresponding to the bound. So here you force the `foo`
> to act only as an int function, masking its structness since that's a finer
> distinction than the bound gives you.

A good catch that I hadn’t thought to try yet!

I think the fundamental trickiness here is that any given contract imposes obligations on
both the client and the server. “Real” bounded parametric polymorphism ensures that the
client uses the value only in ways that are guaranteed to work given the server’s obligations
(though this is violated by languages with instanceof or casts). This corresponds to a contract
where the client and server obligations coincide exactly.

The problem here is that many Racket contracts do not have this property, including -> contracts.
A fix to get the desired behavior is probably to write a more explicit contract like:
(and/c (integer? . -> . integer?) (not/c struct?)).
Unfortunately, this doesn’t work because “struct foo” still passes this contract (surprising?! Is there
a way to write such a contract?). In shill, our bounded parametric contracts were specialized only
to capability contracts, which did have the property of coinciding obligations.

While I could imagine implementing a mechanism that turned the server obligations of the bound
into the corresponding client obligations, I think it would would have to be hard-coded to particular
types of contracts. I personally would probably lean to accepting this as a practical deviation from
the “right thing,” similar to dynamic casts in most OO languages.

Along that line, it might be interesting to look where in the Racket contract library this property holds
and where it doesn’t, and whether it makes sense to add additional contracts that enforce stricter
requirements on clients. (It seems that even with regular function contracts I might want to prevent
a callee from monkeying around with the internals of my prop:procedure implemented function.)

> Also it's interesting that only higher-order contracts are accepted as bounds.
> I guess because you need to stamp the value as belonging to X while still
> allowing operations on it? (which you couldn't do on a symbol, say)

Exactly.

[Matthias Felleisen]

Just a quick encouragement, I haven’t absorbed this in detail yet.

When you write ‘higher-order’, do you mean you could use a class
contract to bound the parameter of a mixin? That might expand what
we can do with Asumu’s type system (because we could compile
gradual types to such contracts).

In any case, you guys should spin this off as a separate idea, perhaps
for ICFP or DSL You are a PhD student and Christos is a post-doc. Go
for it.


— Matthias

> --
> 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 racket-dev+...@googlegroups.com.
> To post to this group, send email to racke...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/racket-dev/etPan.56a9bb34.5eb46042.124%40Scotts-MacBook-Pro.local.
> For more options, visit https://groups.google.com/d/optout.

[Scott Moore]

Thanks for the encouragement. :)

Yes, one of the places we had thought to apply it was with class contracts.

It doesn’t work currently because object contracts are a bit too strict in their enforcement:

a contract that specifies #:opaque makes the lack of additional methods an obligation for

the server rather than an obligation for the client not to call them. The opposite behavior

seems more intuitive to me.

For example, in the following scenario it isn’t possible (as far as I could see) to write a

contract that allows a subclass to be used in place of a superclass, but only with the

superclass’s interface. Did I miss a way to write this?

(define one-method%

  (class object%

    (define/public (foo) 'foo)

    (super-new)))

(define two-method%

  (class one-method%

    (inherit foo)

    (define/public (bar) 'bar)

    (super-new)))

(define one (new one-method%))

(define two (new two-method%))

; This contract is too permissive

(define/contract (contract-one-open obj)

  (-> (instanceof/c (class/c [foo (->m symbol?)])) any/c)

  (send obj bar)) ; Use obj as a two-method%

(contract-one-open two) ; => 'bar

; This contract is too strict

(define/contract (contract-one-closed obj)

  (-> (instanceof/c (class/c #:opaque [foo (->m symbol?)])) any/c)

  (send obj foo)) ; Use obj as a one-method%

(contract-one-closed two) ; Pass in a two... rejected because it supports more

; contract-one-closed: contract violation;

;    method bar not specified in contract

To view this discussion on the web visit https://groups.google.com/d/msgid/racket-dev/22703826-72D8-4D05-80E4-F635086EE2D0%40ccs.neu.edu.

[Asumu Takikawa]

On 2016-01-28 21:48:12 -0500, Scott Moore wrote:
> For example, in the following scenario it isn’t possible (as far as I
> could see) to write a
> contract that allows a subclass to be used in place of a superclass, but
> only with the
> superclass’s interface. Did I miss a way to write this?

For your specific example, Typed Racket does not actually compile `Object`
types to `instanceof/c` contracts. Instead, it compiles to a custom TR-defined
object contract that will enforce a more "lazy" form of opaqueness.

i.e., it only errors when you try to call a method you shouldn't be able to
access like `bar`.

You can't actually use the contract TR uses in ordinary Racket programs though
(because they are part of TR's private modules).

Opaque class contracts are only used when a class value itself flows from
untyped to typed.

Cheers,
Asumu

[Asumu Takikawa]

On 2016-01-28 01:54:44 -0500, Scott Moore wrote:
> While I could imagine implementing a mechanism that turned the server
> obligations of the bound into the corresponding client obligations, I think
> it would would have to be hard-coded to particular types of contracts. I
> personally would probably lean to accepting this as a practical deviation
> from the “right thing,” similar to dynamic casts in most OO languages.

I agree that this may be a practical choice, particularly from the perspective
of a (untyped) Racket programmer.

My example mainly comes from my bias as a Typed Racket dev. If TR had more
support for generics/ad-hoc polymorphism and also had bounded polymorphism it
would be important to treat the bound more opaquely.

Even function contracts would be an issue if TR let prop:procedure based
structs be subtypes of the corresponding function type. (right now TR lets you
call such structs as functions but does not encode the subtype relationship)

Cheers,
Asumu