commit 479ca7d717ba70bc87b1875154481f2f2dddb3dc
parent 98fdc8806cd78cc454cd2e59454797399494b08c
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Mon, 29 Jun 2015 18:20:03 -0400
implement fomega type-level abs and app
- add define-type-alias to fomega
- fomega complete and working
Diffstat:
4 files changed, 204 insertions(+), 49 deletions(-)
diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt
@@ -1,14 +1,14 @@
#lang racket/base
(require "typecheck.rkt")
-(require (except-in "sysf.rkt" #%app λ Int #%datum → Λ inst ∀ + #;type=?)
- (prefix-in sysf: (only-in "sysf.rkt" #%app λ Int → ∀ #;type=?)))
+(require (except-in "sysf.rkt" #%app λ Int #%datum → Λ inst ∀ + type-eval)
+ (prefix-in sysf: (only-in "sysf.rkt" #%app λ Int → ∀ type-eval)))
(provide (rename-out [app/tc #%app] [λ/tc λ] [datum/tc #%datum]))
(provide (except-out (all-from-out "sysf.rkt")
sysf:Int sysf:→ sysf:∀
sysf:#%app sysf:λ
- #;(for-syntax sysf:type=?)))
+ (for-syntax sysf:type-eval)))
(provide Int → ∀ inst Λ tyλ tyapp
- #;(for-syntax type=?))
+ (for-syntax type-eval))
;; System F_omega
;; Type relation:
@@ -17,38 +17,53 @@
;; Terms:
;; - terms from sysf.rkt
+(provide define-type-alias)
+(define-syntax define-type-alias
+ (syntax-parser
+ [(_ alias:id τ:type)
+ ; must eval, otherwise undefined types will be allowed
+ #'(define-syntax alias (syntax-parser [x:id #'τ.norm]))]))
+
(begin-for-syntax
- ;; Extend to handle ∀ with type annotations
- #;(define (eval-τ τ [tvs #'()] . rst)
+ ;; extend type-eval to handle tyapp
+ (define (type-eval τ)
+ (printf "eval: ~a\n" (syntax->datum τ))
(syntax-parse τ
- [((~literal ∀) (b:typed-binding ...) t-body)
- #:with new-tvs #'(b.x ...)
- #`(∀ (b ...) #,(apply (current-τ-eval) #'t-body (stx-append tvs #'new-tvs) rst))]
- ;; need to manually handle type constructors now since they are macros
- [((~literal →) t ...)
- #`(→ #,@(stx-map (λ (ty) (apply (current-τ-eval) ty tvs rst)) #'(t ...)))]
- #;[((~literal #%app) x ...)
- #:when (printf "~a\n" (syntax->datum #'(x ...)))
- #'(void)]
- [((~literal tyapp) ((~literal tyλ) (b:typed-binding ...) τ_body) τ_arg ...)
- #:with (τ_arg+ ...) (stx-map (λ (ty) (apply (current-τ-eval) ty tvs rst)) #'(τ_arg ...))
- #:with τ_body+ (apply (current-τ-eval) #'τ_body tvs rst)
- (substs #'(τ_arg+ ...) #'(b.x ...) #'τ_body+)]
- [_ (apply sysf:eval-τ τ tvs rst)]))
- ;(current-τ-eval eval-τ)
-
- ;; extend to handle ∀ with kind annotations
- #;(define (type=? τ1 τ2)
- (syntax-parse (list τ1 τ2) #:literals (∀)
- [((∀ (a:typed-binding ...) t1:type) (∀ (b:typed-binding ...) t2:type))
- #:when (= (stx-length #'(a ...)) (stx-length #'(b ...)))
- #:with (z ...) (generate-temporaries #'(a ...))
- #:when (typechecks? #'(a.τ ...) #'(b.τ ...))
- ((current-type=?) (substs #'(z ...) #'(a.x ...) #'t1)
- (substs #'(z ...) #'(b.x ...) #'t2))]
- [_ (sysf:type=? τ1 τ2)]))
- #;(current-type=? type=?)
- #;(current-typecheck-relation type=?))
+ [((~literal #%plain-app) τ_fn τ_arg ...)
+ #:with ((~literal #%plain-lambda) (tv ...) τ_body) ((current-type-eval) #'τ_fn)
+ #:with (τ_arg+ ...) (stx-map (current-type-eval) #'(τ_arg ...))
+ #:when (printf "match\n")
+ (substs #'(τ_arg+ ...) #'(tv ...) #'τ_body)]
+ [((~literal ∀) _ ...) ((current-type-eval) (sysf:type-eval τ))]
+ [((~literal →) _ ...) ((current-type-eval) (sysf:type-eval τ))]
+ [((~literal ⇒) _ ...) ((current-type-eval) (sysf:type-eval τ))]
+ [((~literal tyλ) _ ...) (sysf:type-eval τ)]
+ [((~literal tyapp) _ ...) ((current-type-eval) (sysf:type-eval τ))]
+ [((~literal #%plain-lambda) (x ...) τ_body ...)
+ #:with (τ_body+ ...) (stx-map (current-type-eval) #'(τ_body ...))
+ (syntax-track-origin #'(#%plain-lambda (x ...) τ_body+ ...) τ #'plain-lambda)]
+ [((~literal #%plain-app) arg ...)
+ #:with (arg+ ...) (stx-map (current-type-eval) #'(arg ...))
+ (syntax-track-origin #'(#%plain-app arg+ ...) τ #'#%plain-app)]
+ [(τ ...) (stx-map (current-type-eval) #'(τ ...))]
+ [_ (sysf:type-eval τ)]))
+ (current-type-eval type-eval)
+
+ ;; extend to handle tyapp
+; (define (type=? τ1 τ2)
+; (printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum τ1))
+; (printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum τ2))
+; (syntax-parse (list τ1 τ2)
+; [(((~literal #%plain-app) ((~literal #%plain-lambda) (tv ...) τ_body) τ_arg ...) _)
+; #:when (printf "match1\n")
+; ((current-type=?) (substs #'(τ_arg ...) #'(tv ...) #'τ_body) τ2)]
+; [(_ ((~literal #%plain-app) ((~literal #%plain-lambda) (tv ...) τ_body) τ_arg ...))
+; #:when (printf "match2\n")
+; ((current-type=?) τ1 (substs #'(τ_arg ...) #'(tv ...) #'τ_body))]
+; [_ (sysf:type=? τ1 τ2)]))
+; (current-type=? type=?)
+; (current-typecheck-relation type=?))
+)
(define-base-type ★)
(define-type-constructor ⇒)
@@ -80,17 +95,6 @@
#:when (typecheck? #'k #'★)
(⊢ #'(#%plain-lambda tvs- b.τ ... τ-) #;#'(sysf:∀ tvs- τ-) #'★)]))
-#;(define-syntax (Λ stx)
- (syntax-parse stx
- [(_ (tv:id ...) e)
- #:with (tvs- e- τ) (infer/tvs+erase #'e #'(tv ...))
- (⊢ #'e- #'(∀ tvs- τ))]))
-#;(define-syntax (inst stx)
- (syntax-parse stx
- [(_ e τ:type ...)
- #:with (e- ∀τ) (infer+erase #'e)
- #:with ((~literal #%plain-lambda) (tv ...) τ_body) #'∀τ
- (⊢ #'e- (substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))
(define-syntax (Λ stx)
(syntax-parse stx
[(_ (b:typed-binding ...) e)
@@ -106,16 +110,53 @@
(⊢ #'e- (substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))
;; TODO: merge with regular λ and app?
-(define-syntax (tyλ stx)
+#;(define-syntax (tyλ stx)
(syntax-parse stx
; b = [tv : k]
[(_ (b:typed-binding ...) τ)
#:with ((tv- ...) τ- k) (infer/type-ctxt+erase #'(b ...) #'τ)
; TODO: Racket lambda?
(⊢ #'(λ (tv- ...) τ-) #'(⇒ b.τ ... k))]))
+(define-syntax (tyλ stx)
+ (syntax-parse stx
+ [(_ (b:typed-binding ...) τ)
+ #:with (tvs- τ- k) (infer/type-ctxt+erase #'(b ...) #'τ)
+ ;; b.τ's here are actually kinds
+ (⊢ #'(λ tvs- τ-) #'(⇒ b.τ ... k))]))
+
+#;(define-syntax (tyapply stx)
+ (syntax-parse stx
+ [(_ ((~literal #%plain-lambda) (tv ...) τ_body) τ_arg ...)
+ (substs #'(τ_arg ...) #'(tv ...) #'τ_body)]))
(define-syntax (tyapp stx)
(syntax-parse stx
[(_ τ_fn τ_arg ...)
+ #:with [τ_fn- k_fn] (infer+erase #'τ_fn)
+ #:fail-unless (⇒? #'k_fn)
+ (format "Kind error: Attempting to apply a non-tyλ with kind ~a\n"
+ (syntax->datum #'τ_fn) (syntax->datum #'k_fn))
+ #:with ((~literal #%plain-app) _ k ... k_res) #'k_fn
+ #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...))
+ #:fail-unless (typechecks? #'(k_arg ...) #'(k ...))
+ (string-append
+ (format
+ "Wrong number of args given to tyλ ~a, or args have wrong kind:\ngiven: "
+ (syntax->datum #'τ_fn))
+ (string-join
+ (map
+ (λ (τ+k) (format "~a : ~a" (car τ+k) (cadr τ+k)))
+ (syntax->datum #'([τ_arg k_arg] ...)))
+ ", ")
+ "\nexpected arguments with type: "
+ (string-join
+ (map (λ (x) (format "~a" x)) (syntax->datum #'(k ...)))
+ ", "))
+ ;; cant do type-subst here bc τ_fn might be a (forall) tyvar
+ ;#:with τ_res ((current-type-eval) #'(tyapply τ_fn- τ_arg- ...))
+ (⊢ #'(#%app τ_fn- τ_arg- ...) #'k_res)]))
+#;(define-syntax (tyapp stx)
+ (syntax-parse stx
+ [(_ τ_fn τ_arg ...)
#:with [τ_fn- ((~literal ⇒) k ... k_res)] (infer+erase #'τ_fn)
#:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...))
#:when (typechecks? #'(k_arg ...) #'(k ...))
@@ -137,7 +178,7 @@
(syntax-parse stx
[(_ e_fn e_arg ...)
#:with [e_fn- τ_fn] (infer+erase #'e_fn)
- ;; this is sysf:→?, dont need prefix bc it's not defined here
+ ;; this is sysf:→?, it's not defined in fomega so import without prefix
#:fail-unless (→? #'τ_fn)
(format "Type error: Attempting to apply a non-function ~a with type ~a\n"
(syntax->datum #'e_fn) (syntax->datum #'τ_fn))
diff --git a/tapl/notes.txt b/tapl/notes.txt
@@ -180,3 +180,11 @@ debugging notes -------------
- vague "bad syntax" error
- means a syntax-parse #:when or #:with matching failed
- ideally would have better err msg at that spot
+
+- #%datum: keyword used as an expression in: #:with
+ - missing a #:when in front of a printf
+
+- one of type=? arguments is false
+ - term missing a type
+ - type missing a kind
+ - need to transfer syntax properties, eg subst
diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt
@@ -43,8 +43,8 @@
;; Indicates whether two types are equal
;; type equality = structurally free-identifier=?
(define (type=? τ1 τ2)
-; (printf "(τ=) t1 = ~a\n" τ1 #;(syntax->datum τ1))
-; (printf "(τ=) t2 = ~a\n" τ2 #;(syntax->datum τ2))
+ (printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum τ1))
+ (printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum τ2))
(syntax-parse (list τ1 τ2)
[(x:id y:id) (free-identifier=? τ1 τ2)]
[((τa ...) (τb ...)) (types=? #'(τa ...) #'(τb ...))]
diff --git a/tapl/tests/fomega-tests.rkt b/tapl/tests/fomega-tests.rkt
@@ -15,6 +15,112 @@
: (∀ ([X : ★]) (→ X X )))
(typecheck-fail ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (⇒ ★ ★)]) (λ ([x : X]) x))))
+(check-type (tyλ ([t : ★]) t) : (⇒ ★ ★))
+(check-type (tyλ ([t : ★] [s : ★]) t) : (⇒ ★ ★ ★))
+(check-type (tyλ ([t : ★]) (tyλ ([s : ★]) t)) : (⇒ ★ (⇒ ★ ★)))
+(check-type (tyλ ([t : (⇒ ★ ★)]) t) : (⇒ (⇒ ★ ★) (⇒ ★ ★)))
+(check-type (tyλ ([t : (⇒ ★ ★ ★)]) t) : (⇒ (⇒ ★ ★ ★) (⇒ ★ ★ ★)))
+(check-type (tyλ ([arg : ★] [res : ★]) (→ arg res)) : (⇒ ★ ★ ★))
+
+(check-type (tyapp (tyλ ([t : ★]) t) Int) : ★)
+(check-type (λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) : (→ Int Int))
+(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
+(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
+(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
+(typecheck-fail ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
+
+;; partial-apply →
+(check-type (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)
+ : (⇒ ★ ★))
+; f's type must have kind ★
+(typecheck-fail (λ ([f : (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)]) f))
+(check-type (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f)) :
+ (∀ ([tyf : (⇒ ★ ★)]) (→ (tyapp tyf String) (tyapp tyf String))))
+(check-type (inst
+ (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
+ (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
+ : (→ (→ Int String) (→ Int String)))
+;; applied f too early
+(typecheck-fail (inst
+ (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
+ (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)))
+(check-type ((inst
+ (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
+ (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
+ (λ ([x : Int]) "int")) : (→ Int String))
+(check-type (((inst
+ (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
+ (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
+ (λ ([x : Int]) "int")) 1) : String ⇒ "int")
+
+; tapl examples, p441
+(define-type-alias Id (tyλ ([X : ★]) X))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (tyapp Id String)) Int))
+(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int (tyapp Id String)) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) (tyapp Id String)) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) String) Int))
+(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (tyapp Id (→ Int String)) Int))
+(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (→ Int String)) Int))
+(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (tyapp Id (→ Int String))) Int))
+
+; tapl examples, p451
+(define-type-alias Pair (tyλ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
+
+(check-type Pair : (⇒ ★ ★ ★))
+
+(check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X)))
+;; parametric pair constructor
+(check-type
+ (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ : (∀ ([X : ★][Y : ★]) (→ X Y (tyapp Pair X Y))))
+; concrete Pair Int String constructor
+(check-type
+ (inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ Int String)
+ : (→ Int String (tyapp Pair Int String)))
+; Pair Int String value
+(check-type
+ ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ Int String) 1 "1")
+ : (tyapp Pair Int String))
+; fst: parametric
+(check-type
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+ : (∀ ([X : ★][Y : ★]) (→ (tyapp Pair X Y) X)))
+; fst: concrete Pair Int String accessor
+(check-type
+ (inst
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+ Int String)
+ : (→ (tyapp Pair Int String) Int))
+; apply fst
+(check-type
+ ((inst
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+ Int String)
+ ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ Int String) 1 "1"))
+ : Int ⇒ 1)
+; snd
+(check-type
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+ : (∀ ([X : ★][Y : ★]) (→ (tyapp Pair X Y) Y)))
+(check-type
+ (inst
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+ Int String)
+ : (→ (tyapp Pair Int String) String))
+(check-type
+ ((inst
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+ Int String)
+ ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ Int String) 1 "1"))
+ : String ⇒ "1")
+
;(check-type (λ ([x : (∀ ([t : ★]) t)]) x) : (→ (∀ ([t : ★]) t) (∀ ([t : ★]) t)))
;(check-type (λ ([x : (∀ ([t : (⇒ ★ ★)]) (tyapp t Int))]) x) : Int #;(→ (∀ ([t : (⇒ ★ ★)]) t) (∀ ([t : (⇒ ★ ★)]) t)))
