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.
