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 <philnguyen0...@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+unsubscr...@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+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
