commit f0aba484970548681343ead2c5da8dfda065fe9d
parent 87cf55e7aef4ecf30ef2701ff27fac038321cb4f
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Mon, 29 Feb 2016 14:21:02 -0500
- add folding compuate+instantiate-or-inferral of args in app
- start guard support in match (doesnt work yet)
Diffstat:
3 files changed, 164 insertions(+), 43 deletions(-)
diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
@@ -1,7 +1,7 @@
#lang s-exp "typecheck.rkt"
(require (for-syntax syntax/id-set))
-(extends "ext-stlc.rkt" #:except #%app λ → + - void = zero? sub1 add1 not let
+(extends "ext-stlc.rkt" #:except #%app λ → + - void = zero? sub1 add1 not let and
#:rename [~→ ~ext-stlc:→])
(reuse inst ~∀ ∀ ∀? Λ #:from "sysf.rkt")
(require (only-in "stlc+rec-iso.rkt" case fld unfld μ × ∨ var tup define-type-alias)
@@ -12,9 +12,13 @@
;(provide hd tl nil?)
(provide →)
(provide define-type match)
-(provide (rename-out [ext-stlc:let let]))
+(provide (rename-out [ext-stlc:let let] [ext-stlc:and and]))
-;; ML-like language with no type inference
+;; ML-like language
+;; - top level recursive functions
+;; - user-definable algebraic datatypes
+;; - pattern matching
+;; - (local) type inference
;; type inference constraint solving
(begin-for-syntax
@@ -45,8 +49,41 @@
#:when (free-identifier=? #'y x)
#'τ]
[(_ . rst) (lookup x #'rst)]
- [() false])))
+ [() false]))
+ ;; solve for tyvars Xs used in tys, based on types of args in stx
+ ;; infer types of args left-to-right:
+ ;; - use intermediate results to help infer remaining arg types
+ ;; - short circuit if done early
+ ;; return list of types if success; #f if fail
+ (define (solve Xs tys stx)
+ (define args (stx-cdr stx))
+ (cond
+ [(stx-null? Xs) #'()]
+ [(or (stx-null? args) (not (stx-length=? tys args)))
+ (type-error #:src stx
+ #:msg (mk-app-err-msg stx #:expected tys
+ #:note (format "Could not infer instantiation of polymorphic function ~a."
+ (syntax->datum (stx-car stx)))))]
+ [else
+ (let loop ([a (stx-car args)] [args-rst (stx-cdr args)]
+ [ty (stx-car tys)] [tys-rst (stx-cdr tys)]
+ [old-cs #'()])
+ (define/with-syntax [a- ty_a] (infer+erase a))
+ (define cs
+ (stx-append old-cs (compute-constraints (list (list ty #'ty_a)))))
+ (define maybe-solved
+ (filter (lambda (x) x) (stx-map (λ (X) (lookup X cs)) Xs)))
+ (if (stx-length=? maybe-solved Xs)
+ maybe-solved
+ (if (or (stx-null? args-rst) (stx-null? tys-rst))
+ (type-error #:src stx
+ #:msg (mk-app-err-msg stx #:expected tys #:given (stx-map cadr (infers+erase args))
+ #:note (format "Could not infer instantiation of polymorphic function ~a."
+ (syntax->datum (stx-car stx)))))
+ (loop (stx-car args-rst) (stx-cdr args-rst)
+ (stx-car tys-rst) (stx-cdr tys-rst) cs))))])))
+;; define --------------------------------------------------
(define-typed-syntax define
[(_ x:id e)
#:with (e- τ) (infer+erase #'e)
@@ -88,6 +125,7 @@
;; 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-type --------------------------------------------------
(define-syntax (define-type stx)
(syntax-parse stx
[(_ Name:id . rst)
@@ -141,7 +179,7 @@
"\n"
(format "and be applied to ~a arguments with type(s): "(stx-length #'(τ ...)))
(string-join (stx-map type->str #'(τ ...)) ", ")))]
- [(_ τs e_arg ...)
+ [(C τs e_arg ...)
#:when (brace? #'τs) ; commit to this clause
#:with {~! τ_X:type (... ...)} #'τs
#:with (τ_in:type (... ...)) ; instantiated types
@@ -155,7 +193,7 @@
#'(e_arg ...) #'(τ_in.norm (... ...)))
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in.norm (... ...)))
;; need to duplicate #%app err msg here, to attach additional props
- (mk-app-err-msg stx
+ (mk-app-err-msg #'(C e_arg ...)
#:expected #'(τ_in.norm (... ...)) #:given #'(τ_arg ...)
#:name (format "constructor ~a" 'Cons))
#:with τ_out (syntax-property
@@ -168,31 +206,37 @@
;; 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+)]
- [old-cs #'()])
- (define/with-syntax [a- τ_a] (infer+erase a))
- (define cs (stx-append old-cs (compute-constraints (list (list τ+ #'τ_a)))))
- (define maybe-solved (filter syntax-e (stx-map (λ (y) (lookup y cs)) #'Ys)))
- (if (stx-length=? maybe-solved #'Ys)
- #`(C #,(syntax-property #`{#,@maybe-solved} 'paren-shape #\{) . args) ; loses 'paren-shape
- (if (or (stx-null? a-rst) (stx-null? τ+rst))
- (type-error #:src stx
- #:msg "could not infer types for constructor ~a; add annotations" #'(C . args))
- (loop (stx-car a-rst) (stx-cdr a-rst) (stx-car τ+rst) (stx-cdr τ+rst) cs))))]))
-; #:with ([arg- τarg] (... ...)) (infers+erase #'args)
-; #:with (~Tmp Ys τ+ (... ...)) ((current-type-eval) #'(Tmp (X ...) τ ...))
-; #:with cs (compute-constraints #'((τ+ τarg) (... ...)))
-; #:with (τ_solved (... ...)) (stx-map (λ (y) (lookup y #'cs)) #'Ys)
-; #'(C {τ_solved (... ...)} . args)]))
+ #:with (τ_solved (... ...)) (solve #'Ys #'τs+ stx)
+;; (let loop ([a (stx-car #'args)] [a-rst (stx-cdr #'args)]
+;; [τ+ (stx-car #'τs+)] [τ+rst (stx-cdr #'τs+)]
+;; [old-cs #'()])
+;; (define/with-syntax [a- τ_a] (infer+erase a))
+;; (define cs (stx-append old-cs (compute-constraints (list (list τ+ #'τ_a)))))
+;; (define maybe-solved (filter syntax-e (stx-map (λ (y) (lookup y cs)) #'Ys)))
+;; (if (stx-length=? maybe-solved #'Ys)
+;; #`(C #,(syntax-property #`{#,@maybe-solved} 'paren-shape #\{) . args) ; loses 'paren-shape
+;; (if (or (stx-null? a-rst) (stx-null? τ+rst))
+;; (type-error #:src stx
+;; #:msg "could not infer types for constructor ~a; add annotations" #'(C . args))
+;; (loop (stx-car a-rst) (stx-cdr a-rst) (stx-car τ+rst) (stx-cdr τ+rst) cs))))]))
+;; ; #:with ([arg- τarg] (... ...)) (infers+erase #'args)
+;; ; #:with (~Tmp Ys τ+ (... ...)) ((current-type-eval) #'(Tmp (X ...) τ ...))
+;; ; #:with cs (compute-constraints #'((τ+ τarg) (... ...)))
+;; ; #:with (τ_solved (... ...)) (stx-map (λ (y) (lookup y #'cs)) #'Ys)
+ #'(C {τ_solved (... ...)} . args)]))
...)]))
+;; match --------------------------------------------------
(define-syntax (match stx)
(syntax-parse stx #:datum-literals (with ->)
[(_ e with . clauses)
#:fail-when (null? (syntax->list #'clauses)) "no clauses"
- #:with ([Clause:id x ... -> e_c_un] ...) (stx-sort #'clauses symbol<?) ; un = unannotated with expected ty
+ #:with ([Clause:id x ...
+ (~optional (~seq #:when e_guard) #:defaults ([e_guard #'#t]))
+ -> e_c_un] ...) ; un = unannotated with expected ty
+ (stx-sort #'clauses symbol<?)
#:with [e- τ_e] (infer+erase #'e)
+ #:with z (generate-temporary)
#:with ((Cons Cons2 [fld (~datum :) τ] ...) ...) (stx-sort (syntax-property #'τ_e 'variants) symbol<?)
#:fail-unless (= (stx-length #'(Clause ...)) (stx-length #'(Cons ...))) "wrong number of case clauses"
#:fail-unless (typechecks? #'(Clause ...) #'(Cons ...)) "case clauses not exhaustive"
@@ -211,7 +255,12 @@
;; #:with (acc ...) (syntax-property #'τ_e 'accessors)
;; #:with (_ (x_out ...) e_out τ_out) (stx-assoc #'C #'((Clause (x- ...) e_c- τ_ec) ...))
#:with τ_out (stx-car #'(τ_ec ...))
- (⊢ (cond [(Cons? e-) (let ([x- (acc e-)] ...) e_c-)] ...) : τ_out)]))
+ (⊢ (let ([z e-])
+ (cond
+ [(and (Cons? z)
+ (let ([x- (acc z)] ...) e_guard))
+ (let ([x- (acc z)] ...) e_c-)] ...))
+ : τ_out)]))
#;(define-syntax lifted→ ; wrap → with ∀
(syntax-parser
@@ -258,27 +307,58 @@
[(_ f . args)
#'(ext-stlc:#%app (inst f) . args)])
+;; #%app --------------------------------------------------
(define-typed-syntax #%app
- [(_ e_fn e_arg ...) ; infer args first
- #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
+ [(_ e_fn e_arg ...)
+ ;; ) compute fn type (ie ∀ and →)
+ ;; - use multiple steps to produce better err msg
;#: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
- (mk-app-err-msg stx #:expected #'(τ_inX ...) #:given #'(τ_arg ...)
+ #:with (~∀ Xs (~ext-stlc:→ τ_inX ... τ_outX)) #'τ_fn
+ #:with (τ_solved ...) (solve #'Xs #'(τ_inX ...) (syntax/loc stx (e_fn e_arg ...)))
+ ;; ) instantiate polymorphic fn type
+ ;; #:with cs (compute-constraints #'((τ_inX τ_arg) ...))
+ ;; #:with (τ_solved ...) (filter (λ (x) x) (stx-map (λ (y) (lookup y #'cs)) #'(X ...)))
+ ;; #:fail-unless (stx-length=? #'(X ...) #'(τ_solved ...))
+ ;; (mk-app-err-msg stx #:expected #'(τ_inX ...) #:given #'(τ_arg ...)
+ ;; #:note "Could not infer instantiation of polymorphic function.")
+ #:with (τ_in ... τ_out) (stx-map
+ (λ (t) (substs #'(τ_solved ...) #'Xs t))
+ #'(τ_inX ... τ_outX))
+ #:fail-unless (stx-length=? #'(τ_inX ...) #'(e_arg ...))
+ (mk-app-err-msg stx #:expected #'(τ_inX ...)
+; #:given #'(τ_arg ...)
#:note "Wrong number of arguments.")
- #:with cs (compute-constraints #'((τ_inX τ_arg) ...))
- #:with (τ_solved ...) (filter (λ (x) x) (stx-map (λ (y) (lookup y #'cs)) #'(X ...)))
- #:fail-unless (stx-length=? #'(X ...) #'(τ_solved ...))
- (mk-app-err-msg stx #:expected #'(τ_inX ...) #:given #'(τ_arg ...)
- #:note "Could not infer instantiation of polymorphic function.")
- #:with (τ_in ... τ_out) (stx-map (λ (t) (substs #'(τ_solved ...) #'(X ...) t)) #'(τ_inX ... τ_outX))
- ; some code duplication
+ ;; ) compute argument types; (possibly) double-expand args (for now)
+ #:with ([e_arg- τ_arg] ...) (infers+erase (stx-map add-expected-ty #'(e_arg ...) #'(τ_in ...)))
+ ;; ) arity check
+ #:fail-unless (stx-length=? #'(τ_inX ...) #'(e_arg ...))
+ (mk-app-err-msg stx #:expected #'(τ_inX ...)
+ #:given #'(τ_arg ...)
+ #:note "Wrong number of arguments.")
+ ;; ) typecheck args
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
(mk-app-err-msg stx #:given #'(τ_arg ...) #:expected #'(τ_in ...))
(⊢ (#%app e_fn- e_arg- ...) : τ_out)])
+
+
+ ;; ;; 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+)]
+ ;; [old-cs #'()])
+ ;; (define/with-syntax [a- τ_a] (infer+erase a))
+ ;; (define cs (stx-append old-cs (compute-constraints (list (list τ+ #'τ_a)))))
+ ;; (define maybe-solved (filter syntax-e (stx-map (λ (y) (lookup y cs)) #'Ys)))
+ ;; (if (stx-length=? maybe-solved #'Ys)
+ ;; #`(C #,(syntax-property #`{#,@maybe-solved} 'paren-shape #\{) . args) ; loses 'paren-shape
+ ;; (if (or (stx-null? a-rst) (stx-null? τ+rst))
+ ;; (type-error #:src stx
+ ;; #:msg "could not infer types for constructor ~a; add annotations" #'(C . args))
+ ;; (loop (stx-car a-rst) (stx-cdr a-rst) (stx-car τ+rst) (stx-cdr τ+rst) cs))))]))
+
diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt
@@ -78,7 +78,14 @@
#:note [note ""]
#:name [name #f])
(syntax-parse stx
- [(_ e_fn e_arg ...)
+ [(app . rst)
+ #:when (not (equal? '#%app (syntax->datum #'app)))
+ (mk-app-err-msg #'(#%app app . rst)
+ #:expected expected-τs
+ #:given given-τs
+ #:note note
+ #:name name)]
+ [(app e_fn e_arg ...)
(define fn-name
(if name name
(format "function ~a"
@@ -93,7 +100,9 @@
(string-join
(map (λ (e t) (format " ~a : ~a" e t)) ; indent each line
(syntax->datum #'(e_arg ...))
- (stx-map type->str given-τs))
+ (if (stx-length=? #'(e_arg ...) given-τs)
+ (stx-map type->str given-τs)
+ (stx-map (lambda (e) "?") #'(e_arg ...))))
"\n")
"\n")]))
diff --git a/tapl/tests/mlish-tests.rkt b/tapl/tests/mlish-tests.rkt
@@ -28,7 +28,7 @@
(typecheck-fail (g2 1)
#:with-msg
(expected "(List X)" #:given "Int"
- #:note "Could not infer instantiation of polymorphic function"))
+ #:note "Could not infer instantiation of polymorphic function"))
;; todo? allow polymorphic nil?
(check-type (g2 (Nil {Int})) : (List Int) ⇒ (Nil {Int}))
@@ -68,7 +68,39 @@
(match lst with
[Nil -> Nil]
[Cons x xs -> (Cons (f x) (map f xs))]))
-
+(check-type map : (→ (→ X Y) (List X) (List Y)))
+(check-type map : (→ (→ Y X) (List Y) (List X)))
+(check-type map : (→ (→ A B) (List A) (List B)))
+(check-not-type map : (→ (→ A B) (List B) (List A)))
+(check-not-type map : (→ (→ X X) (List X) (List X))) ; only 1 bound tyvar
+
+; nil without annotation tests fn-first, left-to-right arg inference
+; does work yet, need to add left-to-right inference in #%app
+(check-type (map add1 Nil) : (List Int) ⇒ (Nil {Int}))
+(check-type (map add1 (Cons 1 (Cons 2 (Cons 3 Nil))))
+ : (List Int) ⇒ (Cons 2 (Cons 3 (Cons 4 Nil))))
+(typecheck-fail (map add1 (Cons "1" Nil)))
+ ;#:with-msg (expected "Int" #:given "String")) ; TODO: fix err msg
+(check-type (map (λ ([x : Int]) (+ x 2)) (Cons 1 (Cons 2 (Cons 3 Nil))))
+ : (List Int) ⇒ (Cons 3 (Cons 4 (Cons 5 Nil))))
+;; ; doesnt work yet: all lambdas need annotations
+;; (check-type (map (λ (x) (+ x 2)) (list 1 2 3)) : (List Int) ⇒ (list 3 4 5))
+
+(define (filter [p? : (→ X Bool)] [lst : (List X)] → (List X))
+ (match lst with
+ [Nil -> Nil]
+ [Cons x xs -> (if (p? x)
+ (Cons x (filter p? xs))
+ (filter p? xs))]))
+(check-type (filter zero? Nil) : (List Int) ⇒ (Nil {Int}))
+(check-type (filter zero? (Cons 1 (Cons 2 (Cons 3 Nil))))
+ : (List Int) ⇒ (Nil {Int}))
+(check-type (filter zero? (Cons 0 (Cons 1 (Cons 2 Nil))))
+ : (List Int) ⇒ (Cons 0 Nil))
+(check-type (filter (λ ([x : Int]) (not (zero? x))) (Cons 0 (Cons 1 (Cons 2 Nil))))
+ : (List Int) ⇒ (Cons 1 (Cons 2 Nil)))
+; doesnt work yet: all lambdas need annotations
+;(check-type (filter (λ (x) (not (zero? x))) (list 0 1 2)) : (List Int) ⇒ (list 1 2))
;; end infer.rkt tests --------------------------------------------------
@@ -311,7 +343,7 @@
#:with-msg (expected "Int, Int" #:given "(→ Int Int), (→ Int Int)"))
(typecheck-fail
((λ ([x : Int] [y : Int]) y) 1)
- #:with-msg (expected "Int, Int" #:given "Int"
+ #:with-msg (expected "Int, Int" #:given "1"
#:note "Wrong number of arguments"))
(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
