commit 71d65e1a44b73982be5a90e1676c9c7d30e541e2
parent 4d8f904e70efa51cf5d5a22aac3e6580d728e95c
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Thu, 21 Aug 2014 13:31:11 -0400
stlc, sysf: make function tycon infix instead of prefix
- TODO: typecheck uses -> as datum-literal because it can't see the
actual literal, fix this
Diffstat:
6 files changed, 79 insertions(+), 66 deletions(-)
diff --git a/stlc-tests.rkt b/stlc-tests.rkt
@@ -6,19 +6,19 @@
(check-type-and-result ((λ ([x : Int]) (+ x 1)) 10) : Int => 11)
; check fns with literal or id bodies
-(check-type (λ ([x : Int]) x) : (→ Int Int))
-(check-type (λ ([x : Unit] [y : Int]) x y) : (→ Unit Int Int))
+(check-type (λ ([x : Int]) x) : (Int → Int))
+(check-type (λ ([x : Unit] [y : Int]) x y) : (Unit Int → Int))
;; check fns with multi-expr body
-(check-type (λ ([x : Int]) (void) x) : (→ Int Int))
+(check-type (λ ([x : Int]) (void) x) : (Int → Int))
(check-type-error (λ ([x : Int]) 1 x))
-(check-type (λ ([x : Int]) (void) (void) x) : (→ Int Int))
+(check-type (λ ([x : Int]) (void) (void) x) : (Int → Int))
; HO fn
-(check-type-and-result ((λ ([f : (→ Int Int)]) (f 10)) (λ ([x : Int]) (+ x 1))) : Int => 11)
-(check-type (λ ([f : (→ Int Int)]) (f 10)) : (→ (→ Int Int) Int))
-(check-type (λ ([f : (→ Int Int)]) (λ ([x : Int]) (f (f x)))) : (→ (→ Int Int) (→ Int Int)))
-(check-type-error (λ (f : (→ Int Int)) (λ (x : String) (f (f x)))))
+(check-type-and-result ((λ ([f : (Int → Int)]) (f 10)) (λ ([x : Int]) (+ x 1))) : Int => 11)
+(check-type (λ ([f : (Int → Int)]) (f 10)) : ((Int → Int) → Int))
+(check-type (λ ([f : (Int → Int)]) (λ ([x : Int]) (f (f x)))) : ((Int → Int) → (Int → Int)))
+(check-type-error (λ (f : (Int → Int)) (λ (x : String) (f (f x)))))
;; shadowed var
(check-type-error ((λ ([x : Int]) ((λ ([x : String]) x) x)) 10))
@@ -55,10 +55,10 @@
(check-type-and-result (begin (+ 1 2)) : Int => 3)
(check-type-error (begin 1 2))
-(check-type (λ ([x : Int]) (void) (+ x 1)) : (→ Int Int))
+(check-type (λ ([x : Int]) (void) (+ x 1)) : (Int → Int))
(check-type-error (λ ([x : Int]) 1 1))
-(check-type (λ ([x : Int] [y : Int]) (+ x y)) : (→ Int Int Int))
-(check-type-and-result ((λ ([a : Int] [b : Int] [c : Int]) (void) (void) (+ a b c)) 1 2 3)
+(check-type (λ ([x : Int] [y : Int]) (+ x y)) : (Int Int → Int))
+(check-type-and-result ((λ ([a : Int] [b : Int] [c : Int]) (void) (void) (+ a (+ b c))) 1 2 3)
: Int => 6)
; define
@@ -81,7 +81,7 @@
;;; recursive fn
(define (add1 [x : Int]) : Int
(+ x 1))
-(define (map [f : (→ Int Int)] [lst : (Listof Int)]) : (Listof Int)
+(define (map [f : (Int → Int)] [lst : (Listof Int)]) : (Listof Int)
(if (null? {Int} lst)
(null {Int})
(cons {Int} (f (first {Int} lst)) (map f (rest {Int} lst)))))
@@ -119,7 +119,7 @@
(check-type-and-result (Cons 1 (Null)) : IntList => (Cons 1 (Null)))
(check-type-error (Cons "one" (Null)))
(check-type-error (Cons 1 2))
-(define (map/IntList [f : (→ Int Int)] [lst : IntList]) : IntList
+(define (map/IntList [f : (Int → Int)] [lst : IntList]) : IntList
(cases lst
[Null () (Null)]
[Cons (x xs) (Cons (f x) (map/IntList f xs))]))
@@ -129,7 +129,7 @@
: IntList => (Cons 3 (Cons 2 (Null))))
(check-type-error (map/IntList (λ ([n : Int]) #f) (Null)))
(define-type BoolList (variant (BoolNull) (BoolCons Bool BoolList)))
-(define (map/BoolList [f : (→ Bool Int)] [lst : BoolList]) : IntList
+(define (map/BoolList [f : (Bool → Int)] [lst : BoolList]) : IntList
(cases lst
[BoolNull () (Null)]
[BoolCons (x xs) (Cons (f x) (map/BoolList f xs))]))
@@ -143,7 +143,7 @@
(cases lst
[Null () (None)]
[Cons (x xs) (Just x)]))
- : (→ IntList MaybeInt))
+ : (IntList → MaybeInt))
(check-type ((λ ([lst : IntList])
(cases lst
[Null () (None)]
diff --git a/stlc.rkt b/stlc.rkt
@@ -39,12 +39,12 @@
(syntax-parse stx #:datum-literals (variant)
[(_ τ:id (variant (Cons:id τ_fld ...) ...))
#:with ((x ...) ...) (stx-map generate-temporaries #'((τ_fld ...) ...))
- #:when (Γ (type-env-extend #'([Cons (→ τ_fld ... τ)] ...)))
+ #:when (Γ (type-env-extend #'([Cons (τ_fld ... → τ)] ...)))
#'(begin
(struct Cons (x ...) #:transparent) ...)]
[(_ τ:id (Cons:id τ_fld ...))
#:with (x ...) (generate-temporaries #'(τ_fld ...))
- #:when (Γ (type-env-extend #'([Cons (→ τ_fld ... τ)])))
+ #:when (Γ (type-env-extend #'([Cons (τ_fld ... → τ)])))
#'(begin
(struct Cons (x ...) #:transparent))]))
(define-syntax (cases stx)
@@ -52,7 +52,7 @@
[(_ e [Cons (x ...) body ... body_result] ...)
#:with e+ (expand/df #'e)
#:with (Cons+ ...) (stx-map expand/df #'(Cons ...))
- #:with ((→ τ ... τ_Cons) ...) (stx-map typeof #'(Cons+ ...))
+ #:with ((τ ... → τ_Cons) ...) (stx-map typeof #'(Cons+ ...))
#:when (stx-andmap (λ (τ) (assert-type #'e+ τ)) #'(τ_Cons ...))
#:with ((lam (x+ ...) body+ ... body_result+) ...)
(stx-map (λ (bods xs τs)
@@ -91,9 +91,9 @@
(syntax-parse stx
[(_) (⊢ (syntax/loc stx (void)) #'Unit)]))
-(define-syntax (define-prim stx)
- (syntax-parse stx
- [(_ op τ_arg τ_res)
+(define-syntax (define-primop stx)
+ (syntax-parse stx #:datum-literals (:) #:literals (→)
+ [(_ op:id : (τ_arg ... → τ_result))
#:with op/tc (format-id #'op "~a/tc" #'op)
#'(begin
(provide (rename-out [op/tc op]))
@@ -101,17 +101,20 @@
(syntax-parse stx
[f:id #'op] ; HO case
[(_ e (... ...))
- #:with (e+ (... ...)) (stx-map expand/df #'(e (... ...)))
- #:when (stx-andmap (λ (τ) (assert-type τ τ_arg)) #'(e+ (... ...)))
- (⊢ (syntax/loc stx (op e+ (... ...))) τ_res)])))]))
-(define-prim + #'Int #'Int)
-(define-prim - #'Int #'Int)
-(define-prim = #'Int #'Bool)
-(define-prim < #'Int #'Bool)
-(define-prim not #'Bool #'Bool)
-(define-prim or #'Bool #'Bool)
-(define-prim and #'Bool #'Bool)
-(define-prim abs #'Int #'Int)
+ #:with es+ (stx-map expand/df #'(e (... ...)))
+ #:with τs #'(τ_arg ...)
+ #:fail-unless (= (stx-length #'es+) (stx-length #'τs))
+ "Wrong number of arguments"
+ #:when (stx-andmap assert-type #'es+ #'τs)
+ (⊢ (quasisyntax/loc stx (op . es+)) #'τ_result)])))]))
+(define-primop + : (Int Int → Int))
+(define-primop - : (Int Int → Int))
+(define-primop = : (Int Int → Bool))
+(define-primop < : (Int Int → Bool))
+(define-primop or : (Bool Bool → Bool))
+(define-primop and : (Bool Bool → Bool))
+(define-primop not : (Bool → Bool))
+(define-primop abs : (Int → Int))
(define-syntax (λ/tc stx)
@@ -133,7 +136,7 @@
;; manually handle the implicit begin
#:when (stx-map assert-Unit-type #'(e++ ...))
#:with τ_body (typeof #'e_result++)
- (⊢ (syntax/loc stx (lam xs e++ ... e_result++)) #'(→ τ ... τ_body))]))
+ (⊢ (syntax/loc stx (lam xs e++ ... e_result++)) #'(τ ... → τ_body))]))
(define-syntax (let/tc stx)
(syntax-parse stx #:datum-literals (:)
@@ -153,7 +156,7 @@
[(_ :t x) #'(printf "~a : ~a\n" 'x (hash-ref runtime-env 'x))]
[(_ e_fn e_arg ...)
#:with (e_fn+ e_arg+ ...) (stx-map expand/df #'(e_fn e_arg ...))
- #:with (→ τ ... τ_res) (typeof #'e_fn+)
+ #:with (τ ... → τ_res) (typeof #'e_fn+)
#:when (stx-andmap assert-type #'(e_arg+ ...) #'(τ ...))
(⊢ (syntax/loc stx (#%app e_fn+ e_arg+ ...)) #'τ_res)]))
@@ -210,7 +213,7 @@
(define-syntax (define/tc stx)
(syntax-parse stx #:datum-literals (:)
[(_ (f:id [x:id : τ] ...) : τ_result e ...)
- #:when (Γ (type-env-extend #'([f (→ τ ... τ_result)])))
+ #:when (Γ (type-env-extend #'([f (τ ... → τ_result)])))
#'(define f (λ/tc ([x : τ] ...) e ...))]
[(_ x:id e) #'(define x e)]))
@@ -281,7 +284,7 @@
#:with (v ...) #'(deffn+.rhs ...)
#:with (e ...) (template ((?@ . mb-form.e) ...))
;; base type env
- #:when (Γ (type-env-extend #'((+ (→ Int Int Int)))))
+ #:when (Γ (type-env-extend #'((+ (Int Int → Int)))))
;; NOTE: for struct def, define-values *must* come before define-syntaxes
;; ow, error: "Just10: unbound identifier; also, no #%top syntax transformer is bound"
(quasisyntax/loc stx
diff --git a/stx-utils.rkt b/stx-utils.rkt
@@ -11,4 +11,5 @@
(define paren-prop (syntax-property stx 'paren-shape))
(and paren-prop (char=? #\{ paren-prop)))
(define (stx-member v stx)
- (member v (syntax->list stx) free-identifier=?))
-\ No newline at end of file
+ (member v (syntax->list stx) free-identifier=?))
+(define (stx-length stx) (length (syntax->list stx)))
+\ No newline at end of file
diff --git a/sysf-tests.rkt b/sysf-tests.rkt
@@ -6,14 +6,14 @@
(check-type (Just {Int} 1) : (Maybe Int))
(check-type-error (Just {Int} #f))
(check-not-type (Just {Int} 1) : (Maybe Bool))
-(check-type (λ {X} ([x : X]) x) : (∀ (X) (→ X X)))
+(check-type (λ {X} ([x : X]) x) : (∀ (X) (X → X)))
(check-type-error ((λ ([x : X]) x) 1))
;; lists
(define-type (MyList X) (variant (Null) (Cons X (MyList X))))
(check-type (Null {Int}) : (MyList Int))
(check-type (Cons {Int} 1 (Null {Int})) : (MyList Int))
-(define (map/List {A B} [f : (→ A B)] [lst : (MyList A)]) : (MyList B)
+(define (map/List {A B} [f : (A → B)] [lst : (MyList A)]) : (MyList B)
(cases {A} lst
[Null () (Null {B})]
[Cons (x xs) (Cons {B} (f {A B} x) (map/List {A B} f xs))]))
@@ -36,7 +36,7 @@
(check-type-error (list {Int} 1 2 #f))
(check-type-error (list {Bool} 1 2 3))
;; map
-(define (map {A B} [f : (→ A B)] [lst : (Listof A)]) : (Listof B)
+(define (map {A B} [f : (A → B)] [lst : (Listof A)]) : (Listof B)
(if (null? {A} lst)
(null {B})
(cons {B} (f {A B} (first {A} lst)) (map {A B} f (rest {A} lst)))))
@@ -50,7 +50,7 @@
(define-type Queen (Q Int Int))
;; filter
-(define (filter {A} [p? : (→ A Bool)] [lst : (Listof A)]) : (Listof A)
+(define (filter {A} [p? : (A → Bool)] [lst : (Listof A)]) : (Listof A)
(if (null? {A} lst)
(null {A})
(let ([x (first {A} lst)])
@@ -63,7 +63,7 @@
: (Listof Int) => (list {Int} 1 2 3 4 6 7))
;; foldr
-(define (foldr {A B} [f : (→ A B B)] [base : B] [lst : (Listof A)]) : B
+(define (foldr {A B} [f : (A B → B)] [base : B] [lst : (Listof A)]) : B
(if (null? {A} lst)
base
(f (first {A} lst) (foldr {A B} f base (rest {A} lst)))))
@@ -71,7 +71,7 @@
(check-type-and-result (foldr {Int Int} + 0 (build-list {Int} add1 4)) : Int => 10)
;; foldl
-(define (foldl {A B} [f : (→ A B B)] [acc : B] [lst : (Listof A)]) : B
+(define (foldl {A B} [f : (A B → B)] [acc : B] [lst : (Listof A)]) : B
(if (null? {A} lst)
acc
(foldl {A B} f (f (first {A} lst) acc) (rest {A} lst))))
@@ -90,7 +90,7 @@
(check-type-error (tails {Int} (list {Bool} 1 2 3)))
(check-not-type (tails {Int} (list {Int} 1 2 3)) : (Listof Int))
-(define (andmap {A} [f : (→ A Bool)] [lst : (Listof A)]) : Bool
+(define (andmap {A} [f : (A → Bool)] [lst : (Listof A)]) : Bool
(if (null? {A} lst)
#t
(and (f (first {A} lst)) (andmap {A} f (rest {A} lst)))))
@@ -112,16 +112,16 @@
(let ([q1 (first {Queen} lst)])
(andmap {Queen} (λ ([q2 : Queen]) (safe? q1 q2)) (rest {Queen} lst)))))
-(check-type safe/list? : (→ (Listof Queen) Bool))
+(check-type safe/list? : ((Listof Queen) → Bool))
(define (valid? [lst : (Listof Queen)]) : Bool
(andmap {(Listof Queen)} safe/list? (tails {Queen} lst)))
-(define (build-list-help {A} [f : (→ Int A)] [n : Int] [m : Int]) : (Listof A)
+(define (build-list-help {A} [f : (Int → A)] [n : Int] [m : Int]) : (Listof A)
(if (= n m)
(null {A})
(cons {A} (f {A} n) (build-list-help {A} f (add1 n) m))))
-(define (build-list {A} [f : (→ Int A)] [n : Int]) : (Listof A)
+(define (build-list {A} [f : (Int → A)] [n : Int]) : (Listof A)
(build-list-help {A} f 0 n))
(check-type-and-result (build-list {Int} add1 8)
@@ -163,9 +163,9 @@
;; testing for variable capture
(define (polyf {X} [x : X]) : X x)
-(check-type polyf : (∀ (X) (→ X X)))
-(define (polyf2 {X} [x : X]) : (∀ (X) (→ X X)) polyf)
-(check-type polyf2 : (∀ (X) (→ X (∀ (X) (→ X X)))))
+(check-type polyf : (∀ (X) (X → X)))
+(define (polyf2 {X} [x : X]) : (∀ (X) (X → X)) polyf)
+(check-type polyf2 : (∀ (X) (X → (∀ (X) (X → X)))))
;; the following test fails bc X gets captured (2014-08-18)
;; - 2014-08-20: fixed
@@ -177,21 +177,21 @@
;; capture is not ok when forall is applied to non-base types, ie →
;; (see test below)
;; - 2014-08-20: fixed by implementing manual subst
-(check-type (inst polyf2 Int) : (→ Int (∀ (X) (→ X X))))
+(check-type (inst polyf2 Int) : (Int → (∀ (X) (X → X))))
;; the following test "fails" bc forall is nested
;; - Typed Racket has same behavior, so ok
(check-type-error (inst (inst polyf2 Int) Bool))
(check-type-error ((inst polyf2 Int) #f))
;; again, the following example has type (∀ (Int) (→ Int Int)), which is ok
;; - 2014-08-20: fixed by impl manual subst
-(check-type ((inst polyf2 Int) 1) : (∀ (X) (→ X X)))
-(check-type (inst ((inst polyf2 Int) 1) Bool) : (→ Bool Bool))
+(check-type ((inst polyf2 Int) 1) : (∀ (X) (X → X)))
+(check-type (inst ((inst polyf2 Int) 1) Bool) : (Bool → Bool))
;; test same example with type-instantiating apply instead of inst
-(check-type (polyf2 {Int} 1) : (∀ (Y) (→ Y Y)))
+(check-type (polyf2 {Int} 1) : (∀ (Y) (Y → Y)))
(check-type-error (polyf2 {Int} #f))
(check-type-and-result ((polyf2 {Int} 1) {Bool} #f) : Bool => #f)
(check-type-error ((polyf2 {Int} 1) {Bool} 2))
-(check-type (inst polyf (→ Int Int)) : (→ (→ Int Int) (→ Int Int)))
+(check-type (inst polyf (Int → Int)) : ((Int → Int) → (Int → Int)))
;; the follow test fails because the binder is renamed to (→ Int Int)
-(check-type (inst polyf2 (→ Int Int)) : (→ (→ Int Int) (∀ (X) (→ X X))))
-\ No newline at end of file
+(check-type (inst polyf2 (Int → Int)) : ((Int → Int) → (∀ (X) (X → X))))
+\ No newline at end of file
diff --git a/sysf.rkt b/sysf.rkt
@@ -54,7 +54,7 @@
(syntax-parse stx #:datum-literals (variant)
[(_ (Tycon:id X:id ...) (variant (Cons:id τ_fld ...) ...))
#:with ((x ...) ...) (stx-map generate-temporaries #'((τ_fld ...) ...))
- #:when (Γ (type-env-extend #'([Cons (∀ (X ...) (→ τ_fld ... (Tycon X ...)))] ...)))
+ #:when (Γ (type-env-extend #'([Cons (∀ (X ...) (τ_fld ... → (Tycon X ...)))] ...)))
#'(begin ; should be racket begin
(struct Cons (x ...) #:transparent) ...)]
[(_ any ...) #'(stlc:define-type any ...)]))
@@ -76,12 +76,12 @@
;; cases ----------------------------------------------------------------------
(define-syntax (cases stx)
- (syntax-parse stx #:literals (∀)
+ (syntax-parse stx #:literals (∀ →)
[(_ τs:inst-τs e [Cons (x ...) body ... body_result] ...)
#:with e+ (expand/df #'e)
#:with (Cons+ ...) (stx-map expand/df #'(Cons ...))
#:with (τ_Cons:∀τ ...) (stx-map typeof #'(Cons+ ...))
- #:with ((→ τ ... τ_res) ...)
+ #:with ((τ ... → τ_res) ...)
(stx-map (λ (∀τ) (apply-forall ∀τ #'τs)) #'(τ_Cons ...))
;; check constructor type in every branch matches expr being matched
#:when (stx-andmap (λ (τ) (assert-type #'e+ τ)) #'(τ_res ...))
@@ -124,7 +124,7 @@
;; manually typecheck the implicit begin
#:when (stx-map assert-Unit-type #'(e++ ...))
#:with τ_body (typeof #'e_result++)
- (⊢ (syntax/loc stx (lam xs e++ ... e_result++)) #'(∀ tvs (→ τ ... τ_body)))]
+ (⊢ (syntax/loc stx (lam xs e++ ... e_result++)) #'(∀ tvs (τ ... → τ_body)))]
[(_ any ...) #'(stlc:λ any ...)]))
; define ----------------------------------------------------------------------
@@ -133,7 +133,7 @@
;; most of the code from this case, except for the curly? check,
;; is copied from stlc:define
[(_ (f:id tvs:tyvars [x:id : τ] ...) : τ_result e ...)
- #:when (Γ (type-env-extend #'([f (∀ tvs (→ τ ... τ_result))])))
+ #:when (Γ (type-env-extend #'([f (∀ tvs (τ ... → τ_result))])))
#'(define f (λ/tc tvs ([x : τ] ...) e ...))]
[(_ any ...) #'(stlc:define any ...)]))
@@ -146,7 +146,7 @@
[(_ e_fn τs:inst-τs e_arg ...)
#:with (e_fn+ e_arg+ ...) (stx-map expand/df #'(e_fn e_arg ...))
#:with τ_fn:∀τ (typeof #'e_fn+)
- #:with (→ τ_arg ... τ_res) (apply-forall #'τ_fn #'τs)
+ #:with (τ_arg ... → τ_res) (apply-forall #'τ_fn #'τs)
#:when (stx-andmap assert-type #'(e_arg+ ...) #'(τ_arg ...))
(⊢ (syntax/loc stx (#%app e_fn+ e_arg+ ...)) #'τ_res)]
;; handle type apply of non-poly fn here; just pass through
diff --git a/typecheck.rkt b/typecheck.rkt
@@ -26,7 +26,7 @@
(define-for-syntax (type=? τ1 τ2)
; (printf "type= ~a ~a\n" (syntax->datum τ1) (syntax->datum τ2))
- (syntax-parse #`(#,τ1 #,τ2) #:datum-literals (∀)
+ (syntax-parse #`(#,τ1 #,τ2) #:datum-literals (∀ →)
[(x:id y:id) (free-identifier=? τ1 τ2)]
[(∀τ1 ∀τ2)
#:with (∀ τvars1 τ_body1) #'∀τ1
@@ -40,6 +40,9 @@
(and (= (length (syntax->list #'τvars1))
(length (syntax->list #'τvars2)))
(type=? (apply-forall #'∀τ1 #'fresh-τvars) (apply-forall #'∀τ2 #'fresh-τvars)))]
+ [((τ_arg1 ... → τ_result1) (τ_arg2 ... → τ_result2))
+ (and (= (length (syntax->list #'(τ_arg1 ...))) (length (syntax->list #'(τ_arg2 ...))))
+ (type=? #'τ_result1 #'τ_result2))]
[((tycon1:id τ1 ...) (tycon2:id τ2 ...))
(and (free-identifier=? #'tycon1 #'tycon2)
(= (length (syntax->list #'(τ1 ...))) (length (syntax->list #'(τ2 ...))))
@@ -91,7 +94,7 @@
;; apply-forall ---------------------------------------------------------------
(define-for-syntax (subst x τ mainτ)
- (syntax-parse mainτ #:datum-literals (∀)
+ (syntax-parse mainτ #:datum-literals (∀ →)
[y:id
#:when (free-identifier=? #'y x)
τ]
@@ -104,6 +107,12 @@
#:with (∀ tyvars τbody) #'∀τ
#:when (not (stx-member x #'tyvars))
#`(∀ tyvars #,(subst x τ #'τbody))]
+ ;; need the ~and because for the result, I need to use the → literal
+ ;; from the context of the input, and not the context here
+ [(τ_arg ... (~and (~datum →) arrow) τ_result)
+ #:with (τ_arg/subst ... τ_result/subst)
+ (stx-map (curry subst x τ) #'(τ_arg ... τ_result))
+ #'(τ_arg/subst ... arrow τ_result/subst)]
[(tycon:id τarg ...)
#:with (τarg/subst ...) (stx-map (curry subst x τ) #'(τarg ...))
#'(tycon τarg/subst ...)]))
