commit f3172826096a906524dbe8f292a5210ad6d0bb62
parent 69c97a55124d618c9c3b4607c49cba6b524dc05a
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Tue, 19 May 2015 18:54:50 -0400
tapl: reimplement stlc using rename-transformers instead of typeenv
Diffstat:
8 files changed, 338 insertions(+), 14 deletions(-)
diff --git a/tapl/stlc+lit.rkt b/tapl/stlc+lit.rkt
@@ -0,0 +1,25 @@
+#lang racket/base
+(require
+ (for-syntax racket/base syntax/parse)
+ "typecheck.rkt")
+(require (prefix-in stlc: "stlc.rkt"))
+(provide (rename-out [datum/tc #%datum]
+ [stlc:#%app #%app]
+ [stlc:λ λ]))
+(provide Int
+ (rename-out [stlc:→ →]))
+(provide #%module-begin #%top-interaction require)
+
+;; Simply-Typed Lambda Calculus, plus numeric literals and primitives
+;; forms from stlc.rkt
+;; numeric literals
+;; prim +
+
+(define-base-type Int)
+
+(define-syntax (datum/tc stx)
+ (syntax-parse stx
+ [(_ . n:integer) (⊢ (syntax/loc stx (#%datum . n)) #'Int)]
+ [(_ . x)
+ #:when (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)
+ (syntax/loc stx (#%datum . x))]))
diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt
@@ -1,17 +1,55 @@
#lang racket/base
(require
- (for-syntax racket/base syntax/parse))
-
+ (for-syntax racket/base syntax/parse syntax/stx "stx-utils.rkt")
+ "typecheck.rkt")
+(provide (rename-out [λ/tc λ] [app/tc #%app])
+ →)
+(provide #%module-begin #%top-interaction require)
+
;; Simply-Typed Lambda Calculus
-;; - one arg lambda
;; - var
-;; - binary app
-;; - binary +
-;; - integers
+;; - multi-arg lambda
+;; - multi-arg app
-(define-syntax (datum/tc stx)
+;(define-syntax Int
+; (syntax-id-rules ()
+; [Int (error 'Int "Cannot use type at run time")]))
+;(define-syntax →
+; (syntax-id-rules ()
+; [(→ τ ...) (error '→ "Cannot use type at run time")]
+; [→ (error '→ "Cannot use type at run time")]))
+(define-type-constructor →)
+
+(define-syntax (λ/tc stx)
(syntax-parse stx
- [(_ . n:integer) (⊢ (syntax/loc stx (#%datum . n)) #'Int)]
- [(_ . x)
- #:when (type-error #:src #'x #:msg "Literal ~a has unknown type." #'x)
- (syntax/loc stx (#%datum . x))]))
-\ No newline at end of file
+ [(_ (b:typed-binding ...) e)
+; #:with τ_body (infer/type-ctxt #'([b.x b.τ] ...) #'e)
+ #:with τ_body (infer/type-ctxt #'([b.x b.τ] ...) #'e)
+;; #:with (lam xs+ e+)
+; #:with (lam xs+ (lr-stxs+vs1 stxs1 vs1 (lr-stxs+vs2 stxs2 vs2 e+)))
+; (with-extended-type-env
+; #'([x τ] ...)
+; (expand/df
+; #'(λ (x ...)
+; (let-syntax
+; ([x (make-rename-transformer (⊢ #'x #'τ))] ...)
+; e))))
+;; #:with e++ (if (identifier? #'e+)
+;; (with-extended-type-env #'([x τ] ...) (expand/df #'e+))
+;; #'e+)
+; #:with τ_body (typeof #'e+)
+; #:with τ_body (typeof #'e++)
+; (⊢ (syntax/loc stx (λ (b.x ...) e)) #'(b.τ ... → τ_body))]))
+ (⊢ #'(λ (b.x ...) e) #'(b.τ ... → τ_body))]))
+
+(define-syntax (app/tc stx)
+ (syntax-parse stx #:literals (→)
+ [(_ e_fn e_arg ...)
+; #:with (e_fn+ e_arg+ ...) (stx-map expand/df #'(e_fn e_arg ...))
+; #:with (τ ... → τ_res) (typeof #'e_fn+)
+ #:with (τ ... → τ_res) (infer #'e_fn)
+ #:with (τ_arg ...) (infers #'(e_arg ...))
+; #:when (stx-andmap assert-type #'(e_arg+ ...) #'(τ ...))
+ #:when (types=? #'(τ ...) #'(τ_arg ...))
+; (⊢ (syntax/loc stx (#%app e_fn+ e_arg+ ...)) #'τ_res)]))
+ (⊢ #'(#%app e_fn e_arg ...) #'τ_res)]))
diff --git a/tapl/stx-utils.rkt b/tapl/stx-utils.rkt
@@ -0,0 +1,22 @@
+#lang racket/base
+(require syntax/stx racket/list)
+(provide (all-defined-out))
+
+(define (stx-cadr stx) (car (stx-cdr stx)))
+
+(define (stx-andmap f . stx-lsts)
+ (apply andmap f (map syntax->list stx-lsts)))
+
+(define (stx-flatten stxs)
+ (apply append (stx-map syntax->list stxs)))
+
+(define (curly-parens? stx)
+ (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=?))
+
+(define (stx-length stx) (length (syntax->list stx)))
+
+(define (stx-last stx) (last (syntax->list stx)))
+\ No newline at end of file
diff --git a/tapl/tests/lam-testing-tests.rkt b/tapl/tests/lam-testing-tests.rkt
@@ -0,0 +1,3 @@
+#lang s-exp "lam-testing.rkt"
+
+((λ (x y) x) 1 2)
+\ No newline at end of file
diff --git a/tapl/tests/rackunit-typechecking.rkt b/tapl/tests/rackunit-typechecking.rkt
@@ -0,0 +1,50 @@
+#lang racket/base
+(require (for-syntax racket/base syntax/parse syntax/srcloc rackunit)
+ rackunit
+ "../typecheck.rkt")
+(provide (all-defined-out))
+
+(define-syntax (check-type stx)
+ (syntax-parse stx #:datum-literals (:)
+ [(_ e : τ ⇒ v) #'(check-type-and-result e : τ ⇒ v)]
+ [(_ e : τ-expected)
+ #:with e+ (expand/df #'e)
+ #:with τ (typeof #'e+)
+ #:fail-unless
+ (type=? #'τ #'τ-expected)
+ (format
+ "Expression ~a [loc ~a:~a] has type ~a, expected ~a"
+ (syntax->datum #'e) (syntax-line #'e) (syntax-column #'e)
+ (syntax->datum #'τ) (syntax->datum #'τ-expected))
+ #'(void)]))
+
+(define-syntax (check-not-type stx)
+ (syntax-parse stx #:datum-literals (:)
+ [(_ e : not-τ)
+ #:with e+ (expand/df #'e)
+ #:with τ (typeof #'e+)
+ #:fail-when
+ (type=? #'τ #'not-τ)
+ (format
+ "(~a:~a) Expression ~a should not have type ~a"
+ (syntax-line stx) (syntax-column stx)
+ (syntax->datum #'e) (syntax->datum #'τ))
+ #'(void)]))
+
+(define-syntax (typecheck-fail stx)
+ (syntax-parse stx #:datum-literals (:)
+ [(_ e)
+ #:when (check-exn
+ exn:fail?
+ (λ () (expand/df #'e))
+ (format
+ "Expression ~a has valid type, expected type check failure."
+ (syntax->datum #'e)))
+ #'(void)]))
+
+(define-syntax (check-type-and-result stx)
+ (syntax-parse stx #:datum-literals (: ⇒)
+ [(_ e : τ ⇒ v)
+ #'(begin
+ (check-type e : τ)
+ (check-equal? e v))]))
+\ No newline at end of file
diff --git a/tapl/tests/stlc+lit-tests.rkt b/tapl/tests/stlc+lit-tests.rkt
@@ -0,0 +1,12 @@
+#lang s-exp "../stlc+lit.rkt"
+(require "rackunit-typechecking.rkt")
+
+(check-type 1 : Int)
+(check-not-type 1 : Bool)
+(typecheck-fail "one")
+(typecheck-fail #f)
+(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)
+\ No newline at end of file
diff --git a/tapl/tests/stlc-tests.rkt b/tapl/tests/stlc-tests.rkt
@@ -0,0 +1,4 @@
+#lang s-exp "../stlc.rkt"
+(require "typecheck-testing.rkt")
+
+;; cannot have tests without base types
+\ No newline at end of file
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -1,3 +1,170 @@
#lang racket/base
+(require
+ (for-syntax racket/base syntax/parse racket/list syntax/stx "stx-utils.rkt")
+ (for-meta 2 racket/base syntax/parse racket/list syntax/stx "stx-utils.rkt"))
+(provide
+ (for-syntax (all-defined-out))
+ (all-defined-out))
-;; general type checking utility functions
-\ No newline at end of file
+;; type checking functions/forms
+
+;; General type checking strategy:
+;; - Each (expanded) syntax object has a 'type syntax property that is the type
+;; of the surface form.
+;; - To typecheck a surface form, it local-expands each subterm in order to get
+;; their types.
+;; - With this typechecking strategy, the typechecking implementation machinery
+;; is easily inserted into each #%- form
+;; - A base type is just a Racket identifier, so type equality, even with
+;; aliasing, is just free-identifier=?
+
+;; A Type is a Syntax Object
+
+(define-syntax (define-base-type stx)
+ (syntax-parse stx
+ [(_ τ:id)
+ #'(define-syntax (τ stx)
+ (syntax-parse stx
+ [_ (error 'Int "Cannot use type at run time.")]))]))
+(define-syntax (define-type-constructor stx)
+ (syntax-parse stx
+ [(_ τ:id)
+ #'(define-syntax (τ stx)
+ (syntax-parse stx
+ [_ (error 'Int "Cannot use type at run time.")]))]))
+
+(begin-for-syntax
+ ;; ⊢ : Syntax Type -> Syntax
+ ;; Attaches type τ to (expanded) expression e.
+; (define (⊢ e τ) (syntax-property (quasisyntax/loc e #,e) 'type τ))
+ (define (⊢ e τ) (syntax-property e 'type τ))
+
+ (define (infer/type-ctxt x+τs e)
+ (typeof
+ (syntax-parse x+τs
+ [([x τ] ...)
+ #:with
+ (lam xs+ (lr-stxs+vs1 stxs1 vs1 (lr-stxs+vs2 stxs2 vs2 e+)))
+ (expand/df
+ #`(λ (x ...)
+ (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...) #,e)))
+ #'e+])))
+
+
+ (define (infer e) (typeof (expand/df e)))
+ (define (infers es) (stx-map infer es))
+ (define (types=? τs1 τs2)
+ (stx-andmap type=? τs1 τs2))
+
+ ;; typeof : Syntax -> Type or #f
+ ;; Retrieves type of given stx, or #f if input has not been assigned a type.
+ (define (typeof stx) (syntax-property stx 'type))
+ ;; When checking for just the presence of a type,
+ ;; the name has-type? makes more sense (see expand/df for an example).
+ (define has-type? typeof)
+
+ ;; assert-type : Syntax Type -> Boolean
+ ;; Returns #t if (typeof e)==τ, else type error
+ (define (assert-type e τ)
+ ; (printf "~a has type " (syntax->datum e))
+ ; (printf "~a; expected: " (syntax->datum (typeof e)))
+ ; (printf "~a\n" (syntax->datum τ))
+ (or (type=? (typeof e) τ)
+ (type-error #:src e
+ #:msg "~a has type ~a, but should have type ~a" e (typeof e) τ)))
+
+ ;; type=? : Type Type -> Boolean
+ ;; Indicates whether two types are equal
+ (define (type=? τ1 τ2)
+ (syntax-parse #`(#,τ1 #,τ2)
+ ; → should not be datum literal;
+ ; adding a type constructor should extend type equality
+ #:datum-literals (→)
+ [(x:id y:id) (free-identifier=? τ1 τ2)]
+ [((x ... → x_out) (y ... → y_out))
+ (and (type=? #'x_out #'y_out)
+ (stx-andmap type=? #'(x ...) #'(y ...)))]
+ [_ #f]))
+
+
+ ;; expand/df : Syntax -> Syntax
+ ;; Local expands the given syntax object.
+ ;; The result always has a type (ie, a 'type stx-prop).
+ ;; Note:
+ ;; local-expand must expand all the way down, ie stop-ids == null
+ ;; If stop-ids is #f, then subexpressions won't get expanded and thus won't
+ ;; get assigned a type.
+ (define (expand/df e)
+; (printf "expanding: ~a\n" (syntax->datum e))
+; (printf "typeenv: ~a\n" (Γ))
+ (cond
+ ;; Handle identifiers separately.
+ ;; User-defined ids don't have a 'type stx-prop yet because Racket has no
+ ;; #%var form.
+ ;; Built-in ids, like primops, will already have a type though, so check.
+ [(identifier? e)
+ (define e+ (local-expand e 'expression null)) ; null == full expansion
+ (if (has-type? e+) e+ (⊢ e (type-env-lookup e)))]
+ [else (local-expand e 'expression null)]))
+
+ ;; type-error #:src Syntax #:msg String Syntax ...
+ ;; usage:
+ ;; type-error #:src src-stx
+ ;; #:msg msg-string msg-args ...
+ (define-syntax-rule (type-error #:src stx-src #:msg msg args ...)
+ (raise-user-error
+ 'TYPE-ERROR
+ (format (string-append "~a (~a:~a): " msg)
+ (syntax-source stx-src) (syntax-line stx-src) (syntax-column stx-src)
+ (syntax->datum args) ...))))
+
+;; type environment -----------------------------------------------------------
+(begin-for-syntax
+
+ ;; A Variable is a Symbol
+ ;; A TypeEnv is a [HashOf Variable => Type]
+
+ ;; base-type-env : TypeEnv
+ ;; Γ : [ParameterOf TypeEnv]
+ ;; The keys represent variables and the values are their types.
+ ;; NOTE: I can't use a free-id-table because a variable must be in the table
+ ;; before expanding (ie type checking) a λ body, so the vars in the body won't
+ ;; be free-id=? to the ones in the table.
+ ;; Using symbols instead of ids should be fine because I'm manually managing
+ ;; the entire environment, and the surface language has no macros so I know
+ ;; all the binding forms ahead of time.
+ (define base-type-env (hash))
+ (define Γ (make-parameter base-type-env))
+
+ ;; type-env-lookup : Syntax -> Type
+ ;; Returns the type of the input identifier, according to Γ.
+ (define (type-env-lookup x)
+ (hash-ref (Γ) (syntax->datum x)
+ (λ () (type-error #:src x
+ #:msg "Could not find type for variable ~a" x))))
+
+ ;; type-env-extend : #'((x τ) ...) -> TypeEnv
+ ;; Returns a TypeEnv extended with type associations x:τs/
+ (define (type-env-extend x:τs)
+ (define xs (stx-map stx-car x:τs))
+ (define τs (stx-map stx-cadr x:τs))
+ (apply hash-set* (Γ) (append-map (λ (x τ) (list (syntax->datum x) τ)) xs τs)))
+
+ ;; with-extended-type-env : #'((x τ) ...) Syntax ->
+ ;; Must be macro because type env must be extended before expanding the body e.
+ (define-syntax (with-extended-type-env stx)
+ (syntax-parse stx
+ [(_ x-τs e)
+ #'(parameterize ([Γ (type-env-extend x-τs)]) e)])))
+
+;; type classes
+(begin-for-syntax
+ (define-syntax-class typed-binding #:datum-literals (:)
+ (pattern [x:id : τ])
+ (pattern
+ any
+ #:with x #f
+ #:with τ #f
+ #:fail-when #t
+ (format "Improperly formatted type annotation: ~a; should have shape [x : τ]"
+ (syntax->datum #'any)))))
