commit 893d457bad69f85ece8f4d30211dce65c7c13ec4
parent 6fa962f83f4bfe2e1404611f14b66bdb3241affe
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Thu, 25 Feb 2016 17:02:46 -0500
add top lvl defines and infer instantation
- need to err msg when instantiation fails
Diffstat:
2 files changed, 171 insertions(+), 11 deletions(-)
diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
@@ -3,9 +3,9 @@
(extends "ext-stlc.rkt" #:except #%app λ → + - void = zero? sub1 add1 not let
#:rename [~→ ~ext-stlc:→])
-(require (only-in "sysf.rkt" inst ~∀ ∀ Λ))
+(reuse inst ~∀ ∀ ∀? Λ #:from "sysf.rkt")
(require (only-in "stlc+rec-iso.rkt" case fld unfld μ × ∨ var tup define-type-alias)
- (prefix-in stlc+rec-iso: (only-in "stlc+rec-iso.rkt" define)))
+ #;(prefix-in stlc+rec-iso: (only-in "stlc+rec-iso.rkt" define)))
;(reuse cons [head hd] [tail tl] nil [isnil nil?] List ~List list #:from "stlc+cons.rkt")
;(reuse tup × proj #:from "stlc+tup.rkt")
;(reuse define-type-alias #:from "stlc+reco+var.rkt")
@@ -27,7 +27,7 @@
; should only be monomorphic?
[((~∀ () (~ext-stlc:→ τ1 ...)) (~∀ () (~ext-stlc:→ τ2 ...)))
(compute-constraints #'((τ1 τ2) ...))]
- [_ #:when (displayln τ1-τ2) #'()]))
+ [_ #:when #t #;(printf "shouldnt get here. could not unify: ~a\n" τ1-τ2) #'()]))
(define (compute-constraints τs)
;(printf "constraints: ~a\n" (syntax->datum τs))
(stx-appendmap compute-constraint τs))
@@ -47,6 +47,44 @@
[(_ . rst) (lookup x #'rst)]
[() false])))
+(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-))]
+ ; explicit "forall"
+ #;[(_ (~and Xs {X:id ...}) (f:id [x:id (~datum :) τ] ... (~datum →) τ_out) e)
+ #:when (brace? #'Xs)
+ #:with g (generate-temporary #'f)
+ #:with e_ann #'(add-expected e τ_out)
+ #'(begin
+ (define-syntax f (make-rename-transformer (⊢ g : (∀ (X ...) (ext-stlc:→ τ ... τ_out)))))
+ (define g (Λ (X ...) (ext-stlc:λ ([x : τ] ...) e_ann))))]
+ [(_ (f:id [x:id (~datum :) τ] ... (~datum →) τ_out) e)
+ #:when (displayln #'f)
+ #:with Ys
+ (let L ([Xs #'()]) ; compute unbound ids; treat as tyvars
+ (with-handlers
+ ([exn:fail:syntax:unbound?
+ (λ (e)
+ (define X (stx-car (exn:fail:syntax-exprs e)))
+ ; X is tainted, so need to launder it
+ (define Y (datum->syntax #'f (syntax->datum X)))
+ (L (cons Y Xs)))])
+ ((current-type-eval) #`(∀ #,Xs (ext-stlc:→ τ ... τ_out)))
+ Xs))
+ #:when (displayln #'Ys)
+ #:with g (generate-temporary #'f)
+ #:with e_ann #'(add-expected e τ_out)
+ #`(begin
+ (define-syntax f
+ (make-rename-transformer (⊢ g : (∀ Ys (ext-stlc:→ τ ... τ_out)))))
+ (define g
+ (Λ Ys (ext-stlc:λ ([x : τ] ...) e_ann))))])
+;
+;; internal form used to expand many types at once under the same context
(define-type-constructor Tmp #:arity >= 0 #:bvs >= 0) ; need a >= 0 arity
(define-syntax (define-type stx)
@@ -135,7 +173,8 @@
(⊢ (StructName e_arg- ...) : τ_out)]
[(C . args) #:when (stx-null? #'(X ...)) #'(C {} . args)] ; no tyvars, no annotations
[(C . args) ; no type annotations, must infer instantiation
- ;; infer instantiation types from args left-to-right, short-circuit if done early
+ ;; infer instantiation types from args left-to-right,
+ ;; short-circuit if done early, and use result to help infer remaining args
#:with (~Tmp Ys . τs+) ((current-type-eval) #'(Tmp (X ...) τ ...))
(let loop ([a (stx-car #'args)] [a-rst (stx-cdr #'args)]
[τ+ (stx-car #'τs+)] [τ+rst (stx-cdr #'τs+)]
@@ -173,10 +212,28 @@
#:with (acc ...) (syntax-property #'τ_e 'accessors)
(⊢ (let ([x_out (acc e-)] ...) e_out) : τ_out)]))
-(define-syntax lifted→ ; wrap → with ∀
+#;(define-syntax lifted→ ; wrap → with ∀
(syntax-parser
[(_ . rst) #'(∀ () (ext-stlc:→ . rst))]))
+(define-syntax lifted→ ; wrapping →
+ (syntax-parser
+ #;[(_ (~and Xs {X:id ...}) . rst)
+ #:when (brace? #'Xs)
+ #:when (with-handlers ([exn:fail:syntax:unbound? (λ (e) (displayln (exn:fail:syntax-exprs e)))])
+ ((current-type-eval) #'(ext-stlc:→ . rst)))
+ #'(∀ (X ...) (ext-stlc:→ . rst))]
+ [(_ . rst)
+ (let L ([Xs #'()]) ; compute unbound ids; treat as tyvars
+ (with-handlers ([exn:fail:syntax:unbound?
+ (λ (e)
+ (define X (stx-car (exn:fail:syntax-exprs e)))
+ ; X is tainted, so need to launder it
+ (define Y (datum->syntax #'rst (syntax->datum X)))
+ (L (cons Y Xs)))])
+ ((current-type-eval) #`(∀ #,Xs (ext-stlc:→ . rst)))))]))
+ ;#'(∀ () (ext-stlc:→ . rst))
+; redefine these to use lifted→
(define-primop + : (lifted→ Int Int Int))
(define-primop - : (lifted→ Int Int Int))
(define-primop void : (lifted→ Unit))
@@ -188,14 +245,62 @@
(define-primop abs : (lifted→ Int Int))
-; all λs have type (∀ (X ...) (→ τ_in ... τ_out))
+; all λs have type (∀ (X ...) (→ τ_in ... τ_out)), even monomorphic fns
(define-typed-syntax liftedλ #:export-as λ #:datum-literals (:)
[(_ . rst)
#'(Λ () (ext-stlc:λ . rst))])
-(define-typed-syntax new-app #:export-as #%app
+
+#;(define-typed-syntax new-app #:export-as #%app
[(_ τs f . args)
#:when (brace? #'τs)
#'(ext-stlc:#%app (inst f . τs) . args)]
[(_ f . args)
#'(ext-stlc:#%app (inst f) . args)])
+
+(define-typed-syntax #%app
+ [(_ e_fn e_arg ...) ; infer args first
+ #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
+ ;#:with [e_fn- ((X ...) ((~ext-stlc:→ τ_inX ... τ_outX)))] (⇑ e_fn as ∀)
+ ;#:with [e_fn- (~∀ (X ...) (~ext-stlc:→ τ_inX ... τ_outX))] (infer+erase #'e_fn)
+ ;; infer type step-by-step to produce better err msg
+ #:with [e_fn- τ_fn] (infer+erase #'e_fn)
+ #:fail-unless (and (∀? #'τ_fn) (syntax-parse #'τ_fn [(~∀ _ (~ext-stlc:→ . args)) #t][_ #f]))
+ (format "Expected expression ~a to have → type, got: ~a"
+ (syntax->datum #'e_fn) (type->str #'τ_fn))
+ #:with (~∀ (X ...) (~ext-stlc:→ τ_inX ... τ_outX)) #'τ_fn
+ #:fail-unless (stx-length=? #'(τ_inX ...) #'(e_arg ...)) ; check arity
+ (string-append
+ (format "~a (~a:~a) Wrong number of arguments given to function ~a.\n"
+ (syntax-source stx) (syntax-line stx) (syntax-column stx)
+ (syntax->datum #'e_fn))
+ (format "Expected: ~a arguments with types: "
+ (stx-length #'(τ_inX ...)))
+ (string-join (stx-map type->str #'(τ_inX ...)) ", " #:after-last "\n")
+ "Given:\n"
+ (string-join
+ (map (λ (e t) (format " ~a : ~a" e t)) ; indent each line
+ (syntax->datum #'(e_arg ...))
+ (stx-map type->str #'(τ_arg ...)))
+ "\n"))
+ #:with cs (compute-constraints #'((τ_inX τ_arg) ...))
+ #:with (τ_solved ...) (filter (λ (x) x) (stx-map (λ (y) (lookup y #'cs)) #'(X ...)))
+ #:fail-unless (stx-length=? #'(X ...) #'(τ_solved ...))
+ (format "could not instantiate polymorphic fn ~a" (syntax->datum #'e_fn))
+ #:with (τ_in ... τ_out) (stx-map (λ (t) (substs #'(τ_solved ...) #'(X ...) t)) #'(τ_inX ... τ_outX))
+ ; some code duplication
+ #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
+ (string-append
+ (format "~a (~a:~a) Arguments to function ~a have wrong type(s).\n"
+ (syntax-source stx) (syntax-line stx) (syntax-column stx)
+ (syntax->datum #'e_fn))
+ "Given:\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/mlish-tests.rkt b/tapl/tests/mlish-tests.rkt
@@ -1,6 +1,64 @@
#lang s-exp "../mlish.rkt"
(require "rackunit-typechecking.rkt")
+(define (recf [x : Int] → Int) (recf x))
+
+;; tests more or less copied from infer-tests.rkt ------------------------------
+;; top-level defines
+(define (f [x : Int] → Int) x)
+(check-type f : (→ Int Int))
+(check-type (f 1) : Int ⇒ 1)
+(typecheck-fail (f (λ ([x : Int]) x)))
+
+(define (g [x : X] → X) x)
+(check-type g : (→ X X))
+
+; (inferred) polymorpic instantiation
+(check-type (g 1) : Int ⇒ 1)
+(check-type (g #f) : Bool ⇒ #f) ; different instantiation
+(check-type (g add1) : (→ Int Int))
+(check-type (g +) : (→ Int Int Int))
+
+; function polymorphic in list element
+(define-type (List X)
+ (Nil)
+ (Cons X (List X)))
+
+(define (g2 [lst : (List X)] → (List X)) lst)
+(check-type g2 : (→ (List X) (List X)))
+(typecheck-fail (g2 1) #:with-msg "Expected.+arguments with type.+(List X)")
+;(check-type (g2 (Nil {Int})) : (List Int) ⇒ (Nil {Int}))
+;(check-type (g2 (Nil {Bool})) : (List Bool) ⇒ (Nil {Bool}))
+;(check-type (g2 (Nil {(List Int)})) : (List (List Int)) ⇒ (Nil {(List Int)}))
+;(check-type (g2 (Nil {(→ Int Int)})) : (List (→ Int Int)) ⇒ (Nil {(List (→ Int Int))}))
+;(check-type (g2 (Cons 1 Nil)) : (List Int) ⇒ (Cons 1 Nil))
+;(check-type (g2 (Cons "1" Nil)) : (List String) ⇒ (Cons "1" Nil))
+
+;(define (g3 [lst : (List X)] → X) (hd lst)) ; cant type this fn (what to put for nil case)
+;(check-type g3 : (→ {X} (List X) X))
+;(check-type g3 : (→ {A} (List A) A))
+;(check-not-type g3 : (→ {A B} (List A) B))
+;(typecheck-fail (g3) #:with-msg "Expected.+arguments with type.+List") ; TODO: more precise err msg
+;(check-type (g3 (nil {Int})) : Int) ; runtime fail
+;(check-type (g3 (nil {Bool})) : Bool) ; runtime fail
+;(check-type (g3 (cons 1 nil)) : Int ⇒ 1)
+;(check-type (g3 (cons "1" nil)) : String ⇒ "1")
+
+; recursive fn
+;(define (recf [x : Int] → Int) (recf x))
+;(check-type recf : (→ Int Int))
+;
+;(define (countdown [x : Int] → Int)
+; (if (zero? x)
+; 0
+; (countdown (sub1 x))))
+;(check-type (countdown 0) : Int ⇒ 0)
+;(check-type (countdown 10) : Int ⇒ 0)
+;(typecheck-fail (countdown "10") #:with-msg "Arguments.+have wrong type")
+
+;; end infer.rkt tests --------------------------------------------------
+
+;; algebraic data types
(define-type IntList
INil
(ConsI Int IntList))
@@ -17,9 +75,6 @@
[ConsI x xs -> 2]) : Int ⇒ 2)
(typecheck-fail (match 1 with [INil -> 1]))
-(define-type (List X)
- (Nil)
- (Cons X (List X)))
;; annotated
(check-type (Nil {Int}) : (List Int))
(check-type (Cons {Int} 1 (Nil {Int})) : (List Int))
@@ -236,7 +291,7 @@
"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")
+ #:with-msg "Wrong number of arguments given to function")
(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
