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
> <javascript:>> 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 <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.
