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.