www

Unnamed repository; edit this file 'description' to name the repository.
Log | Files | Refs | README

value-restriction-example.mlish (783B)

      1 #lang s-exp "../../mlish.rkt"
      2 (require "../rackunit-typechecking.rkt")
      3 
      4 (define-type (Option X)
      5   None
      6   (Some X))
      7 
      8 (define (make-f → (→ A A))
      9   (let ([r (ref (None {A}))])
     10     (λ (x)
     11       (let ([y (deref r)])
     12         (begin
     13           (:= r (Some x))
     14           (match y with
     15             [None -> x]
     16             [Some y -> y]))))))
     17 ;; This has to fail, because if could succeed with the type (→ A A),
     18 ;; then it could cause unsoundness.
     19 (typecheck-fail (make-f) #:with-msg "Could not infer instantiation of polymorphic function make-f.")
     20 ; ;; If f were defined as the result of (make-f), then it would result
     21 ; ;; in unsoundess if these two expressions were also accepted:
     22 ; (f 13)
     23 ; ;; Because this would typecheck as a String even though it returns 13, an Int:
     24 ; (f "foo")
     25