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 > On Jan 28, 2016, at 1:54 AM, Scott Moore <[email protected]> wrote: > > > 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 > ([email protected](mailto:[email protected])) 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. > > > -- > 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.56a9bb34.5eb46042.124%40Scotts-MacBook-Pro.local. > For more options, visit https://groups.google.com/d/optout. -- 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/22703826-72D8-4D05-80E4-F635086EE2D0%40ccs.neu.edu. For more options, visit https://groups.google.com/d/optout.
