www

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

alex.mlish (827B)

      1 #lang s-exp "../../mlish.rkt"
      2 (require "../rackunit-typechecking.rkt")
      3 
      4 ;; the following function def produces error:
      5 ;; define: Function should-err's body (let ((y (f x))) x) has type X, which
      6 ;; does not match given type Y.
      7 ;; TODO: add check-_ rackunit form for functions
      8 #;(define (should-err [x : X] [f : (→ X Y)] -> Y)
      9   (let ([y (f x)])
     10       x))
     11 
     12 (define (try [x : X][f : (→ X Y)] → X)
     13   (let ([y (f x)]) x))
     14 
     15 (check-type try : (→/test X (→ X Y) X))
     16 
     17 (define (accept-A×A [pair : (× A A)] → (× A A))
     18   pair)
     19 
     20 (typecheck-fail (accept-A×A (tup 8 "ate"))
     21  #:with-msg "couldn't unify Int and String\n *expected: \\(× A A\\)\n *given: \\(× Int String\\)")
     22 
     23 (typecheck-fail (ann (accept-A×A (tup 8 "ate")) : (× String String))
     24  #:with-msg "expected: \\(× String String\\)\n *given: \\(× Int String\\)")
     25