It looks like a more general issue we have is that arguments are sometimes
unexpectedly unsealed and prone to inspection by arbitrary code in
contracts, like `->i`'s range or a second conjunct to `and/c`.
On Wednesday, January 17, 2018 at 11:45:41 AM UTC-5, Philip McGrath wrote:
>
> Of course, it blames the right party only if the party implementing the
> contract is the same as the party implementing `bad-h`. This example blames
> `third-party` for what we really want to hold `(definition bad-h)`
> responsible for:
> #lang racket
>
> (module third-party racket
> (provide the-contract)
> (define the-contract
> (parametric->/c
> {α}
> (->i ([x α]
> [P (-> α contract?)]
> [f {P} (->d ([x α])
> [_ (P x)])])
> [_ {P x} (P x)]))))
> (require 'third-party)
>
> (define/contract bad-h
> the-contract
> (λ (x P f)
> (f 'not-α)))
>
> (bad-h 42 (λ _ string?) number->string)
>
> -Philip
>
> On Wed, Jan 17, 2018 at 9:08 AM, Philip McGrath <phi...@philipmcgrath.com
> <javascript:>> wrote:
>
>> I noticed that this sort of works:
>> (define/contract h
>> (parametric->/c
>> {α}
>> (->i ([x α]
>> [P (-> α contract?)]
>> [f {P} (->d ([x α])
>> [_ (P x)])])
>> [_ {P x} (P x)]))
>> (λ (x P f)
>> (f x)))
>>
>> (h 42 (λ _ string?) number->string)
>>
>> The "sort of" part is if you have a violation, e.g.
>> (define/contract bad-h
>> (parametric->/c
>> {α}
>> (->i ([x α]
>> [P (-> α contract?)]
>> [f {P} (->d ([x α])
>> [_ (P x)])])
>> [_ {P x} (P x)]))
>> (λ (x P f)
>> (f 'not-α)))
>>
>> (bad-h 42 (λ _ string?) number->string)
>>
>> Here the violation is reported in terms of the call to `P` in the range
>> of the `->d`, when in principle one would want it to be in terms of calling
>> `f` with a bad argument. But it does blame the right party.
>>
>> -Philip
>>
>> On Wed, Jan 17, 2018 at 8:52 AM, Robby Findler <
>> ro...@eecs.northwestern.edu <javascript:>> wrote:
>>
>>> My guess is that something more subtle has to happen for the "indy"
>>> part of parameteric contracts (but that really is just a guess).
>>>
>>> Robby
>>>
>>>
>>> On Wed, Jan 17, 2018 at 8:49 AM, Phil Nguyen <philngu...@gmail.com
>>> <javascript:>> wrote:
>>> > It doesn't seem like an implementation bug to me. I mean if we try to
>>> follow
>>> > the usual rule of sealing/unsealing, it makes sense. I just can't
>>> pinpoint
>>> > which part of the contracts I need to fix to be able to express the
>>> > enforcement.
>>> >
>>> > On Wednesday, January 17, 2018 at 9:31:25 AM UTC-5, Robby Findler
>>> wrote:
>>> >>
>>> >> I am not sure, but my first guess would be that it is a bug in the
>>> >> contract system (due to a lack of understanding of what to do by me),
>>> >> not that it is impossible to do this with dynamic sealing.
>>> >>
>>> >> Robby
>>> >>
>>> >>
>>> >> On Tue, Jan 16, 2018 at 2:34 PM, Phil Nguyen <philngu...@gmail.com>
>>> wrote:
>>> >> > The following function with its contract will crash because when
>>> >> > composing
>>> >> > the range (P x), the seal around x is already unwrapped:
>>> >> > (define/contract f
>>> >> > (parametric->/c (α) (->i ([x α]
>>> >> > [P (α . -> . contract?)]
>>> >> > [f (P) (->i ([x α]) (_ (x) (P x)))])
>>> >> > (_ (P x) (P x))))
>>> >> > (λ (x P f) (f x)))
>>> >> > (f 42 (λ _ string?) number->string)
>>> >> >
>>> >> > ; f: broke its own contract
>>> >> > ; promised: α
>>> >> > ; produced: 42
>>> >> > ; in: the 1st argument of
>>> >> > ; the P argument of
>>> >> > ; (parametric->/c
>>> >> > ; (α)
>>> >> > ; (->i
>>> >> > ; ((x α)
>>> >> > ; (P (-> α contract?))
>>> >> > ; (f (P) (->i ... ...)))
>>> >> > ; (_ (P x) (P x))))
>>> >> >
>>> >> > Is it possible to express this kind of enforcement using parametric
>>> >> > contracts? (For example, a contract that enforces something similar
>>> to
>>> >> > the
>>> >> > type of a generated induction principle for a datatype in a proof
>>> >> > assistant)
>>> >> >
>>> >> > It's possible to construct a term of a corresponding type in a
>>> >> > dependently
>>> >> > typed language:
>>> >> > example: ∀ {α : Type}
>>> >> > (x: α)
>>> >> > (P: α → Type)
>>> >> > (f: (∀ (x: α), P x)),
>>> >> > (P x) :=
>>> >> > assume _ x _ f, f x
>>> >> >
>>> >> > --
>>> >> > You received this message because you are subscribed to the Google
>>> >> > Groups
>>> >> > "Racket Users" group.
>>> >> > To unsubscribe from this group and stop receiving emails from it,
>>> send
>>> >> > an
>>> >> > email to racket-users...@googlegroups.com.
>>> >> > For more options, visit https://groups.google.com/d/optout.
>>> >
>>> > --
>>> > You received this message because you are subscribed to the Google
>>> Groups
>>> > "Racket Users" group.
>>> > To unsubscribe from this group and stop receiving emails from it, send
>>> an
>>> > email to racket-users...@googlegroups.com <javascript:>.
>>> > For more options, visit https://groups.google.com/d/optout.
>>>
>>> --
>>> You received this message because you are subscribed to the Google
>>> Groups "Racket Users" group.
>>> To unsubscribe from this group and stop receiving emails from it, send
>>> an email to racket-users...@googlegroups.com <javascript:>.
>>> For more options, visit https://groups.google.com/d/optout.
>>>
>>
>>
>
--
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
