commit a41a4cdd625bc2b585c644973425dd5ce6aa9d73
parent 7999f1cc8c4e29e444ee1ff07924afa5ef1876c4
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Fri, 11 Dec 2015 17:01:25 -0500
start exploring (local) inference
Diffstat:
4 files changed, 277 insertions(+), 1 deletion(-)
diff --git a/tapl/infer.rkt b/tapl/infer.rkt
@@ -0,0 +1,80 @@
+#lang s-exp "typecheck.rkt"
+(extends "ext-stlc.rkt" #:except #%app λ → + - void = zero? sub1 add1 not
+ #:rename [~→ ~ext-stlc:→])
+(reuse ∀ ~∀ ∀? Λ #:from "sysf.rkt")
+(reuse cons head tail nil isnil List #:from "stlc+cons.rkt")
+(provide →)
+
+;; a language with partial (local) type inference using bidirectional type checking
+
+(define-syntax → ; wrapping →
+ (syntax-parser
+ [(_ (~and Xs {X:id ...}) . rst)
+ #:when (brace? #'Xs)
+ #'(∀ (X ...) (ext-stlc:→ . rst))]
+ [(_ . rst) #'(∀ () (ext-stlc:→ . rst))]))
+
+(define-primop + : (→ Int Int Int))
+(define-primop - : (→ Int Int Int))
+(define-primop void : (→ Unit))
+(define-primop = : (→ Int Int Bool))
+(define-primop zero? : (→ Int Bool))
+(define-primop sub1 : (→ Int Int))
+(define-primop add1 : (→ Int Int))
+(define-primop not : (→ Bool Bool))
+
+(define-typed-syntax define
+ [(_ x:id e)
+ #:with (e- τ) (infer+erase #'e)
+ #:with y (generate-temporary)
+ #'(begin
+ (define-syntax x (make-rename-transformer (⊢ y : τ)))
+ (define y e-))]
+ [(_ (~and Xs {X:id ...}) (f:id [x:id (~datum :) τ] ... (~datum →) τ_out) e)
+ #:when (brace? #'Xs)
+ #:with g (generate-temporary)
+ #'(begin
+ (define-syntax f (make-rename-transformer (⊢ g : (∀ (X ...) (ext-stlc:→ τ ... τ_out)))))
+ (define g (Λ (X ...) (ext-stlc:λ ([x : τ] ...) e))))]
+ [(_ (f:id [x:id (~datum :) τ] ... (~datum →) τ_out) e)
+ #:with g (generate-temporary)
+ #'(begin
+ (define-syntax f (make-rename-transformer (⊢ g : (→ τ ... τ_out))))
+ (define g (ext-stlc:λ ([x : τ] ...) e)))])
+
+; all λs have type (∀ (X ...) (→ τ_in ... τ_out))
+(define-typed-syntax λ #:datum-literals (:)
+ [(~and fn (_ (x:id ...) e) ~!) ; no annotations
+ #:with given-τ-args (syntax-property #'fn 'given-τ-args)
+ #:fail-unless (syntax-e #'given-τ-args) ; no inferred types or annotations, so error
+ (format "input types for ~a could not be inferred; add annotations"
+ (syntax->datum #'fn))
+ #:with (τ_arg ...) #'given-τ-args
+ #:with [λ- τ_λ] (infer+erase #'(ext-stlc:λ ([x : τ_arg] ...) e))
+ (⊢ λ- : (∀ () τ_λ))]
+ [(_ . rst)
+ #:with [λ- τ_λ] (infer+erase #'(ext-stlc:λ . rst))
+ (⊢ λ- : (∀ () τ_λ))])
+
+(define-typed-syntax #%app
+ [(_ e_fn e_arg ...)
+ #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
+ #:with e_fn_anno (syntax-property #'e_fn 'given-τ-args #'(τ_arg ...))
+; #:with [e_fn- (τ_in ... τ_out)] (⇑ e_fn_anno as →)
+ #:with [e_fn- ((X ...) ((~ext-stlc:→ τ_in ... τ_out)))] (⇑ e_fn_anno as ∀)
+ ; some code duplication
+ #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
+ (string-append
+ (format "~a (~a:~a) Arguments to function ~a have wrong type(s), "
+ (syntax-source stx) (syntax-line stx) (syntax-column stx)
+ (syntax->datum #'e_fn))
+ "or wrong number of arguments:\nGiven:\n"
+ (string-join
+ (map (λ (e t) (format " ~a : ~a" e t)) ; indent each line
+ (syntax->datum #'(e_arg ...))
+ (stx-map type->str #'(τ_arg ...)))
+ "\n" #:after-last "\n")
+ (format "Expected: ~a arguments with type(s): "
+ (stx-length #'(τ_in ...)))
+ (string-join (stx-map type->str #'(τ_in ...)) ", "))
+ (⊢ (#%app e_fn- e_arg- ...) : τ_out)])
diff --git a/tapl/tests/infer-tests.rkt b/tapl/tests/infer-tests.rkt
@@ -0,0 +1,192 @@
+#lang s-exp "../infer.rkt"
+(require "rackunit-typechecking.rkt")
+
+(typecheck-fail (λ (x) x) #:with-msg "add annotations")
+
+; should bidirectional checking work for this case?
+; I think no, since TR doesnt handle it either
+(typecheck-fail (λ (x) (+ x 1)) #:with-msg "add annotations")
+; can't check this case either
+(typecheck-fail ((λ (f) (f 10)) (λ (x) x)) #:with-msg "add annotations")
+
+; stlc+lit tests with app, but infer types (no annotations)
+(check-type ((λ (x) x) 1) : Int ⇒ 1)
+(check-type ((λ (f x y) (f x y)) + 1 2) : Int ⇒ 3)
+(check-type ((λ (x) (+ x x)) 10) : Int ⇒ 20)
+
+(check-type ((λ (x) ((λ (y) y) x)) 10) : Int ⇒ 10)
+
+; top level functions
+(define (f [x : Int] → Int) x)
+(check-type f : (→ Int Int))
+(check-type (f 1) : Int ⇒ 1)
+(typecheck-fail (f (λ ([x : Int]) x)))
+
+(define {X} (g [x : X] → X) x)
+(check-type g : (→ {X} X X))
+
+; --------------------------------------------------
+; all ext-stlc tests should still pass (copied below):
+;; tests for stlc extensions
+;; new literals and base types
+(check-type "one" : String) ; literal now supported
+(check-type #f : Bool) ; literal now supported
+
+(check-type (λ ([x : Bool]) x) : (→ Bool Bool)) ; Bool is now valid type
+
+;; Unit
+(check-type (void) : Unit)
+(check-type void : (→ Unit))
+
+(typecheck-fail
+ ((λ ([x : Unit]) x) 2)
+ #:with-msg
+ "Arguments to function.+have wrong type.+Given:.+Int.+Expected:.+Unit")
+(typecheck-fail
+ ((λ ([x : Unit]) x) void)
+ #:with-msg
+ "Arguments to function.+have wrong type.+Given:.+(→ Unit).+Expected:.+Unit")
+
+(check-type ((λ ([x : Unit]) x) (void)) : Unit)
+
+;; begin
+(check-type (begin 1) : Int)
+
+(typecheck-fail (begin) #:with-msg "expected more terms")
+(typecheck-fail
+ (begin 1 2 3)
+ #:with-msg "Expected expression 1 to have Unit type, got: Int")
+
+(check-type (begin (void) 1) : Int ⇒ 1)
+(check-type ((λ ([x : Int]) (begin (void) x)) 1) : Int)
+(check-type ((λ ([x : Int]) (begin x)) 1) : Int)
+(check-type ((λ ([x : Int]) (begin (begin x))) 1) : Int)
+(check-type ((λ ([x : Int]) (begin (void) (begin (void) x))) 1) : Int)
+(check-type ((λ ([x : Int]) (begin (begin (void) x))) 1) : Int)
+
+;;ascription
+(check-type (ann 1 : Int) : Int ⇒ 1)
+(check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10)
+(typecheck-fail (ann 1 : Bool) #:with-msg "ann: 1 does not have type Bool")
+;ann errs
+(typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
+(typecheck-fail (ann 1 : 1) #:with-msg "not a valid type")
+(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a valid type")
+(typecheck-fail (ann Int : Int) #:with-msg "does not have type Int")
+
+; let
+(check-type (let () (+ 1 1)) : Int ⇒ 2)
+(check-type (let ([x 10]) (+ 1 2)) : Int)
+(check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30)
+(typecheck-fail
+ (let ([x #f]) (+ x 1))
+ #:with-msg
+ "Arguments to function \\+.+have wrong type.+Given:.+Bool.+Int.+Expected:.+Int.+Int")
+(typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))
+ #:with-msg "x: unbound identifier")
+
+(check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21)
+(typecheck-fail
+ (let* ([x #t] [y (+ x 1)]) 1)
+ #:with-msg
+ "Arguments to function \\+.+have wrong type.+Given:.+Bool.+Int.+Expected:.+Int.+Int")
+
+; letrec
+(typecheck-fail
+ (letrec ([(x : Int) #f] [(y : Int) 1]) y)
+ #:with-msg
+ "letrec: type check fail, args have wrong type:\n#f has type Bool, expected Int")
+(typecheck-fail
+ (letrec ([(y : Int) 1] [(x : Int) #f]) x)
+ #:with-msg
+ "letrec: type check fail, args have wrong type:.+#f has type Bool, expected Int")
+
+(check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3)
+
+;; recursive
+(check-type
+ (letrec ([(countdown : (→ Int String))
+ (λ ([i : Int])
+ (if (= i 0)
+ "liftoff"
+ (countdown (- i 1))))])
+ (countdown 10)) : String ⇒ "liftoff")
+
+;; mutually recursive
+(check-type
+ (letrec ([(is-even? : (→ Int Bool))
+ (λ ([n : Int])
+ (or (zero? n)
+ (is-odd? (sub1 n))))]
+ [(is-odd? : (→ Int Bool))
+ (λ ([n : Int])
+ (and (not (zero? n))
+ (is-even? (sub1 n))))])
+ (is-odd? 11)) : Bool ⇒ #t)
+
+;; check some more err msgs
+(typecheck-fail
+ (and "1" #f)
+ #:with-msg "Expected expression \"1\" to have Bool type, got: String")
+(typecheck-fail
+ (and #t "2")
+ #:with-msg
+ "Expected expression \"2\" to have Bool type, got: String")
+(typecheck-fail
+ (or "1" #f)
+ #:with-msg
+ "Expected expression \"1\" to have Bool type, got: String")
+(typecheck-fail
+ (or #t "2")
+ #:with-msg
+ "Expected expression \"2\" to have Bool type, got: String")
+(typecheck-fail
+ (if "true" 1 2)
+ #:with-msg
+ "Expected expression \"true\" to have Bool type, got: String")
+(typecheck-fail
+ (if #t 1 "2")
+ #:with-msg
+ "branches have incompatible types: Int and String")
+
+;; tests from stlc+lit-tests.rkt --------------------------
+; most should pass, some failing may now pass due to added types/forms
+(check-type 1 : Int)
+;(check-not-type 1 : (Int → Int))
+;(typecheck-fail "one") ; literal now supported
+;(typecheck-fail #f) ; literal now supported
+(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))
+(check-not-type (λ ([x : Int]) x) : Int)
+(check-type (λ ([x : Int]) x) : (→ Int Int))
+(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
+(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
+
+(typecheck-fail
+ ((λ ([x : Bool]) x) 1)
+ #:with-msg
+ "Arguments to function.+have wrong type.+Given:.+Int.+Expected:.+Bool")
+;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type
+(typecheck-fail
+ (λ ([f : Int]) (f 1 2))
+ #:with-msg
+ "Expected expression f to have ∀ type, got: Int")
+
+(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
+ : (→ (→ Int Int Int) Int Int Int))
+(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2)
+ : Int ⇒ 3)
+
+(typecheck-fail
+ (+ 1 (λ ([x : Int]) x))
+ #:with-msg
+ "Arguments to function \\+ have wrong type.+Given:\n 1 : Int.+(→ Int Int).+Expected: 2 arguments with type.+Int\\, Int")
+(typecheck-fail
+ (λ ([x : (→ Int Int)]) (+ x x))
+ #:with-msg
+ "Arguments to function \\+ have wrong type.+Given:.+(→ Int Int).+Expected: 2 arguments with type.+Int\\, Int")
+(typecheck-fail
+ ((λ ([x : Int] [y : Int]) y) 1)
+ #:with-msg "Arguments to function.+have.+wrong number of arguments")
+
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
+
diff --git a/tapl/tests/run-all-tests.rkt b/tapl/tests/run-all-tests.rkt
@@ -1,5 +1,8 @@
#lang racket
+;; type inference
+(require "infer-tests.rkt")
+
;; stlc and extensions
(require "stlc-tests.rkt")
(require "stlc+lit-tests.rkt")
diff --git a/tapl/tests/stlc+box-tests.rkt b/tapl/tests/stlc+box-tests.rkt
@@ -34,7 +34,8 @@
;; previous tests: ------------------------------------------------------------
(typecheck-fail (cons 1 2))
-(typecheck-fail (cons 1 nil))
+;(typecheck-fail (cons 1 nil)) ; works now
+(check-type (cons 1 nil) : (List Int))
(check-type (cons 1 (nil {Int})) : (List Int))
(typecheck-fail nil)
(typecheck-fail (nil Int))
