commit 1a831454f467d7ade5bc3ca01f24c0ad7f1387cc
parent 3d4fe8f71a487f40fa97145e122bb01215fa7439
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Fri, 14 Aug 2015 19:37:09 -0400
progress commit: use typechecking system to typecheck types
- ported (tests passing) up to stlc+sub.rkt
Diffstat:
29 files changed, 1532 insertions(+), 920 deletions(-)
diff --git a/tapl/exist.rkt b/tapl/exist.rkt
@@ -1,12 +1,13 @@
#lang racket/base
(require "typecheck.rkt")
(require (except-in "stlc+reco+var.rkt" #%app λ let type=?)
- (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app λ let type=?))
- (prefix-in sysf: (only-in "sysf.rkt" type=?)))
+ (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app λ let #;type=?))
+ (only-in "stlc+rec-iso.rkt" type=?))
(provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let])
- (for-syntax type=?))
+ #;(for-syntax type=?))
(provide (except-out (all-from-out "stlc+reco+var.rkt") stlc:#%app stlc:λ stlc:let
- (for-syntax stlc:type=?)))
+ #;(for-syntax stlc:type=?))
+ (all-from-out "stlc+rec-iso.rkt"))
(provide ∃ pack open)
;; existential types
@@ -18,25 +19,43 @@
;; - terms from stlc+reco+var.rkt
;; - pack and open
-(begin-for-syntax
+#;(begin-for-syntax
(define (type=? t1 t2)
(or (stlc:type=? t1 t2)
(sysf:type=? t1 t2)))
(current-type=? type=?)
(current-typecheck-relation type=?))
-;; TODO: disambiguate expanded representation of ∃, ok to use lambda in this calculus
-(define-type-constructor (∃ [[X]] τ_body))
-;(provide ∃)
-;(define-syntax (∃ stx)
-; (syntax-parse stx
-; [(_ (tv:id) body)
-; (syntax/loc stx (#%plain-lambda (tv) body))]))
+
+#;(define-type-constructor (∃ [[X]] τ_body))
+; this is exactly the same as μ
+(define-syntax ∃
+ (syntax-parser
+ [(_ (tv:id) τ_body)
+ #:with ((tv-) τ_body- k) (infer/ctx+erase #'([tv : #%type]) #'τ_body)
+ #:when (#%type? #'k)
+ (mk-type #'(λ (tv-) τ_body-))]))
+(begin-for-syntax
+ (define (infer∃+erase e)
+ (syntax-parse (infer+erase e) #:context e
+ [(e- τ_e)
+ #:with ((~literal #%plain-lambda) (tv) τ) #'τ_e
+ #'(e- (tv τ))]))
+ (define-syntax ~∃*
+ (pattern-expander
+ (syntax-parser
+ [(_ (tv:id) τ)
+ #'(~or
+ ((~literal #%plain-lambda) (tv) τ)
+ (~and any (~do
+ (type-error
+ #:src #'any
+ #:msg "Expected ∃ type, got: ~a" #'any))))]))))
(define-syntax (pack stx)
(syntax-parse stx
[(_ (τ:type e) as ∃τ:type)
- #:with (~∃ [[τ_abstract]] τ_body) #'∃τ.norm
+ #:with (~∃* (τ_abstract) τ_body) #'∃τ.norm
; #:with (#%plain-lambda (τ_abstract:id) τ_body) #'∃τ.norm
#:with [e- τ_e] (infer+erase #'e)
#:when (typecheck? #'τ_e (subst #'τ.norm #'τ_abstract #'τ_body))
@@ -45,7 +64,7 @@
(define-syntax (open stx)
(syntax-parse stx #:datum-literals (<=)
[(_ ([(tv:id x:id) <= e_packed]) e)
- #:with [e_packed- (~∃ [[τ_abstract]] τ_body)] (infer+erase #'e_packed)
+ #:with [e_packed- (τ_abstract τ_body)] (infer∃+erase #'e_packed)
; #:with [e_packed- τ_packed] (infer+erase #'e_packed)
; #:with (#%plain-lambda (τ_abstract:id) τ_body) #'τ_packed ; existential
;; The subst below appears to be a hack, but it's not really.
@@ -91,7 +110,6 @@
;; ------------------------------
;; Γ ⊢ let {X_2,x}=t_1 in t_2 : T_2
;;
- #:with [tvs- (x-) (e-) (τ_e)]
- (infer #'(e) #:ctx #`([x : #,(subst #'tv #'τ_abstract #'τ_body)])
- #:tvs #'(tv))
+ #:with [_ (x-) (e-) (τ_e)]
+ (infer #'(e) #:tvctx #'([tv : #%type]) #:ctx #`([x : #,(subst #'tv #'τ_abstract #'τ_body)]))
(⊢ (let ([x- e_packed-]) e-) : τ_e)]))
\ No newline at end of file
diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt
@@ -74,7 +74,10 @@
; #:fail-unless (Bool? #'τ_tst) (format "given non-Bool test: ~a\n" (syntax->datum #'e_tst))
#:with (e1- τ1) (infer+erase #'e1)
#:with (e2- τ2) (infer+erase #'e2)
- #:when ((current-type=?) #'τ1 #'τ2)
+ #:fail-unless (or ((current-typecheck-relation) #'τ1 #'τ2)
+ ((current-typecheck-relation) #'τ2 #'τ1))
+ (format "branches must have the same type: given ~a and ~a"
+ (type->str #'τ1) (type->str #'τ2))
(⊢ (if e_tst- e1- e2-) : τ1)]))
(define-base-type Unit)
@@ -83,24 +86,25 @@
(define-syntax (begin/tc stx)
(syntax-parse stx
[(_ e_unit ... e)
- #:with ([e_unit- τ_unit] ...) (infers+erase #'(e_unit ...))
+ #:with (e_unit- ...) (stx-map inferUnit+erase #'(e_unit ...))
+; #:with ([e_unit- τ_unit] ...) (infers+erase #'(e_unit ...))
+; #:fail-unless (stx-andmap Unit? #'(τ_unit ...))
+; (string-append
+; "all begin expressions except the last one should have type Unit\n"
+; (string-join
+; (stx-map
+; (λ (e τ) (format "~a : ~a" (syntax->datum e) (syntax->datum τ)))
+; #'(e_unit ...) #'(τ_unit ...))
+; "\n")
+; "\n")
#:with (e- τ) (infer+erase #'e)
- #:fail-unless (stx-andmap Unit? #'(τ_unit ...))
- (string-append
- "all begin expressions except the last one should have type Unit\n"
- (string-join
- (stx-map
- (λ (e τ) (format "~a : ~a" (syntax->datum e) (syntax->datum τ)))
- #'(e_unit ...) #'(τ_unit ...))
- "\n")
- "\n")
(⊢ (begin e_unit- ... e-) : τ)]))
(define-syntax (ann stx)
(syntax-parse stx #:datum-literals (:)
- [(_ e : ascribed-τ)
+ [(_ e : ascribed-τ:type)
#:with (e- τ) (infer+erase #'e)
- #:fail-unless (typecheck? #'τ #'ascribed-τ)
+ #:fail-unless (typecheck? #'τ #'ascribed-τ.norm)
(format "~a does not have type ~a\n"
(syntax->datum #'e) (syntax->datum #'ascribed-τ))
(⊢ e- : ascribed-τ)]))
@@ -123,7 +127,7 @@
[(_ ([b:typed-binding e] ...) e_body)
#:with ((x- ...) (e- ... e_body-) (τ ... τ_body))
(infers/type-ctxt+erase #'(b ...) #'(e ... e_body))
- #:fail-unless (typechecks? #'(b.τ ...) #;(type-evals #'(b.τ ...)) #'(τ ...))
+ #:fail-unless (typechecks? #'(b.τ ...) #'(τ ...))
(string-append
"type check fail, args have wrong type:\n"
(string-join
diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt
@@ -1,7 +1,8 @@
#lang racket/base
(require "typecheck.rkt")
(require (except-in "sysf.rkt" #%app λ Int #%datum → Λ inst ∀ + type-eval)
- (prefix-in sysf: (only-in "sysf.rkt" #%app λ Int → ∀ type-eval)))
+ (prefix-in sysf: (only-in "sysf.rkt" #%app λ Int → ∀ type-eval))
+ (only-in "stlc+reco+var.rkt" same-types?))
(provide (rename-out [app/tc #%app] [λ/tc λ] [datum/tc #%datum]))
(provide (except-out (all-from-out "sysf.rkt")
sysf:Int sysf:→ sysf:∀
@@ -21,8 +22,7 @@
(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]))]))
+ #'(define-syntax alias (syntax-parser [x:id #'τ]))]))
(begin-for-syntax
;; extend type-eval to handle tyapp
@@ -49,7 +49,7 @@
(current-type-eval type-eval))
(define-base-type ★)
-(define-type-constructor ⇒)
+(define-type-constructor (⇒ k_in ... k_out))
;; for now, handle kind checking in the types themselves
;; TODO: move kind checking to a common place (like #%app)?
@@ -59,8 +59,8 @@
;; so I dont have to manually add kinds to all types
(define-base-type Str)
(provide String)
-(define-syntax String (syntax-parser [x:id (⊢ #'Str #'★)]))
-(define-syntax Int (syntax-parser [x:id (⊢ #'sysf:Int #'★)]))
+(define-syntax String (syntax-parser [x:id (⊢ Str : ★)]))
+(define-syntax Int (syntax-parser [x:id (⊢ sysf:Int : ★)]))
;; → in Fω is not first-class, can't pass it around
(define-syntax (→ stx)
@@ -69,20 +69,24 @@
#:with ([τ- k] ... [τ_res- k_res]) (infers+erase #'(τ ... τ_res))
#:when (typecheck? #'k_res #'★)
#:when (same-types? #'(k ... k_res))
- (⊢ #'(sysf:→ τ- ... τ_res-) #'★)]))
+ (⊢ (sysf:→ (#%plain-type τ-) ... (#%plain-type τ_res-)) : ★)]))
(define-syntax (∀ stx)
(syntax-parse stx
[(∀ (b:typed-binding ...) τ)
- #:with (tvs- τ- k) (infer/type-ctxt+erase #'(b ...) #'τ)
+ #:with ((tv- ...) τ- k) (infer/type-ctxt+erase #'(b ...) #'τ)
#:when (typecheck? #'k #'★)
- (⊢ #'(#%plain-lambda tvs- b.τ ... τ-) #;#'(sysf:∀ tvs- τ-) #'★)]))
+ (⊢ (#%type
+ (λ (tv- ...)
+ (let-syntax ([tv- (syntax-parser [tv-:id #'(#%type tv-)])] ...)
+ b.τ ... τ-))) #;(sysf:∀ #:bind tvs- τ-) : ★)]))
(define-syntax (Λ stx)
(syntax-parse stx
[(_ (b:typed-binding ...) e)
#:with ((tv- ...) e- τ) (infer/type-ctxt+erase #'(b ...) #'e)
- (⊢ #'e- #'(∀ ([tv- : b.τ] ...) τ))]))
+ #:when (displayln #'(∀ ([tv- : b.τ] ...) τ))
+ (⊢ e- : (∀ ([tv- : b.τ] ...) τ))]))
(define-syntax (inst stx)
(syntax-parse stx
[(_ e τ:type ...)
@@ -90,7 +94,7 @@
#:with (e- ∀τ) (infer+erase #'e)
#:with ((~literal #%plain-lambda) (tv ...) k_tv ... τ_body) #'∀τ
#:when (typechecks? #'(k ...) #'(k_tv ...))
- (⊢ #'e- (substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))
+ (⊢ e- : #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))
;; TODO: merge with regular λ and app?
(define-syntax (tyλ stx)
@@ -98,47 +102,63 @@
[(_ (b:typed-binding ...) τ)
#:with (tvs- τ- k) (infer/type-ctxt+erase #'(b ...) #'τ)
;; b.τ's here are actually kinds
- (⊢ #'(λ tvs- τ-) #'(⇒ b.τ ... k))]))
+ (⊢ (λ tvs- τ-) : (⇒ b.τ ... k))]))
(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 [τ_fn- (~⇒* k_in ... k_out)] (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 (stx-length=? #'(k_arg ...) #'(k ...))
- (string-append
- (format
- "Wrong number of args given to tyλ ~a:\ngiven: "
- (syntax->datum #'τ_fn))
- (string-join
- (map
- (λ (t k) (format "~a : ~a" t k))
- (syntax->datum #'(τ_arg ...))
- (syntax->datum #`#,(stx-map get-orig #'(k_arg ...))))
- ", ")
- (format "\nexpected: ~a argument(s)." (stx-length #'(k ...))))
- #:fail-unless (typechecks? #'(k_arg ...) #'(k ...))
+ #:fail-unless (typechecks? #'(k_arg ...) #'(k_in ...))
(string-append
- (format
- "Arguments to tyλ ~a have wrong type:\ngiven: "
- (syntax->datum #'τ_fn))
- (string-join
- (map
- (λ (t k) (format "~a : ~a" t k))
- (syntax->datum #'(τ_arg ...))
- (syntax->datum #`#,(stx-map get-orig #'(k_arg ...))))
- ", ")
- "\nexpected arguments with type: "
+ (format "~a (~a:~a) Arguments to function ~a have wrong kinds(s), "
+ (syntax-source stx) (syntax-line stx) (syntax-column stx)
+ (syntax->datum #'τ_fn))
+ "or wrong number of arguments:\nGiven:\n"
(string-join
- (map ~a (syntax->datum #`#,(stx-map get-orig #'(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)]))
+ (map (λ (e t) (format " ~a : ~a" e t)) ; indent each line
+ (syntax->datum #'(τ_arg ...))
+ (stx-map type->str #'(k_arg ...)))
+ "\n" #:after-last "\n")
+ (format "Expected: ~a arguments with kind(s): "
+ (stx-length #'(k_in ...)))
+ (string-join (stx-map type->str #'(k_in ...)) ", "))
+ (⊢ (#%app τ_fn- τ_arg- ...) : k_out)]))
+;
+; #:fail-unless (stx-length=? #'(k_arg ...) #'(k ...))
+; (string-append
+; (format
+; "Wrong number of args given to tyλ ~a:\ngiven: "
+; (syntax->datum #'τ_fn))
+; (string-join
+; (map
+; (λ (t k) (format "~a : ~a" t k))
+; (syntax->datum #'(τ_arg ...))
+; (syntax->datum #`#,(stx-map get-orig #'(k_arg ...))))
+; ", ")
+; (format "\nexpected: ~a argument(s)." (stx-length #'(k ...))))
+; #:fail-unless (typechecks? #'(k_arg ...) #'(k ...))
+; (string-append
+; (format
+; "Arguments to tyλ ~a have wrong type:\ngiven: "
+; (syntax->datum #'τ_fn))
+; (string-join
+; (map
+; (λ (t k) (format "~a : ~a" t k))
+; (syntax->datum #'(τ_arg ...))
+; (syntax->datum #`#,(stx-map get-orig #'(k_arg ...))))
+; ", ")
+; "\nexpected arguments with type: "
+; (string-join
+; (map ~a (syntax->datum #`#,(stx-map get-orig #'(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)]))
;; must override #%app and λ and primops to use new →
;; TODO: parameterize →?
@@ -150,52 +170,69 @@
[(_ (b:typed-binding ...) e)
#:when (andmap ★? (stx-map (λ (t) (typeof (expand/df t))) #'(b.τ ...)))
#:with (xs- e- τ_res) (infer/type-ctxt+erase #'(b ...) #'e)
- (⊢ #'(λ xs- e-) #'(→ b.τ ... τ_res))]))
+ (⊢ (λ xs- e-) : (→ b.τ ... τ_res))]))
(define-syntax (app/tc stx)
(syntax-parse stx
[(_ e_fn e_arg ...)
- #:with [e_fn- τ_fn] (infer+erase #'e_fn)
- ;; 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))
- #:with ((~literal #%plain-app) _ τ ... τ_res) #'τ_fn
+ #:with [e_fn- (~→* τ_in ... τ_out)] (infer+erase #'e_fn)
#:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
- #:fail-unless (stx-length=? #'(τ_arg ...) #'(τ ...))
+ #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
(string-append
- (format
- "Wrong number of args given to function ~a:\ngiven: "
- (syntax->datum #'e_fn))
- (string-join
- (map
- (λ (e t) (format "~a : ~a" e t))
- (syntax->datum #'(e_arg ...))
- (syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
- ", ")
- (format "\nexpected: ~a argument(s)." (stx-length #'(τ ...))))
- #:fail-unless (typechecks? #'(τ_arg ...) #'(τ ...))
- (string-append
- (format
- "Arguments to function ~a have wrong type:\ngiven: "
- (syntax->datum #'e_fn))
- (string-join
- (map
- (λ (e t) (format "~a : ~a" e t))
- (syntax->datum #'(e_arg ...))
- (syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
- ", ")
- "\nexpected arguments with type: "
+ (format "~a (~a:~a) Arguments to function ~a have wrong type(s), "
+ (syntax-source stx) (syntax-line stx) (syntax-column stx)
+ (syntax->datum #'e_fn))
+ "or wrong number of arguments:\nGiven:\n"
(string-join
- (map ~a (syntax->datum #`#,(stx-map get-orig #'(τ ...))))
- ", "))
- (⊢ #'(#%app e_fn- e_arg- ...) #'τ_res)]))
+ (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)]))
+; #:with [e_fn- τ_fn] (infer+erase #'e_fn)
+; ;; 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))
+; #:with ((~literal #%plain-app) _ τ ... τ_res) #'τ_fn
+; #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
+; #:fail-unless (stx-length=? #'(τ_arg ...) #'(τ ...))
+; (string-append
+; (format
+; "Wrong number of args given to function ~a:\ngiven: "
+; (syntax->datum #'e_fn))
+; (string-join
+; (map
+; (λ (e t) (format "~a : ~a" e t))
+; (syntax->datum #'(e_arg ...))
+; (syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
+; ", ")
+; (format "\nexpected: ~a argument(s)." (stx-length #'(τ ...))))
+; #:fail-unless (typechecks? #'(τ_arg ...) #'(τ ...))
+; (string-append
+; (format
+; "Arguments to function ~a have wrong type:\ngiven: "
+; (syntax->datum #'e_fn))
+; (string-join
+; (map
+; (λ (e t) (format "~a : ~a" e t))
+; (syntax->datum #'(e_arg ...))
+; (syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
+; ", ")
+; "\nexpected arguments with type: "
+; (string-join
+; (map ~a (syntax->datum #`#,(stx-map get-orig #'(τ ...))))
+; ", "))
+; (⊢ (#%app e_fn- e_arg- ...) : τ_res)]))
;; must override #%datum to use new kinded-Int, etc
(define-syntax (datum/tc stx)
(syntax-parse stx
- [(_ . n:integer) (⊢ (syntax/loc stx (#%datum . n)) #'Int)]
- [(_ . s:str) (⊢ (syntax/loc stx (#%datum . s)) #'String)]
+ [(_ . n:integer) (⊢ (#%datum . n) : Int)]
+ [(_ . s:str) (⊢ (#%datum . s) : String)]
[(_ . x)
#:when (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)
#'(#%datum . x)]))
\ No newline at end of file
diff --git a/tapl/notes.txt b/tapl/notes.txt
@@ -1,3 +1,25 @@
+2015-08-13
+Requirements for define-type-constructor syntax:
+- identifier types, like Int
+- basic tuples, like arrow
+ - arity
+- nested tuples, like records
+- binding forms, like forall
+
+Problem:
+Types must be expanded, to check that they are valid, catch unbound ids, etc.
+But should I attach the expanded type to a term, or the original surface stx?
+- maybe this is just repeating the same thing I wrote below?
+- Related question: fully expand types before calling type=? or typecheck?
+Answer: must only compare fully expanded forms, otherwise these will not work
+- define-type-alias
+Rules:
+- all user-written types must be expanded and checked
+ - check for invalid types, unbound ids
+- use expanded types (when available) to create new types
+- expand all types before attaching
+- assume types are expanded in type=? and typechecks
+
2015-07-31
Problem: pattern-expander not being recognized
Solution: syntax-parse pattern directives must begin with ~ prefix
diff --git a/tapl/stlc+box.rkt b/tapl/stlc+box.rkt
@@ -13,7 +13,8 @@
;; Terms:
;; - terms from stlc+cons.rkt
-(define-type-constructor (Ref τ) #:declare τ type)
+;(define-type-constructor (Ref τ) #:declare τ type)
+(define-basic-checked-stx Ref #:arity = 1)
(define-syntax (ref stx)
(syntax-parse stx
@@ -23,16 +24,14 @@
(define-syntax (deref stx)
(syntax-parse stx
[(_ e)
+; #:with (e- (~Ref* τ)) (infer+erase #'e) ; alternate pattern; worse err msg
#:with (e- (τ)) (inferRef+erase #'e)
-; #:with (e- ref-τ) (infer+erase #'e)
-; #:with τ (Ref-get τ from ref-τ)
(⊢ (unbox e-) : τ)]))
(define-syntax (:= stx)
(syntax-parse stx
[(_ e_ref e)
#:with (e_ref- (τ1)) (inferRef+erase #'e_ref)
-; #:with (e_ref- ref-τ) (infer+erase #'e_ref)
-; #:with τ1 (Ref-get τ from ref-τ)
+; #:with (e_ref- (~Ref* τ1)) (infer+erase #'e_ref) ; alt pattern; worse err msg
#:with (e- τ2) (infer+erase #'e)
#:when (typecheck? #'τ1 #'τ2)
(⊢ (set-box! e_ref- e-) : Unit)]))
\ No newline at end of file
diff --git a/tapl/stlc+cons.rkt b/tapl/stlc+cons.rkt
@@ -15,7 +15,8 @@
;; TODO: enable HO use of list primitives
-(define-type-constructor (List τ) #:declare τ type)
+;(define-type-constructor (List τ) #:declare τ type)
+(define-basic-checked-stx List #:arity = 1)
(define-syntax (nil stx)
(syntax-parse stx
@@ -28,7 +29,7 @@
(syntax-parse stx
[(_ e1 e2)
#:with (e1- τ1) (infer+erase #'e1)
- #:with (e2- (~List τ2)) (infer+erase #'e2)
+ #:with (e2- (τ2)) (inferList+erase #'e2)
; #:with (e2- τ-lst) (infer+erase #'e2)
; #:with τ2 (List-get τ from τ-lst)
#:when (typecheck? #'τ1 #'τ2)
diff --git a/tapl/stlc+lit.rkt b/tapl/stlc+lit.rkt
@@ -16,6 +16,8 @@
(define-base-type Int)
+;(define-base-type Int)
+
(define-primop + : (→ Int Int Int))
(define-syntax (datum/tc stx)
diff --git a/tapl/stlc+rec-iso.rkt b/tapl/stlc+rec-iso.rkt
@@ -17,17 +17,25 @@
;; - terms from stlc+reco+var.rkt
;; - fld/unfld
-(define-type-constructor
+#;(define-type-constructor
(μ [[tv]] τ_body))
-; can't enforce this because bound ids wont have #%type tag
- ;#:declare τ_body type)
-#;(define-syntax (μ stx)
- (syntax-parse stx
+(define-syntax μ
+ (syntax-parser
[(_ (tv:id) τ_body)
- #'(#%type
- (λ (tv)
- (let-syntax ([tv (syntax-parser [tv:id #'(#%type tv)])])
- τ_body)))]))
+ #:with ((tv-) τ_body- k) (infer/ctx+erase #'([tv : #%type]) #'τ_body)
+ #:when (#%type? #'k)
+ (mk-type #'(λ (tv-) τ_body-))]))
+(begin-for-syntax
+ (define-syntax ~μ*
+ (pattern-expander
+ (syntax-parser
+ [(_ (tv:id) τ)
+ #'(~or
+ ((~literal #%plain-lambda) (tv) τ)
+ (~and any (~do
+ (type-error
+ #:src #'any
+ #:msg "Expected μ type, got: ~a" #'any))))]))))
(begin-for-syntax
;; extend to handle μ
@@ -48,7 +56,7 @@
(define-syntax (unfld stx)
(syntax-parse stx
[(_ τ:ann e)
- #:with (~μ [[tv]] τ_body) #'τ.norm
+ #:with (~μ* (tv) τ_body) #'τ.norm
; #:with ((~literal #%plain-lambda) (tv:id) τ_body) #'τ.norm
#:with [e- τ_e] (infer+erase #'e)
#:when (typecheck? #'τ_e #'τ.norm)
@@ -56,7 +64,7 @@
(define-syntax (fld stx)
(syntax-parse stx
[(_ τ:ann e)
- #:with (~μ [[tv]] τ_body) #'τ.norm
+ #:with (~μ* (tv) τ_body) #'τ.norm
; #:with ((~literal #%plain-type) ((~literal #%plain-lambda) (tv:id) τ_body)) #'τ.norm
#:with [e- τ_e] (infer+erase #'e)
#:when (typecheck? #'τ_e (subst #'τ.norm #'tv #'τ_body))
diff --git a/tapl/stlc+reco+sub.rkt b/tapl/stlc+reco+sub.rkt
@@ -28,11 +28,12 @@
(begin-for-syntax
(define (sub? τ1 τ2)
(or
- (syntax-parse (list τ1 τ2) #:literals (× ∨ quote)
- [(tup1 tup2)
- #:when (and (×? #'tup1) (×? #'tup2))
- #:with (['k:str τk] ...) (stx-map :-args (×-args #'tup1))
- #:with (['l:str τl] ...) (stx-map :-args (×-args #'tup2))
+ (syntax-parse (list τ1 τ2) #:literals (quote)
+ [((~× [: 'k τk] ...) (~× [: 'l τl] ...))
+; [(tup1 tup2)
+; #:when (and (×? #'tup1) (×? #'tup2))
+; #:with (['k:str τk] ...) (stx-map :-args (×-args #'tup1))
+; #:with (['l:str τl] ...) (stx-map :-args (×-args #'tup2))
#:when (subset? (stx-map syntax-e (syntax->list #'(l ...)))
(stx-map syntax-e (syntax->list #'(k ...))))
(stx-andmap
@@ -41,10 +42,11 @@
#:with (k_match τk_match) (str-stx-assoc #'l #'([k τk] ...))
((current-sub?) #'τk_match #'τl)])
#'([l τl] ...))]
- [(var1 var2)
- #:when (and (∨? #'var1) (∨? #'var2))
- #:with (['k:str τk] ...) (stx-map :-args (∨-args #'var1))
- #:with (['l:str τl] ...) (stx-map :-args (∨-args #'var2))
+ [((~∨ [<> 'k τk] ...) (~∨ [<> 'l τl] ...))
+; [(var1 var2)
+; #:when (and (∨? #'var1) (∨? #'var2))
+; #:with (['k:str τk] ...) (stx-map :-args (∨-args #'var1))
+; #:with (['l:str τl] ...) (stx-map :-args (∨-args #'var2))
#:when (subset? (stx-map syntax-e (syntax->list #'(l ...)))
(stx-map syntax-e (syntax->list #'(k ...))))
(stx-andmap
diff --git a/tapl/stlc+reco+var.rkt b/tapl/stlc+reco+var.rkt
@@ -1,14 +1,15 @@
#lang racket/base
(require "typecheck.rkt")
-(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app begin tup proj let type=?))
- (except-in "stlc+tup.rkt" #%app begin tup proj let type=? × ~×))
+(require (only-in racket/bool symbol=?))
+(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app begin let #;type=? × infer×+erase))
+ (except-in "stlc+tup.rkt" #%app begin tup proj let #;type=? × infer×+erase))
(provide (rename-out [stlc:#%app #%app] [stlc:let let] [stlc:begin begin]
[define/tc define]))
(provide (except-out (all-from-out "stlc+tup.rkt")
- stlc:#%app stlc:let stlc:begin stlc:tup stlc:proj
- (for-syntax stlc:type=?)))
-(provide tup proj var case)
-(provide (for-syntax type=?))
+ stlc:#%app stlc:let stlc:begin stlc:×
+ (for-syntax #;stlc:type=? stlc:infer×+erase)))
+(provide tup proj × var case ∨)
+(provide (for-syntax #;type=? same-types?))
;; Simply-Typed Lambda Calculus, plus records and variants
@@ -29,15 +30,15 @@
(begin-for-syntax
; extend to:
; 1) accept strings (ie, record labels)
- (define (type=? τ1 τ2)
+ #;(define (type=? τ1 τ2)
; (printf "t1 = ~a\n" (syntax->datum τ1))
; (printf "t2 = ~a\n" (syntax->datum τ2))
(syntax-parse (list τ1 τ2)
[(s1:str s2:str) (string=? (syntax-e #'s1) (syntax-e #'s2))]
[_ (stlc:type=? τ1 τ2)]))
- (current-type=? type=?)
- (current-typecheck-relation (current-type=?))
+ ;(current-type=? type=?)
+ ;(current-typecheck-relation (current-type=?))
(define (same-types? τs)
(define τs-lst (syntax->list τs))
@@ -50,12 +51,23 @@
[(_ alias:id τ:type)
; must eval, otherwise undefined types will be allowed
;#'(define-syntax alias (syntax-parser [x:id #'τ.norm]))]))
- #'(define-syntax alias (syntax-parser [x:id #'τ]))]))
+ #'(define-syntax alias (syntax-parser [x:id #'τ.norm]))]))
;(define-type-constructor [: str τ] #:lits (:))
; re-define tuples as records
-(define-type-constructor
+(define-syntax ×
+ (syntax-parser #:datum-literals (:)
+ [(_ [label:id : τ:type] ...)
+ #:with (valid-τ ...) (stx-map mk-type #'(('label τ.norm) ...))
+ #`(stlc:× valid-τ ...)]))
+(define-for-syntax (infer×+erase e)
+ (syntax-parse (stlc:infer×+erase e) #:context e
+ [(e- τ_e)
+ #:with (((~literal #%plain-app) (quote l) τ) ...) #'τ_e
+ #'(e- ((l τ) ...))]))
+
+#;(define-type-constructor
;(× [~× label τ_fld] ...) #:lits (~×)
(× [: label τ_fld] ...) #:lits (:)
#:declare label str
@@ -67,46 +79,109 @@
;; records
(define-syntax (tup stx)
(syntax-parse stx #:datum-literals (=)
- [(_ [l:str = e] ...)
+ [(_ [l:id = e] ...)
#:with ([e- τ] ...) (infers+erase #'(e ...))
;(⊢ (list (list l e-) ...) : (× [~× l τ] ...))]
- (⊢ (list (list l e-) ...) : (× [: l τ] ...))]
+ (⊢ (list (list 'l e-) ...) : (× [l : τ] ...))]
#;[(_ e ...)
#'(stlc:tup e ...)]))
(define-syntax (proj stx)
(syntax-parse stx #:literals (quote)
- [(_ e_rec l:str)
- #:with (e_rec- (~× [: 'l_τ τ] ...)) (infer+erase #'e_rec)
+ [(_ e_rec l:id)
+; #:with (e_rec- (~×* [: 'l_τ τ] ...)) (infer+erase #'e_rec)
+ #:with (e_rec- ([l_τ τ] ...)) (infer×+erase #'e_rec)
; #:with [rec- τ_rec] (infer+erase #'e_rec) ; match method #2: get
; #:with ('l_τ:str ...) (×-get label from τ_rec)
; #:with (τ ...) (×-get τ_fld from τ_rec)
- #:with (l_match:str τ_match) (str-stx-assoc #'l #'([l_τ τ] ...))
- (⊢ (cadr (assoc l e_rec-)) : τ_match)]
+ #:with (_ τ_match) (stx-assoc #'l #'([l_τ τ] ...))
+ (⊢ (cadr (assoc 'l e_rec-)) : τ_match)]
#;[(_ e ...) #'(stlc:proj e ...)]))
+(define-basic-checked-stx ∨/internal)
+
+; re-define tuples as records
+(define-syntax ∨
+ (syntax-parser #:datum-literals (:)
+ [(_ (~and [label:id : τ:type] x) ...)
+ #:when (> (stx-length #'(x ...)) 0)
+ #:with (valid-τ ...) (stx-map mk-type #'(('label τ.norm) ...))
+ #'(∨/internal valid-τ ...)]
+ [any
+ (type-error #:src #'any
+ #:msg (string-append
+ "Improper usage of type constructor ∨: ~a, expected (∨ [label:id : τ:type] ...+)")
+ #'any)]))
+(begin-for-syntax
+ (define (infer∨+erase e)
+ (syntax-parse (infer+erase e) #:context e
+ [(e- τ_e)
+ #:fail-unless (∨/internal? #'τ_e)
+ (format
+ "~a (~a:~a): Expected expression ~a to have ∨ type, got: ~a"
+ (syntax-source e) (syntax-line e) (syntax-column e)
+ (syntax->datum e) (type->str #'τ_e))
+ #:with (~∨/internal ((~literal #%plain-app) (quote l) τ) ...) #'τ_e
+ #'(e- ((l τ) ...))]))
+ (define-syntax ~∨*
+ (pattern-expander
+ (syntax-parser #:datum-literals (:)
+ [(_ [l : τ_l] (~and ddd (~literal ...)))
+ #'(~or (~∨/internal ((~literal #%plain-app) (quote l) τ_l) ddd)
+ (~and any (~do (type-error
+ #:src #'any
+ #:msg "Expected ∨ type, got: ~a" #'any))))]))))
-(define-type-constructor
+#;(define-type-constructor
(∨ [<> label τ_var] ...) #:lits (<>)
#:declare label str
#:declare τ_var type)
(define-syntax (var stx)
+ (syntax-parse stx #:datum-literals (as =)
+ [(_ l:id = e as τ:type)
+; #:when (∨? #'τ.norm)
+; #:with (['l_τ:str τ_l] ...) (stx-map :-args (∨-args #'τ.norm))
+ #:with (~∨* [l_τ : τ_l] ...) #'τ.norm
+; #:with ('l_τ:str ...) (∨-get label from τ)
+; #:with (τ_l ...) (∨-get τ_var from τ)
+ #:with (_ τ_match) (stx-assoc #'l #'((l_τ τ_l) ...))
+ #:with (e- τ_e) (infer+erase #'e)
+ #:when (typecheck? #'τ_e #'τ_match)
+ (⊢ (list 'l e) : τ)]))
+(define-syntax (case stx)
+ (syntax-parse stx #:datum-literals (of =>)
+ [(_ e [l:id x:id => e_l] ...)
+ #:fail-when (null? (syntax->list #'(l ...))) "no clauses"
+; #:with (e- (~∨* [<> 'l_x τ_x] ...)) (infer+erase #'e)
+ #:with (e- ([l_x τ_x] ...)) (infer∨+erase #'e)
+; #:with ('l_x:str ...) (∨-get label from τ_e)
+; #:with (τ_x ...) (∨-get τ_var from τ_e)
+ #:fail-unless (= (stx-length #'(l ...)) (stx-length #'(l_x ...))) "wrong number of case clauses"
+ #:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive"
+ #:with (((x-) e_l- τ_el) ...)
+ (stx-map (λ (bs e) (infer/type-ctxt+erase bs e)) #'(([x : τ_x]) ...) #'(e_l ...))
+ #:fail-unless (same-types? #'(τ_el ...)) "branches have different types"
+ (⊢ (let ([l_e (car e-)])
+ (cond [(symbol=? l_e 'l) (let ([x- (cadr e-)]) e_l-)] ...))
+ : #,(stx-car #'(τ_el ...)))]))
+
+#;(define-syntax (var stx)
(syntax-parse stx #:datum-literals (as =) #:literals (quote)
[(_ l:str = e as τ:type)
; #:when (∨? #'τ.norm)
; #:with (['l_τ:str τ_l] ...) (stx-map :-args (∨-args #'τ.norm))
- #:with (~∨ [<> 'l_τ τ_l] ...) #'τ.norm
+ #:with (~∨* [<> 'l_τ τ_l] ...) #'τ.norm
; #:with ('l_τ:str ...) (∨-get label from τ)
; #:with (τ_l ...) (∨-get τ_var from τ)
#:with (l_match:str τ_match) (str-stx-assoc #'l #'((l_τ τ_l) ...))
#:with (e- τ_e) (infer+erase #'e)
#:when (typecheck? #'τ_e #'τ_match)
(⊢ (list l e) : τ)]))
-(define-syntax (case stx)
+#;(define-syntax (case stx)
(syntax-parse stx #:datum-literals (of =>) #:literals (quote)
[(_ e [l:str x => e_l] ...)
#:fail-when (null? (syntax->list #'(l ...))) "no clauses"
- #:with (e- (~∨ [<> 'l_x τ_x] ...)) (infer+erase #'e)
+ #:with (e- (~∨* [<> 'l_x τ_x] ...)) (infer+erase #'e)
; #:with ('l_x:str ...) (∨-get label from τ_e)
; #:with (τ_x ...) (∨-get τ_var from τ_e)
#:fail-unless (= (stx-length #'(l ...)) (stx-length #'(l_x ...))) "wrong number of case clauses"
diff --git a/tapl/stlc+sub.rkt b/tapl/stlc+sub.rkt
@@ -31,26 +31,26 @@
(define-syntax (datum/tc stx)
(syntax-parse stx
- [(_ . n:nat) (⊢ (syntax/loc stx (#%datum . n)) #'Nat)]
- [(_ . n:integer) (⊢ (syntax/loc stx (#%datum . n)) #'Int)]
- [(_ . n:number) (⊢ (syntax/loc stx (#%datum . n)) #'Num)]
+ [(_ . n:nat) (⊢ (#%datum . n) : Nat)]
+ [(_ . n:integer) (⊢ (#%datum . n) : Int)]
+ [(_ . n:number) (⊢ (#%datum . n) : Num)]
[(_ . x) #'(stlc:#%datum . x)]))
(begin-for-syntax
(define (sub? τ1 τ2)
+ ; only need this because recursive calls made with unexpanded types
+ (define τ1 ((current-type-eval) t1))
+ (define τ2 ((current-type-eval) t2))
; (printf "t1 = ~a\n" (syntax->datum τ1))
; (printf "t2 = ~a\n" (syntax->datum τ2))
(or ((current-type=?) τ1 τ2)
- (syntax-parse (list τ1 τ2) #:literals (Nat Int Num Top)
- [(_ Top) #t]
- [(Nat τ) ((current-sub?) #'Int #'τ)]
- [(Int τ) ((current-sub?) #'Num #'τ)]
- [(τ Num) ((current-sub?) #'τ #'Int)]
- [(τ Int) ((current-sub?) #'τ #'Nat)]
- [(arr1 arr2)
- #:when (and (→? #'arr1) (→? #'arr2))
- #:with (s1 ... s2) (→-args #'arr1)
- #:with (t1 ... t2) (→-args #'arr2)
+ (syntax-parse (list τ1 τ2)
+ [(_ ~Top) #t]
+ [(~Nat τ) ((current-sub?) #'Int #'τ)]
+ [(~Int τ) ((current-sub?) #'Num #'τ)]
+ [(τ ~Num) ((current-sub?) #'τ #'Int)]
+ [(τ ~Int) ((current-sub?) #'τ #'Nat)]
+ [((~→ s1 ... s2) (~→ t1 ... t2))
(and (subs? #'(t1 ...) #'(s1 ...))
((current-sub?) #'s2 #'t2))]
[_ #f])))
diff --git a/tapl/stlc+tup.rkt b/tapl/stlc+tup.rkt
@@ -14,7 +14,8 @@
;; - terms from ext-stlc.rkt
;; - tup and proj
-(define-type-constructor (× τ ...) #:declare τ type)
+(define-basic-checked-stx ×)
+;(define-type-constructor (× τ ...) #:declare τ type)
(define-syntax (tup stx)
(syntax-parse stx
diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt
@@ -21,9 +21,8 @@
;; - may require some caution when mixing expanded and unexpanded types to
;; create other types
(define (type-eval τ)
- (if (plain-type? τ) ; don't expand if already expanded
- τ
- (add-orig #`(#%plain-type #,(expand/df τ)) τ)))
+ (or (plain-type? τ) ; don't expand if already expanded
+ (add-orig (expand/df τ) τ)))
(current-type-eval type-eval)
@@ -48,7 +47,9 @@
(define current-type=? (make-parameter type=?))
(current-typecheck-relation type=?))
-(define-type-constructor (→ τ_in ... τ_out)
+(define-basic-checked-stx → #:arity >= 1)
+
+#;(define-type-constructor (→ τ_in ... τ_out)
#:declare τ_in type
#:declare τ_out type)
@@ -62,11 +63,11 @@
(syntax-parse stx
[(_ e_fn e_arg ...)
;; 2015-08-06: there are currently three alternative tycon matching syntaxes
- #:with [e_fn- (~→ τ_in ... τ_out)] (infer+erase #'e_fn) ; #1 (external) pattern expander
+; #:with [e_fn- (~→* τ_in ... τ_out)] (infer→+erase #'e_fn) ; #1 (external) pattern expander
;#:with [e_fn- τ_fn] (infer+erase #'e_fn) ; #2 get, via (internal) pattern expander
;#:with (τ_in ...) (→-get τ_in from #'τ_fn)
;#:with τ_out (→-get τ_out from #'τ_fn)
- ;#:with [e_fn- (τ_in ... τ_out)] (infer→+erase #'e_fn) ; #3 work directly on term
+ #:with [e_fn- (τ_in ... τ_out)] (infer→+erase #'e_fn) ; #3 work directly on term -- better err msg
#:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
(string-append
diff --git a/tapl/stx-utils.rkt b/tapl/stx-utils.rkt
@@ -2,7 +2,7 @@
(require syntax/stx racket/list)
(provide (all-defined-out))
-(define (stx-cadr stx) (car (stx-cdr stx)))
+(define (stx-cadr stx) (stx-car (stx-cdr stx)))
(define (stx-andmap f . stx-lsts)
(apply andmap f (map syntax->list stx-lsts)))
@@ -23,6 +23,8 @@
(member (datum->syntax v) (map datum->syntax (syntax->list stx)) string=?))
(define (str-stx-assoc v stx)
(assoc v (map syntax->list (syntax->list stx)) stx-str=?))
+(define (stx-assoc v stx) ; v = id
+ (assoc v (map syntax->list (syntax->list stx)) free-identifier=?))
(define (stx-length stx) (length (syntax->list stx)))
(define (stx-length=? stx1 stx2)
diff --git a/tapl/sysf.rkt b/tapl/sysf.rkt
@@ -20,12 +20,13 @@
;; - Λ and inst
;; dont use define-type-constructor, instead define explicit macro
-(provide ∀)
-(define-syntax (∀ stx)
+;(provide ∀)
+#;(define-syntax (∀ stx)
(syntax-parse stx
[(_ (x:id ...) body) ; cannot use :type annotation on body bc of unbound vars
;; use #%plain-lambda to avoid insertion of #%expression
(syntax/loc stx (#%plain-lambda (x ...) body))]))
+(define-type-constructor (∀ [[x ...]] body))
(begin-for-syntax
;; extend to handle ∀
@@ -44,11 +45,12 @@
(define-syntax (Λ stx)
(syntax-parse stx
[(_ (tv:id ...) e)
- #:with (tvs- e- τ) (infer/tvs+erase #'e #'(tv ...))
- (⊢ #'e- #'(∀ tvs- τ))]))
+ #:with ((tv- ...) e- τ) (infer/tvs+erase #'e #'(tv ...))
+ (⊢ e- : (∀ #:bind (tv- ...) τ))]))
(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))]))
-\ No newline at end of file
+ #:with (e- (~∀* [[tv ...]] τ_body)) (infer+erase #'e)
+; #:with (e- ∀τ) (infer+erase #'e)
+; #:with ((~literal #%plain-lambda) (tv ...) τ_body) #'∀τ
+ (⊢ e- : #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))
+\ No newline at end of file
diff --git a/tapl/tests/exist-tests.rkt b/tapl/tests/exist-tests.rkt
@@ -1,99 +1,99 @@
#lang s-exp "../exist.rkt"
(require "rackunit-typechecking.rkt")
-(check-type (pack (Int 0) as (∃ [[X]] X)) : (∃ [[X]] X))
-(check-type (pack (Int 0) as (∃ [[X]] X)) : (∃ [[Y]] Y))
-(typecheck-fail (pack (Int 0) as (∃ [[X]] Y)))
-(check-type (pack (Bool #t) as (∃ [[X]] X)) : (∃ [[X]] X))
-(typecheck-fail (pack (Int #t) as (∃ [[X]] X)))
+(check-type (pack (Int 0) as (∃ (X) X)) : (∃ (X) X))
+(check-type (pack (Int 0) as (∃ (X) X)) : (∃ (Y) Y))
+(typecheck-fail (pack (Int 0) as (∃ (X) Y)))
+(check-type (pack (Bool #t) as (∃ (X) X)) : (∃ (X) X))
+(typecheck-fail (pack (Int #t) as (∃ (X) X)))
; cant typecheck bc X has local scope, and no X elimination form
-;(check-type (open ([(X x) <= (pack (Int 0) as (∃ [[X]] X))]) x) : X)
+;(check-type (open ([(X x) <= (pack (Int 0) as (∃ (X) X))]) x) : X)
(check-type 0 : Int)
(check-type (+ 0 1) : Int ⇒ 1)
(check-type ((λ ([x : Int]) (+ x 1)) 0) : Int ⇒ 1)
-(typecheck-fail (open ([(X x) <= (pack (Int 0) as (∃ [[X]] X))]) (+ x 1))) ; can't use as Int
+(typecheck-fail (open ([(X x) <= (pack (Int 0) as (∃ (X) X))]) (+ x 1))) ; can't use as Int
-(check-type (λ ([x : (∃ [[X]] X)]) x) : (→ (∃ [[X]] X) (∃ [[Y]] Y)))
-(check-type ((λ ([x : (∃ [[X]] X)]) x) (pack (Int 0) as (∃ [[Z]] Z)))
- : (∃ [[X]] X) ⇒ 0)
-(check-type ((λ ([x : (∃ [[X]] X)]) x) (pack (Bool #t) as (∃ [[Z]] Z)))
- : (∃ [[X]] X) ⇒ #t)
+(check-type (λ ([x : (∃ (X) X)]) x) : (→ (∃ (X) X) (∃ (Y) Y)))
+(check-type ((λ ([x : (∃ (X) X)]) x) (pack (Int 0) as (∃ (Z) Z)))
+ : (∃ (X) X) ⇒ 0)
+(check-type ((λ ([x : (∃ (X) X)]) x) (pack (Bool #t) as (∃ (Z) Z)))
+ : (∃ (X) X) ⇒ #t)
;; example where the two binding X's are conflated, see exist.rkt for explanation
-(check-type (open ([(X x) <= (pack (Int 0) as (∃ [[X]] X))]) ((λ ([y : X]) 1) x))
+(check-type (open ([(X x) <= (pack (Int 0) as (∃ (X) X))]) ((λ ([y : X]) 1) x))
: Int ⇒ 1)
(check-type
- (pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
- as (∃ [[X]] (× [: "a" X] [: "f" (→ X X)])))
- : (∃ [[X]] (× [: "a" X] [: "f" (→ X X)])))
+ (pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))]))
+ as (∃ (X) (× [a : X] [f : (→ X X)])))
+ : (∃ (X) (× [a : X] [f : (→ X X)])))
(define p4
- (pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
- as (∃ [[X]] (× [: "a" X] [: "f" (→ X Int)]))))
-(check-type p4 : (∃ [[X]] (× [: "a" X] [: "f" (→ X Int)])))
+ (pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))]))
+ as (∃ (X) (× [a : X] [f : (→ X Int)]))))
+(check-type p4 : (∃ (X) (× [a : X] [f : (→ X Int)])))
-(check-not-type (open ([(X x) <= p4]) (proj x "a")) : Int) ; type is X, not Int
+(check-not-type (open ([(X x) <= p4]) (proj x a)) : Int) ; type is X, not Int
; type is (→ X X), not (→ Int Int)
-(check-not-type (open ([(X x) <= p4]) (proj x "f")) : (→ Int Int))
-(typecheck-fail (open ([(X x) <= p4]) (+ 1 (proj x "a"))))
-(check-type (open ([(X x) <= p4]) ((proj x "f") (proj x "a"))) : Int ⇒ 6)
-(check-type (open ([(X x) <= p4]) ((λ ([y : X]) ((proj x "f") y)) (proj x "a"))) : Int ⇒ 6)
+(check-not-type (open ([(X x) <= p4]) (proj x f)) : (→ Int Int))
+(typecheck-fail (open ([(X x) <= p4]) (+ 1 (proj x a))))
+(check-type (open ([(X x) <= p4]) ((proj x f) (proj x a))) : Int ⇒ 6)
+(check-type (open ([(X x) <= p4]) ((λ ([y : X]) ((proj x f) y)) (proj x a))) : Int ⇒ 6)
(check-type
- (open ([(X x) <= (pack (Int 0) as (∃ [[Y]] Y))])
+ (open ([(X x) <= (pack (Int 0) as (∃ (Y) Y))])
((λ ([y : X]) 1) x))
: Int ⇒ 1)
(check-type
- (pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
- as (∃ [[X]] (× [: "a" Int] [: "f" (→ Int Int)])))
- : (∃ [[X]] (× [: "a" Int] [: "f" (→ Int Int)])))
+ (pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))]))
+ as (∃ (X) (× [a : Int] [f : (→ Int Int)])))
+ : (∃ (X) (× [a : Int] [f : (→ Int Int)])))
(typecheck-fail
- (pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
- as (∃ [[X]] (× [: "a" Int] [: "f" (→ Bool Int)]))))
+ (pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))]))
+ as (∃ (X) (× [a : Int] [f : (→ Bool Int)]))))
(typecheck-fail
- (pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
- as (∃ [[X]] (× [: "a" X] [: "f" (→ X Bool)]))))
+ (pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))]))
+ as (∃ (X) (× [a : X] [f : (→ X Bool)]))))
(check-type
- (pack (Bool (tup ["a" = #t] ["f" = (λ ([x : Bool]) (if x 1 2))]))
- as (∃ [[X]] (× [: "a" X] [: "f" (→ X Int)])))
- : (∃ [[X]] (× [: "a" X] [: "f" (→ X Int)])))
+ (pack (Bool (tup [a = #t] [f = (λ ([x : Bool]) (if x 1 2))]))
+ as (∃ (X) (× [a : X] [f : (→ X Int)])))
+ : (∃ (X) (× [a : X] [f : (→ X Int)])))
(define counterADT
- (pack (Int (tup ["new" = 1]
- ["get" = (λ ([i : Int]) i)]
- ["inc" = (λ ([i : Int]) (+ i 1))]))
- as (∃ [[Counter]] (× [: "new" Counter]
- [: "get" (→ Counter Int)]
- [: "inc" (→ Counter Counter)]))))
+ (pack (Int (tup [new = 1]
+ [get = (λ ([i : Int]) i)]
+ [inc = (λ ([i : Int]) (+ i 1))]))
+ as (∃ (Counter) (× [new : Counter]
+ [get : (→ Counter Int)]
+ [inc : (→ Counter Counter)]))))
(check-type counterADT :
- (∃ [[Counter]] (× [: "new" Counter]
- [: "get" (→ Counter Int)]
- [: "inc" (→ Counter Counter)])))
+ (∃ (Counter) (× [new : Counter]
+ [get : (→ Counter Int)]
+ [inc : (→ Counter Counter)])))
(check-type
(open ([(Counter counter) <= counterADT])
- ((proj counter "get") ((proj counter "inc") (proj counter "new"))))
+ ((proj counter get) ((proj counter inc) (proj counter new))))
: Int ⇒ 2)
(check-type
(open ([(Counter counter) <= counterADT])
- (let ([inc (proj counter "inc")]
- [get (proj counter "get")])
+ (let ([inc (proj counter inc)]
+ [get (proj counter get)])
(let ([add3 (λ ([c : Counter]) (inc (inc (inc c))))])
- (get (add3 (proj counter "new"))))))
+ (get (add3 (proj counter new))))))
: Int ⇒ 4)
(check-type
(open ([(Counter counter) <= counterADT])
- (let ([get (proj counter "get")]
- [inc (proj counter "inc")]
- [new (λ () (proj counter "new"))])
+ (let ([get (proj counter get)]
+ [inc (proj counter inc)]
+ [new (λ () (proj counter new))])
(letrec ([(is-even? : (→ Int Bool))
(λ ([n : Int])
(or (zero? n)
@@ -103,38 +103,38 @@
(and (not (zero? n))
(is-even? (sub1 n))))])
(open ([(FlipFlop flipflop) <=
- (pack (Counter (tup ["new" = (new)]
- ["read" = (λ ([c : Counter]) (is-even? (get c)))]
- ["toggle" = (λ ([c : Counter]) (inc c))]
- ["reset" = (λ ([c : Counter]) (new))]))
- as (∃ [[FlipFlop]] (× [: "new" FlipFlop]
- [: "read" (→ FlipFlop Bool)]
- [: "toggle" (→ FlipFlop FlipFlop)]
- [: "reset" (→ FlipFlop FlipFlop)])))])
- (let ([read (proj flipflop "read")]
- [togg (proj flipflop "toggle")])
- (read (togg (togg (togg (togg (proj flipflop "new")))))))))))
+ (pack (Counter (tup [new = (new)]
+ [read = (λ ([c : Counter]) (is-even? (get c)))]
+ [toggle = (λ ([c : Counter]) (inc c))]
+ [reset = (λ ([c : Counter]) (new))]))
+ as (∃ (FlipFlop) (× [new : FlipFlop]
+ [read : (→ FlipFlop Bool)]
+ [toggle : (→ FlipFlop FlipFlop)]
+ [reset : (→ FlipFlop FlipFlop)])))])
+ (let ([read (proj flipflop read)]
+ [togg (proj flipflop toggle)])
+ (read (togg (togg (togg (togg (proj flipflop new)))))))))))
: Bool ⇒ #f)
(define counterADT2
- (pack ((× [: "x" Int])
- (tup ["new" = (tup ["x" = 1])]
- ["get" = (λ ([i : (× [: "x" Int])]) (proj i "x"))]
- ["inc" = (λ ([i : (× [: "x" Int])]) (tup ["x" = (+ 1 (proj i "x"))]))]))
- as (∃ [[Counter]] (× [: "new" Counter]
- [: "get" (→ Counter Int)]
- [: "inc" (→ Counter Counter)]))))
+ (pack ((× [x : Int])
+ (tup [new = (tup [x = 1])]
+ [get = (λ ([i : (× [x : Int])]) (proj i x))]
+ [inc = (λ ([i : (× [x : Int])]) (tup [x = (+ 1 (proj i x))]))]))
+ as (∃ (Counter) (× [new : Counter]
+ [get : (→ Counter Int)]
+ [inc : (→ Counter Counter)]))))
(check-type counterADT2 :
- (∃ [[Counter]] (× [: "new" Counter]
- [: "get" (→ Counter Int)]
- [: "inc" (→ Counter Counter)])))
+ (∃ (Counter) (× [new : Counter]
+ [get : (→ Counter Int)]
+ [inc : (→ Counter Counter)])))
;; same as above, but with different internal counter representation
(check-type
(open ([(Counter counter) <= counterADT2])
- (let ([get (proj counter "get")]
- [inc (proj counter "inc")]
- [new (λ () (proj counter "new"))])
+ (let ([get (proj counter get)]
+ [inc (proj counter inc)]
+ [new (λ () (proj counter new))])
(letrec ([(is-even? : (→ Int Bool))
(λ ([n : Int])
(or (zero? n)
@@ -144,19 +144,29 @@
(and (not (zero? n))
(is-even? (sub1 n))))])
(open ([(FlipFlop flipflop) <=
- (pack (Counter (tup ["new" = (new)]
- ["read" = (λ ([c : Counter]) (is-even? (get c)))]
- ["toggle" = (λ ([c : Counter]) (inc c))]
- ["reset" = (λ ([c : Counter]) (new))]))
- as (∃ [[FlipFlop]] (× [: "new" FlipFlop]
- [: "read" (→ FlipFlop Bool)]
- [: "toggle" (→ FlipFlop FlipFlop)]
- [: "reset" (→ FlipFlop FlipFlop)])))])
- (let ([read (proj flipflop "read")]
- [togg (proj flipflop "toggle")])
- (read (togg (togg (togg (togg (proj flipflop "new")))))))))))
+ (pack (Counter (tup [new = (new)]
+ [read = (λ ([c : Counter]) (is-even? (get c)))]
+ [toggle = (λ ([c : Counter]) (inc c))]
+ [reset = (λ ([c : Counter]) (new))]))
+ as (∃ (FlipFlop) (× [new : FlipFlop]
+ [read : (→ FlipFlop Bool)]
+ [toggle : (→ FlipFlop FlipFlop)]
+ [reset : (→ FlipFlop FlipFlop)])))])
+ (let ([read (proj flipflop read)]
+ [togg (proj flipflop toggle)])
+ (read (togg (togg (togg (togg (proj flipflop new)))))))))))
: Bool ⇒ #f)
+;; err cases
+(typecheck-fail
+ (pack (Int 1) as Int)
+ #:with-msg
+ "Expected type of expression to match pattern \\(∃ \\(\\(X)) τ_body), got: Int")
+(typecheck-fail
+ (open ([(X x) <= 2]) 3)
+ #:with-msg
+ "Expected type of expression to match pattern \\(∃ \\(\\(X)) τ_body), got: Int")
+
;; previous tets from stlc+reco+var-tests.rkt ---------------------------------
;; define-type-alias
(define-type-alias Integer Int)
@@ -171,68 +181,68 @@
;; records (ie labeled tuples)
(check-type "Stephen" : String)
-(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× [: "name" String] [: "phone" Int] [: "male?" Bool]))
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+(check-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+ (× [name : String] [phone : Int] [male? : Bool]))
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
: String ⇒ "Stephen")
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
: String ⇒ "Stephen")
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) phone)
: Int ⇒ 781)
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) male?)
: Bool ⇒ #t)
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× [: "my-name" String] [: "phone" Int] [: "male?" Bool]))
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× [: "name" String] [: "my-phone" Int] [: "male?" Bool]))
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× [: "name" String] [: "phone" Int] [: "is-male?" Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+ (× [my-name : String] [phone : Int] [male? : Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+ (× [name : String] [my-phone : Int] [male? : Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+ (× [name : String] [phone : Int] [is-male? : Bool]))
;; variants
-(check-type (var "coffee" = (void) as (∨ [<> "coffee" Unit])) : (∨ [<> "coffee" Unit]))
-(check-not-type (var "coffee" = (void) as (∨ [<> "coffee" Unit])) : (∨ [<> "coffee" Unit] [<> "tea" Unit]))
-(typecheck-fail ((λ ([x : (∨ [<> "coffee" Unit] [<> "tea" Unit])]) x)
- (var "coffee" = (void) as (∨ [<> "coffee" Unit]))))
-(check-type (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit])) : (∨ [<> "coffee" Unit] [<> "tea" Unit]))
-(check-type (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit] [<> "coke" Unit]))
- : (∨ [<> "coffee" Unit] [<> "tea" Unit] [<> "coke" Unit]))
+(check-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit]))
+(check-not-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit] [tea : Unit]))
+(typecheck-fail ((λ ([x : (∨ [coffee : Unit] [tea : Unit])]) x)
+ (var coffee = (void) as (∨ [coffee : Unit]))))
+(check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) : (∨ [coffee : Unit] [tea : Unit]))
+(check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit] [coke : Unit]))
+ : (∨ [coffee : Unit] [tea : Unit] [coke : Unit]))
(typecheck-fail
- (case (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
- ["coffee" x => 1])) ; not enough clauses
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+ [coffee x => 1])) ; not enough clauses
(typecheck-fail
- (case (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
- ["coffee" x => 1]
- ["teaaaaaa" x => 2])) ; wrong clause
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+ [coffee x => 1]
+ [teaaaaaa x => 2])) ; wrong clause
(typecheck-fail
- (case (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
- ["coffee" x => 1]
- ["tea" x => 2]
- ["coke" x => 3])) ; too many clauses
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+ [coffee x => 1]
+ [tea x => 2]
+ [coke x => 3])) ; too many clauses
(typecheck-fail
- (case (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
- ["coffee" x => "1"]
- ["tea" x => 2])) ; mismatched branch types
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+ [coffee x => "1"]
+ [tea x => 2])) ; mismatched branch types
(check-type
- (case (var "coffee" = 1 as (∨ [<> "coffee" Int] [<> "tea" Unit]))
- ["coffee" x => x]
- ["tea" x => 2]) : Int ⇒ 1)
-(define-type-alias Drink (∨ [<> "coffee" Int] [<> "tea" Unit] [<> "coke" Bool]))
+ (case (var coffee = 1 as (∨ [coffee : Int] [tea : Unit]))
+ [coffee x => x]
+ [tea x => 2]) : Int ⇒ 1)
+(define-type-alias Drink (∨ [coffee : Int] [tea : Unit] [coke : Bool]))
(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
(check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int))
(check-type
(case ((λ ([d : Drink]) d)
- (var "coffee" = 1 as (∨ [<> "coffee" Int] [<> "tea" Unit] [<> "coke" Bool])))
- ["coffee" x => (+ (+ x x) (+ x x))]
- ["tea" x => 2]
- ["coke" y => 3])
+ (var coffee = 1 as (∨ [coffee : Int] [tea : Unit] [coke : Bool])))
+ [coffee x => (+ (+ x x) (+ x x))]
+ [tea x => 2]
+ [coke y => 3])
: Int ⇒ 4)
(check-type
- (case ((λ ([d : Drink]) d) (var "coffee" = 1 as Drink))
- ["coffee" x => (+ (+ x x) (+ x x))]
- ["tea" x => 2]
- ["coke" y => 3])
+ (case ((λ ([d : Drink]) d) (var coffee = 1 as Drink))
+ [coffee x => (+ (+ x x) (+ x x))]
+ [tea x => 2]
+ [coke y => 3])
: Int ⇒ 4)
;; previous tests: ------------------------------------------------------------
diff --git a/tapl/tests/ext-stlc-tests.rkt b/tapl/tests/ext-stlc-tests.rkt
@@ -29,7 +29,7 @@
(typecheck-fail (begin) #:with-msg "expected more terms")
(typecheck-fail
(begin 1 2 3)
- #:with-msg "all begin expressions except the last one should have type Unit")
+ #:with-msg "Expected expression 1 to have type Unit, got: Int")
(check-type (begin (void) 1) : Int ⇒ 1)
(check-type ((λ ([x : Int]) (begin (void) x)) 1) : Int)
@@ -42,6 +42,11 @@
(check-type (ann 1 : Int) : Int ⇒ 1)
(check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10)
(typecheck-fail (ann 1 : Bool) #:with-msg "ann: 1 does not have type Bool")
+;ann errs
+(typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
+(typecheck-fail (ann 1 : 1) #:with-msg "not a valid type")
+(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a valid type")
+(typecheck-fail (ann Int : Int) #:with-msg "does not have type Int")
; let
(check-type (let () (+ 1 1)) : Int ⇒ 2)
@@ -60,7 +65,6 @@
#:with-msg
"Arguments to function \\+.+have wrong type.+Given:.+Bool.+Int.+Expected:.+Int.+Int")
-
; letrec
(typecheck-fail
(letrec ([(x : Int) #f] [(y : Int) 1]) y)
@@ -95,12 +99,29 @@
(is-odd? 11)) : Bool ⇒ #t)
;; check some more err msgs
-(typecheck-fail (and "1" #f) #:with-msg "Expected type of.+to be Bool")
-(typecheck-fail (and #t "2") #:with-msg "Expected type of.+to be Bool")
-(typecheck-fail (or "1" #f) #:with-msg "Expected type of.+to be Bool")
-(typecheck-fail (or #t "2") #:with-msg "Expected type of.+to be Bool")
-(typecheck-fail (if "true" 1 2) #:with-msg "Expected type of.+to be Bool")
-
+(typecheck-fail
+ (and "1" #f)
+ #:with-msg "Expected expression \"1\" to have type Bool, got: String")
+(typecheck-fail
+ (and #t "2")
+ #:with-msg
+ "Expected expression \"2\" to have type Bool, got: String")
+(typecheck-fail
+ (or "1" #f)
+ #:with-msg
+ "Expected expression \"1\" to have type Bool, got: String")
+(typecheck-fail
+ (or #t "2")
+ #:with-msg
+ "Expected expression \"2\" to have type Bool, got: String")
+(typecheck-fail
+ (if "true" 1 2)
+ #:with-msg
+ "Expected expression \"true\" to have type Bool, got: String")
+(typecheck-fail
+ (if #t 1 "2")
+ #:with-msg
+ "branches must have the same type: given Int and String")
;; tests from stlc+lit-tests.rkt --------------------------
; most should pass, some failing may now pass due to added types/forms
@@ -122,7 +143,7 @@
(typecheck-fail
(λ ([f : Int]) (f 1 2))
#:with-msg
- "Expected type of expression to match pattern \\(→ τ_in ... τ_out\\), got: Int")
+ "Expected expression f to have → type, got: Int")
(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
: (→ (→ Int Int Int) Int Int Int))
diff --git a/tapl/tests/fomega-tests.rkt b/tapl/tests/fomega-tests.rkt
@@ -1,188 +1,191 @@
#lang s-exp "../fomega.rkt"
(require "rackunit-typechecking.rkt")
-(check-type Int : ★)
-(check-type String : ★)
-(typecheck-fail →)
-(check-type (→ Int Int) : ★)
-(typecheck-fail (→ →))
-(check-type 1 : Int)
-
-(check-type (∀ ([t : ★]) (→ t t)) : ★)
-(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
-
-(check-type ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : ★]) (λ ([x : X]) x)))
- : (∀ ([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")
-
-;;; sysf tests wont work, unless augmented with kinds
-(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
-
-(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) t)) : (∀ ([X : ★]) (→ X X X))) ; true
-(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([X : ★]) (→ X X X))) ; false
-(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([Y : ★]) (→ Y Y Y))) ; false, alpha equiv
-
-(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
- : (∀ ([t1 : ★]) (∀ ([t2 : ★]) (→ t1 (→ t2 t2)))))
-
-(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
- : (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4)))))
-
-(check-not-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
- : (∀ ([t4 : ★]) (∀ ([t3 : ★]) (→ t3 (→ t4 t4)))))
-
-(check-type (inst (Λ ([t : ★]) (λ ([x : t]) x)) Int) : (→ Int Int))
-(check-type (inst (Λ ([t : ★]) 1) (→ Int Int)) : Int)
-; first inst should be discarded
-(check-type (inst (inst (Λ ([t : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int))
-; second inst is discarded
-(check-type (inst (inst (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int))
-
-;; polymorphic arguments
-(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([t : ★]) (→ t t)))
-(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([s : ★]) (→ s s)))
-(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([s : ★]) (∀ ([t : ★]) (→ t t))))
-(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([t : ★]) (→ t t))))
-(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([s : ★]) (→ s s))))
-(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([u : ★]) (→ u u))))
-(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) x) : (→ (∀ ([s : ★]) (→ s s)) (∀ ([u : ★]) (→ u u))))
-(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x)))
-(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1))
-(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) : (∀ ([u : ★]) (→ u u)))
-(check-type
- (inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) : (→ Int Int))
-(check-type
- ((inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) 10)
- : Int ⇒ 10)
-(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) (inst x Int)) : (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)))
-(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10)) : (→ (∀ ([t : ★]) (→ t t)) Int))
-(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10))
- (Λ ([s : ★]) (λ ([y : s]) y)))
- : Int ⇒ 10)
-
-
-;; previous tests -------------------------------------------------------------
-(check-type 1 : Int)
-(check-not-type 1 : (→ Int Int))
-(typecheck-fail #f) ; unsupported literal
-(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)
-(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type
-(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type
-(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
-(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
- : (→ (→ Int Int Int) Int Int Int))
-(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
-(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
-(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
-(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
-(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
+;(check-type Int : ★)
+;(check-type String : ★)
+;(typecheck-fail →)
+;(check-type (→ Int Int) : ★)
+;(typecheck-fail (→ →))
+;(typecheck-fail (→ 1))
+;(check-type 1 : Int)
+;
+;(check-type (∀ ([t : ★]) (→ t t)) : ★)
+;(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
+
+(Λ ([X : ★]) (λ ([x : X]) x))
+
+#;(check-type ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : ★]) (λ ([x : X]) x)))
+ : (∀ ([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")
+;
+;;;; sysf tests wont work, unless augmented with kinds
+;(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+;
+;(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) t)) : (∀ ([X : ★]) (→ X X X))) ; true
+;(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([X : ★]) (→ X X X))) ; false
+;(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([Y : ★]) (→ Y Y Y))) ; false, alpha equiv
+;
+;(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+; : (∀ ([t1 : ★]) (∀ ([t2 : ★]) (→ t1 (→ t2 t2)))))
+;
+;(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+; : (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4)))))
+;
+;(check-not-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+; : (∀ ([t4 : ★]) (∀ ([t3 : ★]) (→ t3 (→ t4 t4)))))
+;
+;(check-type (inst (Λ ([t : ★]) (λ ([x : t]) x)) Int) : (→ Int Int))
+;(check-type (inst (Λ ([t : ★]) 1) (→ Int Int)) : Int)
+;; first inst should be discarded
+;(check-type (inst (inst (Λ ([t : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int))
+;; second inst is discarded
+;(check-type (inst (inst (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int))
+;
+;;; polymorphic arguments
+;(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([t : ★]) (→ t t)))
+;(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([s : ★]) (→ s s)))
+;(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([s : ★]) (∀ ([t : ★]) (→ t t))))
+;(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([t : ★]) (→ t t))))
+;(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([s : ★]) (→ s s))))
+;(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([u : ★]) (→ u u))))
+;(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) x) : (→ (∀ ([s : ★]) (→ s s)) (∀ ([u : ★]) (→ u u))))
+;(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x)))
+;(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1))
+;(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) : (∀ ([u : ★]) (→ u u)))
+;(check-type
+; (inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) : (→ Int Int))
+;(check-type
+; ((inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) 10)
+; : Int ⇒ 10)
+;(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) (inst x Int)) : (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)))
+;(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10)) : (→ (∀ ([t : ★]) (→ t t)) Int))
+;(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10))
+; (Λ ([s : ★]) (λ ([y : s]) y)))
+; : Int ⇒ 10)
+;
+;
+;;; previous tests -------------------------------------------------------------
+;(check-type 1 : Int)
+;(check-not-type 1 : (→ Int Int))
+;(typecheck-fail #f) ; unsupported literal
+;(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)
+;(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type
+;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type
+;(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
+;(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
+; : (→ (→ Int Int Int) Int Int Int))
+;(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
+;(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
+;(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
+;(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
+;(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
diff --git a/tapl/tests/rackunit-typechecking.rkt b/tapl/tests/rackunit-typechecking.rkt
@@ -3,7 +3,7 @@
(provide (all-defined-out))
(define-syntax (check-type stx)
- (syntax-parse stx #:datum-literals (:)
+ (syntax-parse stx #:datum-literals (: ⇒)
[(_ e : τ ⇒ v) #'(check-type-and-result e : τ ⇒ v)]
[(_ e : τ-expected:type)
#:with τ (typeof (expand/df #'e))
diff --git a/tapl/tests/run-all-tests.rkt b/tapl/tests/run-all-tests.rkt
@@ -11,16 +11,16 @@
(require "stlc+rec-iso-tests.rkt")
-;(require "exist-tests.rkt")
+(require "exist-tests.rkt")
;; subtyping
-;(require "stlc+sub-tests.rkt")
+(require "stlc+sub-tests.rkt")
;(require "stlc+reco+sub-tests.rkt")
-;(require "fsub-tests.rkt")
+;;(require "fsub-tests.rkt")
;
;;; system F
;(require "sysf-tests.rkt")
-;
+
;;; F_omega
;(require "fomega-tests.rkt")
;(require "fomega2-tests.rkt")
\ No newline at end of file
diff --git a/tapl/tests/stlc+box-tests.rkt b/tapl/tests/stlc+box-tests.rkt
@@ -13,8 +13,24 @@
(check-type ((λ ([b : (Ref Int)]) (deref b)) (ref 10)) : Int ⇒ 10)
(check-type ((λ ([b : (Ref Int)]) (begin (begin (:= b 20) (deref b)))) (ref 10)) : Int ⇒ 20)
-(typecheck-fail (λ ([lst : (Ref Int Int)]) lst)) ; type constructor wrong arity
-(typecheck-fail (λ ([lst : (Ref)]) lst)) ; type constructor wrong arity
+;; Ref err msgs
+; wrong arity
+(typecheck-fail
+ (λ ([lst : (Ref Int Int)]) lst)
+ #:with-msg
+ "Improper usage of type constructor Ref: \\(Ref Int Int), expected pattern \\(Ref τ)")
+(typecheck-fail
+ (λ ([lst : (Ref)]) lst)
+ #:with-msg
+ "Improper usage of type constructor Ref: \\(Ref), expected pattern \\(Ref τ)")
+(typecheck-fail
+ (deref 1)
+ #:with-msg
+ "Expected type of expression.+to match pattern \\(Ref τ), got: Int")
+(typecheck-fail
+ (:= 1 1)
+ #:with-msg
+ "Expected type of expression.+to match pattern \\(Ref τ), got: Int")
;; previous tests: ------------------------------------------------------------
(typecheck-fail (cons 1 2))
@@ -49,69 +65,69 @@
(check-type (λ ([f : ArithBinOp]) (f 1 2)) : (→ (→ Int Int Int) Int))
(check-type "Stephen" : String)
-(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× [: "name" String] [: "phone" Int] [: "male?" Bool]))
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+(check-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+ (× [name : String] [phone : Int] [male? : Bool]))
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
: String ⇒ "Stephen")
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
: String ⇒ "Stephen")
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) phone)
: Int ⇒ 781)
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) male?)
: Bool ⇒ #t)
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× [: "my-name" String] [: "phone" Int] [: "male?" Bool]))
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× [: "name" String] [: "my-phone" Int] [: "male?" Bool]))
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× [: "name" String] [: "phone" Int] [: "is-male?" Bool]))
-
-
-(check-type (var "coffee" = (void) as (∨ [<> "coffee" Unit])) : (∨ [<> "coffee" Unit]))
-(check-not-type (var "coffee" = (void) as (∨ [<> "coffee" Unit])) : (∨ [<> "coffee" Unit] [<> "tea" Unit]))
-(typecheck-fail ((λ ([x : (∨ [<> "coffee" Unit] [<> "tea" Unit])]) x)
- (var "coffee" = (void) as (∨ [<> "coffee" Unit]))))
-(check-type (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
- : (∨ [<> "coffee" Unit] [<> "tea" Unit]))
-(check-type (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit] [<> "coke" Unit]))
- : (∨ [<> "coffee" Unit] [<> "tea" Unit] [<> "coke" Unit]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+ (× [my-name : String] [phone : Int] [male? : Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+ (× [name : String] [my-phone : Int] [male? : Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+ (× [name : String] [phone : Int] [is-male? : Bool]))
+
+
+(check-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit]))
+(check-not-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit] [tea : Unit]))
+(typecheck-fail ((λ ([x : (∨ [coffee : Unit] [tea : Unit])]) x)
+ (var coffee = (void) as (∨ [coffee : Unit]))))
+(check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+ : (∨ [coffee : Unit] [tea : Unit]))
+(check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit] [coke : Unit]))
+ : (∨ [coffee : Unit] [tea : Unit] [coke : Unit]))
(typecheck-fail
- (case (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
- ["coffee" x => 1])) ; not enough clauses
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+ [coffee x => 1])) ; not enough clauses
(typecheck-fail
- (case (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
- ["coffee" x => 1]
- ["teaaaaaa" x => 2])) ; wrong clause
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+ [coffee x => 1]
+ [teaaaaaa x => 2])) ; wrong clause
(typecheck-fail
- (case (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
- ["coffee" x => 1]
- ["tea" x => 2]
- ["coke" x => 3])) ; too many clauses
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+ [coffee x => 1]
+ [tea x => 2]
+ [coke x => 3])) ; too many clauses
(typecheck-fail
- (case (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
- ["coffee" x => "1"]
- ["tea" x => 2])) ; mismatched branch types
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+ [coffee x => "1"]
+ [tea x => 2])) ; mismatched branch types
(check-type
- (case (var "coffee" = 1 as (∨ [<> "coffee" Int] [<> "tea" Unit]))
- ["coffee" x => x]
- ["tea" x => 2]) : Int ⇒ 1)
-(define-type-alias Drink (∨ [<> "coffee" Int] [<> "tea" Unit] [<> "coke" Bool]))
+ (case (var coffee = 1 as (∨ [coffee : Int] [tea : Unit]))
+ [coffee x => x]
+ [tea x => 2]) : Int ⇒ 1)
+(define-type-alias Drink (∨ [coffee : Int] [tea : Unit] [coke : Bool]))
(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
(check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int))
(check-type
(case ((λ ([d : Drink]) d)
- (var "coffee" = 1 as (∨ [<> "coffee" Int] [<> "tea" Unit] [<> "coke" Bool])))
- ["coffee" x => (+ (+ x x) (+ x x))]
- ["tea" x => 2]
- ["coke" y => 3])
+ (var coffee = 1 as (∨ [coffee : Int] [tea : Unit] [coke : Bool])))
+ [coffee x => (+ (+ x x) (+ x x))]
+ [tea x => 2]
+ [coke y => 3])
: Int ⇒ 4)
(check-type
- (case ((λ ([d : Drink]) d) (var "coffee" = 1 as Drink))
- ["coffee" x => (+ (+ x x) (+ x x))]
- ["tea" x => 2]
- ["coke" y => 3])
+ (case ((λ ([d : Drink]) d) (var coffee = 1 as Drink))
+ [coffee x => (+ (+ x x) (+ x x))]
+ [tea x => 2]
+ [coke y => 3])
: Int ⇒ 4)
;; previous tests: ------------------------------------------------------------
diff --git a/tapl/tests/stlc+cons-tests.rkt b/tapl/tests/stlc+cons-tests.rkt
@@ -34,6 +34,12 @@
(check-type ((head fn-lst) 25) : Int ⇒ 35)
(check-type (tail fn-lst) : (List (→ Int Int)) ⇒ (nil {(→ Int Int)}))
+; more list errors
+(typecheck-fail
+ (cons 1 1)
+ #:with-msg
+ "Expected type of expression to match pattern \\(List τ), got: Int")
+
;; previous tests: ------------------------------------------------------------
;; define-type-alias
(define-type-alias Integer Int)
@@ -47,69 +53,69 @@
;; records (ie labeled tuples)
(check-type "Stephen" : String)
-(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× [: "name" String] [: "phone" Int] [: "male?" Bool]))
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+(check-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+ (× [name : String] [phone : Int] [male? : Bool]))
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
: String ⇒ "Stephen")
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
: String ⇒ "Stephen")
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) phone)
: Int ⇒ 781)
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) male?)
: Bool ⇒ #t)
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× [: "my-name" String] [: "phone" Int] [: "male?" Bool]))
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× [: "name" String] [: "my-phone" Int] [: "male?" Bool]))
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× [: "name" String] [: "phone" Int] [: "is-male?" Bool]))
-
-
-(check-type (var "coffee" = (void) as (∨ [<> "coffee" Unit])) : (∨ [<> "coffee" Unit]))
-(check-not-type (var "coffee" = (void) as (∨ [<> "coffee" Unit])) : (∨ [<> "coffee" Unit] [<> "tea" Unit]))
-(typecheck-fail ((λ ([x : (∨ [<> "coffee" Unit] [<> "tea" Unit])]) x)
- (var "coffee" = (void) as (∨ [<> "coffee" Unit]))))
-(check-type (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
- : (∨ [<> "coffee" Unit] [<> "tea" Unit]))
-(check-type (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit] [<> "coke" Unit]))
- : (∨ [<> "coffee" Unit] [<> "tea" Unit] [<> "coke" Unit]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+ (× [my-name : String] [phone : Int] [male? : Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+ (× [name : String] [my-phone : Int] [male? : Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+ (× [name : String] [phone : Int] [is-male? : Bool]))
+
+
+(check-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit]))
+(check-not-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit] [tea : Unit]))
+(typecheck-fail ((λ ([x : (∨ [coffee : Unit] [tea : Unit])]) x)
+ (var coffee = (void) as (∨ [coffee : Unit]))))
+(check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+ : (∨ [coffee : Unit] [tea : Unit]))
+(check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit] [coke : Unit]))
+ : (∨ [coffee : Unit] [tea : Unit] [coke : Unit]))
(typecheck-fail
- (case (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
- ["coffee" x => 1])) ; not enough clauses
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+ [coffee x => 1])) ; not enough clauses
(typecheck-fail
- (case (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
- ["coffee" x => 1]
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+ [coffee x => 1]
["teaaaaaa" x => 2])) ; wrong clause
(typecheck-fail
- (case (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
- ["coffee" x => 1]
- ["tea" x => 2]
- ["coke" x => 3])) ; too many clauses
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+ [coffee x => 1]
+ [tea x => 2]
+ [coke x => 3])) ; too many clauses
(typecheck-fail
- (case (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
- ["coffee" x => "1"]
- ["tea" x => 2])) ; mismatched branch types
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+ [coffee x => "1"]
+ [tea x => 2])) ; mismatched branch types
(check-type
- (case (var "coffee" = 1 as (∨ [<> "coffee" Int] [<> "tea" Unit]))
- ["coffee" x => x]
- ["tea" x => 2]) : Int ⇒ 1)
-(define-type-alias Drink (∨ [<> "coffee" Int] [<> "tea" Unit] [<> "coke" Bool]))
+ (case (var coffee = 1 as (∨ [coffee : Int] [tea : Unit]))
+ [coffee x => x]
+ [tea x => 2]) : Int ⇒ 1)
+(define-type-alias Drink (∨ [coffee : Int] [tea : Unit] [coke : Bool]))
(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
(check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int))
(check-type
(case ((λ ([d : Drink]) d)
- (var "coffee" = 1 as (∨ [<> "coffee" Int] [<> "tea" Unit] [<> "coke" Bool])))
- ["coffee" x => (+ (+ x x) (+ x x))]
- ["tea" x => 2]
- ["coke" y => 3])
+ (var coffee = 1 as (∨ [coffee : Int] [tea : Unit] [coke : Bool])))
+ [coffee x => (+ (+ x x) (+ x x))]
+ [tea x => 2]
+ [coke y => 3])
: Int ⇒ 4)
(check-type
- (case ((λ ([d : Drink]) d) (var "coffee" = 1 as Drink))
- ["coffee" x => (+ (+ x x) (+ x x))]
- ["tea" x => 2]
- ["coke" y => 3])
+ (case ((λ ([d : Drink]) d) (var coffee = 1 as Drink))
+ [coffee x => (+ (+ x x) (+ x x))]
+ [tea x => 2]
+ [coke y => 3])
: Int ⇒ 4)
;; previous tests: ------------------------------------------------------------
diff --git a/tapl/tests/stlc+lit-tests.rkt b/tapl/tests/stlc+lit-tests.rkt
@@ -13,27 +13,27 @@
(typecheck-fail
(λ ([x : →]) x)
- #:with-msg "Improper usage of type constructor →: →, expected pattern")
+ #:with-msg "Improper usage of type constructor →: →, expected >= 1 arguments")
(typecheck-fail
(λ ([x : (→ →)]) x)
- #:with-msg "Improper usage of type constructor →: →, expected pattern")
+ #:with-msg "Improper usage of type constructor →: →, expected >= 1 arguments")
(typecheck-fail
(λ ([x : (→)]) x)
- #:with-msg "Improper usage of type constructor →: \\(→\\), expected pattern")
+ #:with-msg "Improper usage of type constructor →: \\(→), expected >= 1 arguments")
(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
(typecheck-fail ((λ ([x : Bool]) x) 1)
- #:with-msg "not a valid type: Bool")
+ #:with-msg "Bool: unbound identifier")
(typecheck-fail (λ ([x : (→ Bool Bool)]) x)
- #:with-msg "not a valid type: Bool")
+ #:with-msg "Bool: unbound identifier")
(typecheck-fail (λ ([x : Bool]) x)
- #:with-msg "not a valid type: Bool")
+ #:with-msg "Bool: unbound identifier")
(typecheck-fail
(λ ([f : Int]) (f 1 2))
#:with-msg
- "Expected type of expression to match pattern \\(→ τ_in ... τ_out\\), got: Int")
+ "Expected expression f to have → type, got: Int")
(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
: (→ (→ Int Int Int) Int Int Int))
diff --git a/tapl/tests/stlc+rec-iso-tests.rkt b/tapl/tests/stlc+rec-iso-tests.rkt
@@ -1,15 +1,15 @@
#lang s-exp "../stlc+rec-iso.rkt"
(require "rackunit-typechecking.rkt")
-(define-type-alias IntList (μ [[X]] (∨ [<> "nil" Unit] [<> "cons" (× Int X)])))
-(define-type-alias ILBody (∨ [<> "nil" Unit] [<> "cons" (× Int IntList)]))
+(define-type-alias IntList (μ (X) (∨ [nil : Unit] [cons : (× Int X)])))
+(define-type-alias ILBody (∨ [nil : Unit] [cons : (× Int IntList)]))
;; nil
-(define nil (fld {IntList} (var "nil" = (void) as ILBody)))
+(define nil (fld {IntList} (var nil = (void) as ILBody)))
(check-type nil : IntList)
;; cons
-(define cons (λ ([n : Int] [lst : IntList]) (fld {IntList} (var "cons" = (tup n lst) as ILBody))))
+(define cons (λ ([n : Int] [lst : IntList]) (fld {IntList} (var cons = (tup n lst) as ILBody))))
(check-type cons : (→ Int IntList IntList))
(check-type (cons 1 nil) : IntList)
(typecheck-fail (cons 1 2))
@@ -19,8 +19,8 @@
(define isnil
(λ ([lst : IntList])
(case (unfld {IntList} lst)
- ["nil" n => #t]
- ["cons" p => #f])))
+ [nil n => #t]
+ [cons p => #f])))
(check-type isnil : (→ IntList Bool))
(check-type (isnil nil) : Bool ⇒ #t)
(check-type (isnil (cons 1 nil)) : Bool ⇒ #f)
@@ -33,8 +33,8 @@
(define hd
(λ ([lst : IntList])
(case (unfld {IntList} lst)
- ["nil" n => 0]
- ["cons" p => (proj p 0)])))
+ [nil n => 0]
+ [cons p => (proj p 0)])))
(check-type hd : (→ IntList Int))
(check-type (hd nil) : Int ⇒ 0)
(typecheck-fail (hd 1))
@@ -44,14 +44,24 @@
(define tl
(λ ([lst : IntList])
(case (unfld {IntList} lst)
- ["nil" n => lst]
- ["cons" p => (proj p 1)])))
+ [nil n => lst]
+ [cons p => (proj p 1)])))
(check-type tl : (→ IntList IntList))
(check-type (tl nil) : IntList ⇒ nil)
(check-type (tl (cons 1 nil)) : IntList ⇒ nil)
(check-type (tl (cons 1 (cons 2 nil))) : IntList ⇒ (cons 2 nil))
(typecheck-fail (tl 1))
+;; some typecheck failure msgs
+(typecheck-fail
+ (fld {Int} 1)
+ #:with-msg
+ "Expected type of expression to match pattern \\(μ \\(\\(tv)) τ_body), got: Int")
+(typecheck-fail
+ (unfld {Int} 1)
+ #:with-msg
+ "Expected type of expression to match pattern \\(μ \\(\\(tv)) τ_body), got: Int")
+
;; previous stlc+var tests ----------------------------------------------------
;; define-type-alias
(define-type-alias Integer Int)
@@ -85,50 +95,50 @@
; (× [: "name" String] [: "phone" Int] [: "is-male?" Bool]))
;; variants
-(check-type (var "coffee" = (void) as (∨ [<> "coffee" Unit])) : (∨ [<> "coffee" Unit]))
-(check-not-type (var "coffee" = (void) as (∨ [<> "coffee" Unit])) : (∨ [<> "coffee" Unit] [<> "tea" Unit]))
-(typecheck-fail ((λ ([x : (∨ [<> "coffee" Unit] [<> "tea" Unit])]) x)
- (var "coffee" = (void) as (∨ [<> "coffee" Unit]))))
-(check-type (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit])) : (∨ [<> "coffee" Unit] [<> "tea" Unit]))
-(check-type (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit] [<> "coke" Unit]))
- : (∨ [<> "coffee" Unit] [<> "tea" Unit] [<> "coke" Unit]))
+(check-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit]))
+(check-not-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit] [tea : Unit]))
+(typecheck-fail ((λ ([x : (∨ [coffee : Unit] [tea : Unit])]) x)
+ (var coffee = (void) as (∨ [coffee : Unit]))))
+(check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) : (∨ [coffee : Unit] [tea : Unit]))
+(check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit] [coke : Unit]))
+ : (∨ [coffee : Unit] [tea : Unit] [coke : Unit]))
(typecheck-fail
- (case (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
- ["coffee" x => 1])) ; not enough clauses
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+ [coffee x => 1])) ; not enough clauses
(typecheck-fail
- (case (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
- ["coffee" x => 1]
- ["teaaaaaa" x => 2])) ; wrong clause
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+ [coffee x => 1]
+ [teaaaaaa x => 2])) ; wrong clause
(typecheck-fail
- (case (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
- ["coffee" x => 1]
- ["tea" x => 2]
- ["coke" x => 3])) ; too many clauses
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+ [coffee x => 1]
+ [tea x => 2]
+ [coke x => 3])) ; too many clauses
(typecheck-fail
- (case (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
- ["coffee" x => "1"]
- ["tea" x => 2])) ; mismatched branch types
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+ [coffee x => "1"]
+ [tea x => 2])) ; mismatched branch types
(check-type
- (case (var "coffee" = 1 as (∨ [<> "coffee" Int] [<> "tea" Unit]))
- ["coffee" x => x]
- ["tea" x => 2]) : Int ⇒ 1)
-(define-type-alias Drink (∨ [<> "coffee" Int] [<> "tea" Unit] [<> "coke" Bool]))
+ (case (var coffee = 1 as (∨ [coffee : Int] [tea : Unit]))
+ [coffee x => x]
+ [tea x => 2]) : Int ⇒ 1)
+(define-type-alias Drink (∨ [coffee : Int] [tea : Unit] [coke : Bool]))
(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
(check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int))
(check-type
(case ((λ ([d : Drink]) d)
- (var "coffee" = 1 as (∨ [<> "coffee" Int] [<> "tea" Unit] [<> "coke" Bool])))
- ["coffee" x => (+ (+ x x) (+ x x))]
- ["tea" x => 2]
- ["coke" y => 3])
+ (var coffee = 1 as (∨ [coffee : Int] [tea : Unit] [coke : Bool])))
+ [coffee x => (+ (+ x x) (+ x x))]
+ [tea x => 2]
+ [coke y => 3])
: Int ⇒ 4)
(check-type
- (case ((λ ([d : Drink]) d) (var "coffee" = 1 as Drink))
- ["coffee" x => (+ (+ x x) (+ x x))]
- ["tea" x => 2]
- ["coke" y => 3])
+ (case ((λ ([d : Drink]) d) (var coffee = 1 as Drink))
+ [coffee x => (+ (+ x x) (+ x x))]
+ [tea x => 2]
+ [coke y => 3])
: Int ⇒ 4)
;; previous tests: ------------------------------------------------------------
diff --git a/tapl/tests/stlc+reco+sub-tests.rkt b/tapl/tests/stlc+reco+sub-tests.rkt
@@ -4,10 +4,10 @@
;; record subtyping tests
(check-type "coffee" : String)
(check-type (tup ["coffee" = 3]) : (× [: "coffee" Int])) ; element subtyping
-(check-type (var "coffee" = 3 as (∨ [: "coffee" Nat])) : (∨ [: "coffee" Int])) ; element subtyping
+(check-type (var "coffee" = 3 as (∨ [<> "coffee" Nat])) : (∨ [<> "coffee" Int])) ; element subtyping
(check-type (tup ["coffee" = 3]) : (× [: "coffee" Nat]))
(check-type (tup ["coffee" = 3]) : (× [: "coffee" Top]))
-(check-type (var "coffee" = 3 as (∨ [: "coffee" Int])) : (∨ [: "coffee" Top])) ; element subtyping (twice)
+(check-type (var "coffee" = 3 as (∨ [<> "coffee" Int])) : (∨ [<> "coffee" Top])) ; element subtyping (twice)
(check-type (tup ["coffee" = 3]) : (× [: "coffee" Num]))
(check-not-type (tup ["coffee" = -3]) : (× [: "coffee" Nat]))
(check-type (tup ["coffee" = -3]) : (× [: "coffee" Num]))
diff --git a/tapl/tests/stlc+reco+var-tests.rkt b/tapl/tests/stlc+reco+var-tests.rkt
@@ -15,78 +15,119 @@
; records (ie labeled tuples)
(check-type "Stephen" : String)
(check-type (tup) : (×))
-(check-type (tup ["name" = "Stephen"]) : (× [: "name" String]))
-(check-type (proj (tup ["name" = "Stephen"]) "name") : String ⇒ "Stephen")
-(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× [: "name" String] [: "phone" Int] [: "male?" Bool]))
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+(check-type (tup [name = "Stephen"]) : (× [name : String]))
+(check-type (proj (tup [name = "Stephen"]) name) : String ⇒ "Stephen")
+(check-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+ (× [name : String] [phone : Int] [male? : Bool]))
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
: String ⇒ "Stephen")
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
: String ⇒ "Stephen")
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) phone)
: Int ⇒ 781)
-(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?")
+(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) male?)
: Bool ⇒ #t)
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× [: "my-name" String] [: "phone" Int] [: "male?" Bool]))
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× [: "name" String] [: "my-phone" Int] [: "male?" Bool]))
-(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× [: "name" String] [: "phone" Int] [: "is-male?" Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+ (× [my-name : String] [phone : Int] [male? : Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+ (× [name : String] [my-phone : Int] [male? : Bool]))
+(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
+ (× [name : String] [phone : Int] [is-male? : Bool]))
+
+;; record errors
+(typecheck-fail
+ (proj 1 "a")
+ #:with-msg
+ "expected identifier")
+(typecheck-fail
+ (proj 1 a)
+ #:with-msg
+ "Expected expression 1 to have × type, got: Int")
;; variants
-(check-type (var "coffee" = (void) as (∨ [<> "coffee" Unit])) : (∨ [<> "coffee" Unit]))
-(check-not-type (var "coffee" = (void) as (∨ [<> "coffee" Unit])) : (∨ [<> "coffee" Unit] [<> "tea" Unit]))
-(typecheck-fail ((λ ([x : (∨ [<> "coffee" Unit] [<> "tea" Unit])]) x)
- (var "coffee" = (void) as (∨ [<> "coffee" Unit])))
+(check-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit]))
+(check-not-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit] [tea : Unit]))
+(typecheck-fail ((λ ([x : (∨ [coffee : Unit] [tea : Unit])]) x)
+ (var coffee = (void) as (∨ [coffee : Unit])))
#:with-msg "Arguments to function.+have wrong type")
-(check-type (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit])) :
- (∨ [<> "coffee" Unit] [<> "tea" Unit]))
-(check-type (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit] [<> "coke" Unit]))
- : (∨ [<> "coffee" Unit] [<> "tea" Unit] [<> "coke" Unit]))
+(check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) :
+ (∨ [coffee : Unit] [tea : Unit]))
+(check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit] [coke : Unit]))
+ : (∨ [coffee : Unit] [tea : Unit] [coke : Unit]))
(typecheck-fail
- (case (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
- ["coffee" x => 1])
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+ [coffee x => 1])
#:with-msg "wrong number of case clauses")
(typecheck-fail
- (case (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
- ["coffee" x => 1]
- ["teaaaaaa" x => 2])
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+ [coffee x => 1]
+ [teaaaaaa x => 2])
#:with-msg "case clauses not exhaustive")
(typecheck-fail
- (case (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
- ["coffee" x => 1]
- ["tea" x => 2]
- ["coke" x => 3])
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+ [coffee x => 1]
+ [tea x => 2]
+ [coke x => 3])
#:with-msg "wrong number of case clauses")
(typecheck-fail
- (case (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit]))
- ["coffee" x => "1"]
- ["tea" x => 2])
+ (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
+ [coffee x => "1"]
+ [tea x => 2])
#:with-msg "branches have different types")
(check-type
- (case (var "coffee" = 1 as (∨ [<> "coffee" Int] [<> "tea" Unit]))
- ["coffee" x => x]
- ["tea" x => 2]) : Int ⇒ 1)
-(define-type-alias Drink (∨ [<> "coffee" Int] [<> "tea" Unit] [<> "coke" Bool]))
+ (case (var coffee = 1 as (∨ [coffee : Int] [tea : Unit]))
+ [coffee x => x]
+ [tea x => 2]) : Int ⇒ 1)
+(define-type-alias Drink (∨ [coffee : Int] [tea : Unit] [coke : Bool]))
(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
(check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int))
(check-type
(case ((λ ([d : Drink]) d)
- (var "coffee" = 1 as (∨ [<> "coffee" Int] [<> "tea" Unit] [<> "coke" Bool])))
- ["coffee" x => (+ (+ x x) (+ x x))]
- ["tea" x => 2]
- ["coke" y => 3])
+ (var coffee = 1 as (∨ [coffee : Int] [tea : Unit] [coke : Bool])))
+ [coffee x => (+ (+ x x) (+ x x))]
+ [tea x => 2]
+ [coke y => 3])
: Int ⇒ 4)
(check-type
- (case ((λ ([d : Drink]) d) (var "coffee" = 1 as Drink))
- ["coffee" x => (+ (+ x x) (+ x x))]
- ["tea" x => 2]
- ["coke" y => 3])
+ (case ((λ ([d : Drink]) d) (var coffee = 1 as Drink))
+ [coffee x => (+ (+ x x) (+ x x))]
+ [tea x => 2]
+ [coke y => 3])
: Int ⇒ 4)
+;; variant errors
+(typecheck-fail
+ (var name = "Steve" as Int)
+ #:with-msg
+ "Expected ∨ type, got: Int")
+(typecheck-fail
+ (case 1 [racket x => 1])
+ #:with-msg
+ "Expected expression 1 to have ∨ type, got: Int")
+(typecheck-fail
+ (λ ([x : (∨)]) x)
+ #:with-msg "Improper usage of type constructor ∨: \\(∨), expected \\(∨ [label:id : τ:type] ...+)")
+(typecheck-fail
+ (λ ([x : (∨ 1)]) x)
+ #:with-msg "Improper usage of type constructor ∨: \\(∨ 1\\), expected \\(∨ [label:id : τ:type] ...+)")
+(typecheck-fail
+ (λ ([x : (∨ [1 2])]) x)
+ #:with-msg "Improper usage of type constructor ∨: \\(∨ (1 2)), expected \\(∨ [label:id : τ:type] ...+)")
+(typecheck-fail
+ (λ ([x : (∨ [a 2])]) x)
+ #:with-msg "Improper usage of type constructor ∨: \\(∨ (a 2)), expected \\(∨ [label:id : τ:type] ...+)")
+(typecheck-fail
+ (λ ([x : (∨ [a Int])]) x)
+ #:with-msg "Improper usage of type constructor ∨: \\(∨ (a Int)), expected \\(∨ [label:id : τ:type] ...+)")
+(typecheck-fail
+ (λ ([x : (∨ [1 : Int])]) x)
+ #:with-msg "Improper usage of type constructor ∨: \\(∨ (1 : Int)), expected \\(∨ [label:id : τ:type] ...+)")
+(typecheck-fail
+ (λ ([x : (∨ [a : 1])]) x)
+ #:with-msg "Improper usage of type constructor ∨: \\(∨ (a : 1)), expected \\(∨ [label:id : τ:type] ...+)")
+
;; previous tuple tests: ------------------------------------------------------------
;; wont work anymore
;;(check-type (tup 1 2 3) : (× Int Int Int))
diff --git a/tapl/tests/stlc+tup-tests.rkt b/tapl/tests/stlc+tup-tests.rkt
@@ -17,7 +17,7 @@
(typecheck-fail
(proj 1 2)
#:with-msg
- "Expected type of expression 1 to match pattern \\(× τ ...\\), got: Int")
+ "Expected expression 1 to have × type, got: Int")
;; ext-stlc.rkt tests ---------------------------------------------------------
;; should still pass
diff --git a/tapl/tests/sysf-tests.rkt b/tapl/tests/sysf-tests.rkt
@@ -1,20 +1,20 @@
#lang s-exp "../sysf.rkt"
(require "rackunit-typechecking.rkt")
-(check-type (Λ (X) (λ ([x : X]) x)) : (∀ (X) (→ X X)))
+(check-type (Λ (X) (λ ([x : X]) x)) : (∀ [[X]] (→ X X)))
-(check-type (Λ (X) (λ ([t : X] [f : X]) t)) : (∀ (X) (→ X X X))) ; true
-(check-type (Λ (X) (λ ([t : X] [f : X]) f)) : (∀ (X) (→ X X X))) ; false
-(check-type (Λ (X) (λ ([t : X] [f : X]) f)) : (∀ (Y) (→ Y Y Y))) ; false, alpha equiv
+(check-type (Λ (X) (λ ([t : X] [f : X]) t)) : (∀ [[X]] (→ X X X))) ; true
+(check-type (Λ (X) (λ ([t : X] [f : X]) f)) : (∀ [[X]] (→ X X X))) ; false
+(check-type (Λ (X) (λ ([t : X] [f : X]) f)) : (∀ [[Y]] (→ Y Y Y))) ; false, alpha equiv
(check-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y))))
- : (∀ (t1) (∀ (t2) (→ t1 (→ t2 t2)))))
+ : (∀ [[t1]] (∀ [[t2]] (→ t1 (→ t2 t2)))))
(check-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y))))
- : (∀ (t3) (∀ (t4) (→ t3 (→ t4 t4)))))
+ : (∀ [[t3]] (∀ [[t4]] (→ t3 (→ t4 t4)))))
(check-not-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y))))
- : (∀ (t4) (∀ (t3) (→ t3 (→ t4 t4)))))
+ : (∀ [[t4]] (∀ [[t3]] (→ t3 (→ t4 t4)))))
(check-type (inst (Λ (t) (λ ([x : t]) x)) Int) : (→ Int Int))
(check-type (inst (Λ (t) 1) (→ Int Int)) : Int)
@@ -23,30 +23,36 @@
; second inst is discarded
(check-type (inst (inst (Λ (t1) (Λ (t2) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int))
-;;; polymorphic arguments
-(check-type (Λ (t) (λ ([x : t]) x)) : (∀ (t) (→ t t)))
-(check-type (Λ (t) (λ ([x : t]) x)) : (∀ (s) (→ s s)))
-(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ (s) (∀ (t) (→ t t))))
-(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ (r) (∀ (t) (→ t t))))
-(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ (r) (∀ (s) (→ s s))))
-(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ (r) (∀ (u) (→ u u))))
-(check-type (λ ([x : (∀ (t) (→ t t))]) x) : (→ (∀ (s) (→ s s)) (∀ (u) (→ u u))))
-(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x)))
-(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1))
-(check-type ((λ ([x : (∀ (t) (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) : (∀ (u) (→ u u)))
+;; inst err
+(typecheck-fail
+ (inst 1 Int)
+ #:with-msg
+ "Expected type of expression to match pattern \\(∀ \\(\\(x ...)) body), got: Int")
+
+;; polymorphic arguments
+(check-type (Λ (t) (λ ([x : t]) x)) : (∀ [[t]] (→ t t)))
+(check-type (Λ (t) (λ ([x : t]) x)) : (∀ [[s]] (→ s s)))
+(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ [[s]] (∀ [[t]] (→ t t))))
+(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ [[r]] (∀ [[t]] (→ t t))))
+(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ [[r]] (∀ [[s]] (→ s s))))
+(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ [[r]] (∀ [[u]] (→ u u))))
+(check-type (λ ([x : (∀ [[t]] (→ t t))]) x) : (→ (∀ [[s]] (→ s s)) (∀ [[u]] (→ u u))))
+(typecheck-fail ((λ ([x : (∀ [[t]] (→ t t))]) x) (λ ([x : Int]) x)))
+(typecheck-fail ((λ ([x : (∀ [[t]] (→ t t))]) x) 1))
+(check-type ((λ ([x : (∀ [[t]] (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) : (∀ [[u]] (→ u u)))
(check-type
- (inst ((λ ([x : (∀ (t) (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) Int) : (→ Int Int))
+ (inst ((λ ([x : (∀ [[t]] (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) Int) : (→ Int Int))
(check-type
- ((inst ((λ ([x : (∀ (t) (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) Int) 10)
+ ((inst ((λ ([x : (∀ [[t]] (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) Int) 10)
: Int ⇒ 10)
-(check-type (λ ([x : (∀ (t) (→ t t))]) (inst x Int)) : (→ (∀ (t) (→ t t)) (→ Int Int)))
-(check-type (λ ([x : (∀ (t) (→ t t))]) ((inst x Int) 10)) : (→ (∀ (t) (→ t t)) Int))
-(check-type ((λ ([x : (∀ (t) (→ t t))]) ((inst x Int) 10))
+(check-type (λ ([x : (∀ [[t]] (→ t t))]) (inst x Int)) : (→ (∀ [[t]] (→ t t)) (→ Int Int)))
+(check-type (λ ([x : (∀ [[t]] (→ t t))]) ((inst x Int) 10)) : (→ (∀ [[t]] (→ t t)) Int))
+(check-type ((λ ([x : (∀ [[t]] (→ t t))]) ((inst x Int) 10))
(Λ (s) (λ ([y : s]) y)))
: Int ⇒ 10)
-;;; previous tests -------------------------------------------------------------
+;; previous tests -------------------------------------------------------------
(check-type 1 : Int)
(check-not-type 1 : (→ Int Int))
(typecheck-fail "one") ; unsupported literal
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -10,7 +10,8 @@
(provide
(for-syntax (all-defined-out)) (all-defined-out)
(for-syntax
- (all-from-out racket syntax/parse racket/syntax syntax/stx "stx-utils.rkt")))
+ (all-from-out racket syntax/parse racket/syntax syntax/stx "stx-utils.rkt"))
+ (for-meta 2 (all-from-out racket/base syntax/parse)))
;; type checking functions/forms
@@ -54,59 +55,141 @@
(regexp-replace pre-pat name ""))))
(all-from-out base-lang))))]))
-;; when combining #%type's with #%plain-type's, eg when inferring type for λ
-;; (call this mixed type) we create a type that still needs expansion, ie eval
-;; With the #%type and #%plain-type distinction, mixed types can be evaled
-;; and the #%plain-type will wrappers will simply go away
-(define-syntax #%type (syntax-parser [(_ τ) #'τ])) ; surface stx
-(define-syntax #%plain-type (syntax-parser [(_ τ) #'τ])) ; expanded representation
-
-(define-syntax (define-base-type stx)
- (syntax-parse stx
- [(_ τ:id)
- #:with τ? (format-id #'τ "~a?" #'τ)
- #:with τ-internal (generate-temporary #'τ)
- #:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
- #:with τ-cls (generate-temporary #'τ)
- #'(begin
- (provide τ (for-syntax τ? inferτ+erase))
- (define τ-internal
- (λ () (raise (exn:fail:type:runtime
- (format "~a: Cannot use type at run time" 'τ)
- (current-continuation-marks)))))
- (define-syntax (τ stx)
- (syntax-parse stx
- [x:id (add-orig #'(#%type (τ-internal)) #'τ)]))
- (begin-for-syntax
- ; expanded form of τ
- (define-syntax-class τ-cls
- (pattern ((~literal #%plain-type) ((~literal #%plain-app) ty))))
- (define (τ? t)
- (syntax-parse ((current-type-eval) t)
- [expanded-type
- #:declare expanded-type τ-cls
- (typecheck? #'expanded-type.ty #'τ-internal)]))
- (define (inferτ+erase e)
- (syntax-parse (infer+erase e) #:context e
- [(e- expanded-type)
- #:declare expanded-type τ-cls
- #:fail-unless (typecheck? #'expanded-type.ty #'τ-internal)
- (format
- "~a (~a:~a): Expected type of expression ~v to be ~a, got: ~a"
- (syntax-source e) (syntax-line e) (syntax-column e)
- (syntax->datum e) (type->str #'τ) (type->str #'expanded-type))
- #'e-]))))]))
+
+
+;; type assignment
+(begin-for-syntax
+ ;; macro for nicer syntax
+ (define-syntax (⊢ stx)
+ (syntax-parse stx #:datum-literals (:)
+ [(_ e : τ) #'(assign-type #'e #`τ)]
+ [(_ e τ) #'(⊢ e : τ)]))
+
+ ;; assign-type Type -> Syntax
+ ;; Attaches type τ to (expanded) expression e.
+ ;; must eval here, to catch unbound types
+ (define (assign-type e τ #:tag [tag 'type])
+ (syntax-property e tag (syntax-local-introduce ((current-type-eval) τ))))
+
+ ;; typeof : Syntax -> Type or #f
+ ;; Retrieves type of given stx, or #f if input has not been assigned a type.
+ (define (typeof stx #:tag [tag 'type]) (syntax-property stx tag))
+
+ ;; infers the type and erases types in an expression
+ (define (infer+erase e)
+ (define e+ (expand/df e))
+ (list e+ (typeof e+)))
+ ;; infers the types and erases types in multiple expressions
+ (define (infers+erase es)
+ (stx-map infer+erase es))
+
+ ;; This is the main "infer" function. All others are defined in terms of this.
+ ;; It should be named infer+erase but leaving it for now for backward compat.
+ ;; NOTE: differs slightly from infer/type-ctxt+erase in that types are not
+ ;; expanded before wrapping in lambda
+ ;; - This caused one problem in fomega2.rkt #%app, but I just had to expand
+ ;; the types before typechecking, which is acceptable
+ (define (infer es #:ctx [ctx null] #:tvctx [tvctx null] #:tag [tag 'type])
+ (syntax-parse ctx #:datum-literals (:)
+ [([x : τ] ...) ; dont expand yet bc τ may have references to tvs
+ #:with ([tv : k] ...) tvctx
+ #:with (e ...) es
+ #:with
+ ; old expander pattern
+ #;((~literal #%plain-lambda) tvs+
+ ((~literal #%expression)
+ ((~literal #%plain-lambda) xs+
+ ((~literal letrec-syntaxes+values) stxs1 ()
+ ((~literal letrec-syntaxes+values) stxs2 ()
+ ((~literal #%expression) e+) ...)))))
+ ; new expander pattern
+ ((~literal #%plain-lambda) tvs+
+ ((~literal let-values) () ((~literal let-values) ()
+ ((~literal #%expression)
+ ((~literal #%plain-lambda) xs+
+ ((~literal let-values) () ((~literal let-values) ()
+ ((~literal #%expression) e+) ...)))))))
+ (expand/df
+ #`(λ (tv ...)
+ (let-syntax ([tv (make-rename-transformer (assign-type #'tv #'k #:tag '#,tag))] ...)
+ (λ (x ...)
+ (let-syntax ([x (make-rename-transformer (assign-type #'x #'τ #:tag '#,tag))] ...)
+ (#%expression e) ...)))))
+ (list #'tvs+ #'xs+ #'(e+ ...)
+ (stx-map syntax-local-introduce (stx-map typeof #'(e+ ...))))]
+ [([x τ] ...) (infer es #:ctx #'([x : τ] ...) #:tvctx tvctx)]))
+
+ ;; fns derived from infer ---------------------------------------------------
+ ;; some are syntactic shortcuts, some are for backwards compat
+
+ ;; shorter name
+ (define (infer/ctx+erase ctx e)
+ (syntax-parse (infer (list e) #:ctx ctx)
+ [(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)]))
+ ;; infers type and erases types in a single expression,
+ ;; in the context of the given bindings and their types
+ (define (infer/type-ctxt+erase x+τs e)
+ (syntax-parse (infer (list e) #:ctx x+τs)
+ [(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)]))
+ ;; infers type and erases types in multiple expressions,
+ ;; in the context of (one set of) given bindings and their tpyes
+ (define (infers/type-ctxt+erase ctxt es)
+ (stx-cdr (infer es #:ctx ctxt)))
+ ;; infers and erases types in an expression, in the context of given type vars
+ #;(define (infer/tvs+erase e tvs)
+ (syntax-parse (infer (list e) #:tvs tvs)
+ [(tvs _ (e+) (τ)) (list #'tvs #'e+ #'τ)]))
+
+ ; type parameters, for type checker aspects that require extension
+ (define current-typecheck-relation (make-parameter #f))
+ (define (typecheck? t1 t2)
+ ((current-typecheck-relation) t1 t2)) ;((current-type-eval) t1) ((current-type-eval) t2)))
+ (define (typechecks? τs1 τs2)
+ (and (= (stx-length τs1) (stx-length τs2))
+ (stx-andmap typecheck? τs1 τs2)))
+
+ (define current-type-eval (make-parameter #f))
+ (define (type-evals τs) #`#,(stx-map (current-type-eval) τs))
+
+ ; get rid of this?
+ (define current-promote (make-parameter (λ (x) x)))
+
+ ;; term expansion
+ ;; 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)
+ (local-expand e 'expression null))
+
+ (struct exn:fail:type:check exn:fail:user ())
+
+ ;; 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
+ (exn:fail:type:check
+ (format (string-append "TYPE-ERROR: ~a (~a:~a): " msg)
+ (syntax-source stx-src) (syntax-line stx-src) (syntax-column stx-src)
+ (type->str args) ...)
+ (current-continuation-marks)))))
(begin-for-syntax
;; type validation
;; only check outer wrapper; tycons are responsible for verifying their own args
- (define (is-type? τ)
+ (define (#%type? t) (typecheck? t #'#%type))
+ #;(define (is-type? τ)
(or (plain-type? τ)
; partial expand to reveal #%type wrapper
(syntax-parse (local-expand τ 'expression (list #'#%type))
[((~literal #%type) _) #t] [_ #f])))
(define (plain-type? τ)
- (syntax-parse τ [((~literal #%plain-type) _) #t] [_ #f]))
+ (and (typeof τ) (typecheck? (typeof τ) #'#%type) τ))
; surface type syntax is saved as the value of the 'orig property
(define (add-orig stx orig)
@@ -127,7 +210,7 @@
;; - type
;; - type constructor identifier
;; - syntax-class representing shape of arguments to tycon
- (define-syntax (match-type stx)
+ #;(define-syntax (match-type stx)
(syntax-parse stx
[(_ ty tycon cls)
#'(syntax-parse ((current-type-eval) ty)
@@ -148,22 +231,186 @@
(define paren-shape/#f (syntax-property stx 'paren-shape))
(and paren-shape/#f (char=? paren-shape/#f #\[)))
(define-syntax-class bound-vars
- (pattern (~and stx [[x:id ...]])
- #:when (and (bracket? #'stx)
- (bracket? (stx-car #'stx)))))
+ (pattern
+ (~and stx [[x:id ...]]
+ #;[[(~and x:id (~not (~literal ...))) ... (~optional (~literal ...))]])
+ #:when (and (bracket? #'stx)
+ (bracket? (stx-car #'stx)))))
(begin-for-syntax
(define (bracket? stx)
(define paren-shape/#f (syntax-property stx 'paren-shape))
(and paren-shape/#f (char=? paren-shape/#f #\[)))
(define-syntax-class bound-vars
- (pattern (~and stx [[x:id ...]])
- #:when (and (bracket? #'stx)
- (bracket? (stx-car #'stx)))))))
+ (pattern
+ (~and stx [[x:id ...]]
+ #;[[(~and x:id (~not (~literal ...))) ... (~optional (~literal ...))]])
+ #:when (and (bracket? #'stx)
+ (bracket? (stx-car #'stx)))))))
+
+(begin-for-syntax
+ (define (mk-? id) (format-id id "~a?" id)))
+
+(define #%type void)
+(define-for-syntax (mk-type t) (assign-type t #'#%type))
+
+#;(define-syntax (define-base-type stx)
+ (syntax-parse stx
+ [(_ τ:id)
+ #:with τ? (format-id #'τ "~a?" #'τ)
+ #:with τ-internal (generate-temporary #'τ)
+ #:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
+ #:with τ-cls (generate-temporary #'τ)
+ #:with τ-expander (format-id #'τ "~~~a" #'τ)
+ #'(begin
+ (provide τ (for-syntax τ? inferτ+erase τ-expander))
+ (define τ-internal
+ (λ () (raise (exn:fail:type:runtime
+ (format "~a: Cannot use type at run time" 'τ)
+ (current-continuation-marks)))))
+ (define-syntax (τ stx)
+ (syntax-parse stx
+ [x:id (add-orig #'(#%type (τ-internal)) #'τ)]))
+ (begin-for-syntax
+ ; expanded form of τ
+ (define-syntax-class τ-cls
+ (pattern ((~literal #%plain-type) ((~literal #%plain-app) ty))))
+ (define (τ? t)
+ (syntax-parse ((current-type-eval) t)
+ [expanded-type
+ #:declare expanded-type τ-cls
+ (typecheck? #'expanded-type.ty #'τ-internal)]))
+ ; base type pattern expanders should be identifier macros but
+ ; parsing them is ambiguous, so handle and pass through other args
+ (define-syntax τ-expander
+ (pattern-expander
+ (syntax-parser
+ [ty:id #'((~literal #%plain-type)
+ ((~literal #%plain-app)
+ (~literal τ-internal)))]
+ [(_ . rst)
+ #'(((~literal #%plain-type)
+ ((~literal #%plain-app)
+ (~literal τ-internal))) . rst)])))
+ (define (inferτ+erase e)
+ (syntax-parse (infer+erase e) #:context e
+ [(e- expanded-type)
+ #:declare expanded-type τ-cls
+ #:fail-unless (typecheck? #'expanded-type.ty #'τ-internal)
+ (format
+ "~a (~a:~a): Expected type of expression ~v to be ~a, got: ~a"
+ (syntax-source e) (syntax-line e) (syntax-column e)
+ (syntax->datum e) (type->str #'τ) (type->str #'expanded-type))
+ #'e-]))))]))
-(define-syntax define-type-constructor
+(define-syntax define-basic-checked-id-stx
(syntax-parser
- [(_ (τ:id (~optional (~and bvs-pat:bound-vars bvs-test)
- #:defaults ([bvs-pat.stx #'[[]]]))
+ [(_ τ:id)
+ #:with τ? (format-id #'τ "~a?" #'τ)
+ #:with τ-internal (generate-temporary #'τ)
+ #:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
+ #:with τ-cls (generate-temporary #'τ)
+ #:with τ-expander (format-id #'τ "~~~a" #'τ)
+ #'(begin
+ (provide τ (for-syntax τ? τ-expander))
+ (begin-for-syntax
+ (define (τ? t) (typecheck? t #'τ-internal))
+ (define (inferτ+erase e)
+ (syntax-parse (infer+erase e) #:context e
+ [(e- e_τ)
+ #:fail-unless (τ? #'e_τ)
+ (format
+ "~a (~a:~a): Expected expression ~v to have type ~a, got: ~a"
+ (syntax-source e) (syntax-line e) (syntax-column e)
+ (syntax->datum e) (type->str #'τ) (type->str #'e_τ))
+ #'e-]))
+ (define-syntax τ-expander
+ (pattern-expander
+ (syntax-parser
+ [ty:id #'(~literal τ-internal)]
+ [(_ . rst)
+ #'((~literal τ-internal) . rst)]))))
+ (define τ-internal
+ (λ () (raise (exn:fail:type:runtime
+ (format "~a: Cannot use type at run time" 'τ)
+ (current-continuation-marks)))))
+ (define-syntax τ
+ (syntax-parser
+ [(~var _ id) (add-orig (assign-type #'τ-internal #'#%type) #'τ)])))]))
+
+(define-syntax define-base-type (syntax-parser [(_ τ:id) #'(define-basic-checked-id-stx τ)]))
+
+(define-syntax (define-basic-checked-stx stx)
+ (syntax-parse stx
+ [(_ τ:id (~optional
+ (~seq #:arity op n:exact-nonnegative-integer)
+ #:defaults ([op #'>=] [n #'0])))
+ #:with τ-internal (generate-temporary #'τ)
+ #:with τ? (mk-? #'τ)
+ #:with τ-expander (format-id #'τ "~~~a" #'τ)
+ #:with τ-expander* (format-id #'τ-expander "~a*" #'τ-expander)
+ #:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ)
+ #'(begin
+ (provide τ (for-syntax τ-expander τ-expander* inferτ+erase))
+ (begin-for-syntax
+ (define-syntax τ-expander
+ (pattern-expander
+ (syntax-parser
+ [(_ . pat)
+ #'((~literal #%plain-app) (~literal τ-internal) . pat)])))
+ (define-syntax τ-expander*
+ (pattern-expander
+ (syntax-parser
+ [(_ . pat)
+ #'(~or
+ ;((~literal #%plain-app) (~literal τ-internal) . pat)
+ (τ-expander . pat)
+ (~and
+ any
+ (~do
+ (type-error #:src #'any
+ #:msg
+ "Expected ~a type, got: ~a"
+ #'τ #'any))))])))
+ (define (τ? t) (and (stx-pair? t) (typecheck? (stx-cadr t) #'τ-internal)))
+ (define (inferτ+erase e)
+ (syntax-parse (infer+erase e) #:context e
+ [(e- τ_e)
+ #:fail-unless (stx-pair? #'τ_e)
+ (format
+ "~a (~a:~a): Expected expression ~a to have ~a type, got: ~a"
+ (syntax-source e) (syntax-line e) (syntax-column e)
+ (syntax->datum e) 'τ (type->str #'τ_e))
+ #:with ((~literal #%plain-app) tycon . args) #'τ_e
+ #:fail-unless (typecheck? #'tycon #'τ-internal)
+ (format
+ "~a (~a:~a): Expected expression ~a to have ~a type, got: ~a"
+ (syntax-source e) (syntax-line e) (syntax-column e)
+ (syntax->datum e) 'τ (type->str #'τ_e))
+ #`(e- args)])))
+ (define τ-internal
+ (λ _ (raise (exn:fail:type:runtime
+ (format "~a: Cannot use type at run time" 'τ)
+ (current-continuation-marks)))))
+ ;(define (τ? ty) (syntax-parser ty [((~literal τ) . pat) #t][_ #f]))
+ ;; ; this is the actual constructor
+ (define-syntax (τ stx)
+ (syntax-parse stx
+ [(_ . args)
+ #:fail-unless (op (stx-length #'args) n)
+ (format "wrong number of arguments, expected ~a ~a" 'op 'n)
+ #:with (~! (~var ty type) (... ...)) #'args
+; #:with (~! [arg- τ_arg] (... ...)) (infers+erase #'args)
+; #:when (stx-andmap (λ (t) (typecheck? t #'#%type)) #'(τ_arg (... ...)))
+ (assign-type #'(τ-internal ty.norm (... ...)) #'#%type)]
+ ;; else fail with err msg
+ [_
+ (type-error #:src stx
+ #:msg (string-append
+ "Improper usage of type constructor ~a: ~a, expected ~a ~a arguments")
+ #'τ stx #'op #'n)])))]
+ #;[(_ #:cat cat
+ (τ:id (~optional (~and bvs-pat:bound-vars bvs-test) ; bvs-test checks for existence of bound vars
+ #:defaults ([bvs-pat.stx #'[[]]][(bvs-pat.x 1) null]))
. pat)
; lits must have ~ prefix (for syntax-parse compat) for now
(~optional (~seq #:lits (lit ...)) #:defaults ([(lit 1) null]))
@@ -175,6 +422,7 @@
#:with τ-get (format-id #'τ "~a-get" #'τ)
#:with τ-match+erase (format-id #'τ "infer~a+erase" #'τ)
#:with τ-expander (format-id #'τ "~~~a" #'τ)
+ #:with τ-expander* (format-id #'τ "~~~a*" #'τ)
#:with pat-class (generate-temporary #'τ) ; syntax-class name
#:with tycon (generate-temporary #'τ) ; need a runtime id for expansion
#:with (lit-tmp ...) (generate-temporaries #'(lit ...))
@@ -185,20 +433,41 @@
(define lit-tmp void) ...
(define-syntax lit (syntax-parser [(_ . xs) #'(lit-tmp . xs)])) ...
(provide lit ...)
- (provide τ (for-syntax τ-expander))
+ (provide τ (for-syntax τ-expander τ-expander*))
(begin-for-syntax
- #'(define-syntax lit
+ #;(define-syntax lit
(pattern-expander
(syntax-parser
[(_ . xs)
- #'((~literal #%plain-app) (~literal lit-tmp) . xs)]))) ...
+ #'((~literal #%plain-app) (~literal lit-tmp) . xs)]))) ;...
+ ; the ~τ pattern backtracks normally;
+ ; the ~τ* version errors immediately for a non-match
(define-syntax τ-expander
(pattern-expander
(syntax-parser
[(_ (~optional
(~and bvs:bound-vars bvs-pat.stx) #:defaults ([(bvs.x 1) null]))
. match-pat)
- #:with pat-from-constructor (quote-syntax (τ . pat))
+ ;; manually replace literals with expanded form, to get around ~ restriction
+ #:with new-match-pat
+ #`#,(subst-datum-lits
+ #`((#,(quote-syntax ~seq) (~literal #%plain-app) (~literal lit-tmp)) ...)
+ #'(lit ...)
+ #'match-pat)
+ #'((~literal #%plain-type)
+ ((~literal #%plain-lambda) (bvs.x (... ...))
+ ((~literal let-values) () ((~literal let-values) ()
+ ((~literal #%plain-app) (~literal tycon) . new-match-pat)))))])))
+ (define-syntax τ-expander*
+ (pattern-expander
+ (syntax-parser
+ [(_ (~optional
+ (~and bvs:bound-vars bvs-pat.stx) #:defaults ([(bvs.x 1) null]))
+ . match-pat)
+ #:with pat-from-constructor
+ #,(if (attribute bvs-test)
+ #'(quote-syntax (τ bvs-pat.stx . pat))
+ #'(quote-syntax (τ . pat)))
;; manually replace literals with expanded form, to get around ~ restriction
#:with new-match-pat
#`#,(subst-datum-lits
@@ -271,16 +540,20 @@
(current-continuation-marks)))))
(define-syntax (τ stx)
(syntax-parse stx #:literals (lit ...)
- [(_ (~optional (~and bvs:bound-vars bvs-pat.stx)
- #:defaults ([(bvs.x 1) null]))
- . (~and pat !~ args)) ; first check shape
+ [(_ (~optional (~or (~and bvs:bound-vars bvs-pat.stx)
+ (~seq #:bind (~and bvs (bvs-pat.x ...)))))
+ . (~and pat ~! args)) ; first check shape
+ #:with (tv (... ...)) (cond [(attribute bvs.x) #'(bvs.x (... ...))]
+ [(attribute bvs) #'bvs]
+ [else null])
; this inner syntax-parse gets the ~! to register
; otherwise, apparently #:declare's get subst into pat (before ~!)
(syntax-parse #'args #:literals (lit ...)
[pat #,@#'(decls ...) ; then check declarations (eg, valid type)
#'(#%type
- (λ (bvs.x (... ...))
- (let-syntax ([bvs.x (syntax-parser [bvs.x:id #'(#%type bvs.x)])] (... ...))
+ (λ (tv (... ...)) ;(bvs.x (... ...))
+; (let-syntax ([bvs.x (syntax-parser [bvs.x:id #'(#%type bvs.x)])] (... ...))
+ (let-syntax ([tv (syntax-parser [tv:id #'(#%type tv)])] (... ...))
(tycon . args))))])]
[_
#:with expected-pat
@@ -299,6 +572,173 @@
", ")))
#'τ stx #'expected-pat)])))]))
+; define-type-constructor, archied 2015-08-12
+;(define-syntax define-type-constructor
+; (syntax-parser
+; [(_ (τ:id (~optional (~and bvs-pat:bound-vars bvs-test) ; bvs-test checks for existence of bound vars
+; #:defaults ([bvs-pat.stx #'[[]]][(bvs-pat.x 1) null]))
+; . pat)
+; ; lits must have ~ prefix (for syntax-parse compat) for now
+; (~optional (~seq #:lits (lit ...)) #:defaults ([(lit 1) null]))
+; decls ...
+; #;(~optional (~seq (~seq #:decl tvar (~datum as) cls) ...)
+; #:defaults ([(tvar 1) null][(cls 1) null])))
+; #:with τ-match (format-id #'τ "~a-match" #'τ)
+; #:with τ? (format-id #'τ "~a?" #'τ)
+; #:with τ-get (format-id #'τ "~a-get" #'τ)
+; #:with τ-match+erase (format-id #'τ "infer~a+erase" #'τ)
+; #:with τ-expander (format-id #'τ "~~~a" #'τ)
+; #:with τ-expander* (format-id #'τ "~~~a*" #'τ)
+; #:with pat-class (generate-temporary #'τ) ; syntax-class name
+; #:with tycon (generate-temporary #'τ) ; need a runtime id for expansion
+; #:with (lit-tmp ...) (generate-temporaries #'(lit ...))
+; #`(begin
+; ;; list can't be function, ow it will use typed #%app
+; ;; define lit as macro that expands into #%app,
+; ;; so it will use the #%app here (racket's #%app)
+; (define lit-tmp void) ...
+; (define-syntax lit (syntax-parser [(_ . xs) #'(lit-tmp . xs)])) ...
+; (provide lit ...)
+; (provide τ (for-syntax τ-expander τ-expander*))
+; (begin-for-syntax
+; #;(define-syntax lit
+; (pattern-expander
+; (syntax-parser
+; [(_ . xs)
+; #'((~literal #%plain-app) (~literal lit-tmp) . xs)]))) ;...
+; ; the ~τ pattern backtracks normally;
+; ; the ~τ* version errors immediately for a non-match
+; (define-syntax τ-expander
+; (pattern-expander
+; (syntax-parser
+; [(_ (~optional
+; (~and bvs:bound-vars bvs-pat.stx) #:defaults ([(bvs.x 1) null]))
+; . match-pat)
+; ;; manually replace literals with expanded form, to get around ~ restriction
+; #:with new-match-pat
+; #`#,(subst-datum-lits
+; #`((#,(quote-syntax ~seq) (~literal #%plain-app) (~literal lit-tmp)) ...)
+; #'(lit ...)
+; #'match-pat)
+; #'((~literal #%plain-type)
+; ((~literal #%plain-lambda) (bvs.x (... ...))
+; ((~literal let-values) () ((~literal let-values) ()
+; ((~literal #%plain-app) (~literal tycon) . new-match-pat)))))])))
+; (define-syntax τ-expander*
+; (pattern-expander
+; (syntax-parser
+; [(_ (~optional
+; (~and bvs:bound-vars bvs-pat.stx) #:defaults ([(bvs.x 1) null]))
+; . match-pat)
+; #:with pat-from-constructor
+; #,(if (attribute bvs-test)
+; #'(quote-syntax (τ bvs-pat.stx . pat))
+; #'(quote-syntax (τ . pat)))
+; ;; manually replace literals with expanded form, to get around ~ restriction
+; #:with new-match-pat
+; #`#,(subst-datum-lits
+; #`((#,(quote-syntax ~seq) (~literal #%plain-app) (~literal lit-tmp)) ...)
+; #'(lit ...)
+; #'match-pat)
+; #'(~and
+; (~or
+; ((~literal #%plain-type)
+; ((~literal #%plain-lambda) (bvs.x (... ...))
+; ((~literal let-values) () ((~literal let-values) ()
+; ((~literal #%plain-app) (~literal tycon) . new-match-pat)))))
+; (~and any
+; (~do
+; (type-error #:src #'any
+; #:msg
+; "Expected type of expression to match pattern ~a, got: ~a"
+; (quote-syntax pat-from-constructor) #'any))))
+; ~!)])))
+; (define-syntax-class pat-class
+; ;; dont check is-type? here; should already be types
+; ;; only check is-type? for user-entered types, eg tycon call
+; ;; thus, dont include decls here, only want shape
+; ; uses "lit" pattern expander
+; (pattern pat))
+; (define (τ-match ty)
+; (or (match-type ty tycon pat-class)
+; ;; error msg should go in specific macro def?
+; (type-error #:src ty
+; #:msg "Expected type with pattern: ~a, got: ~a"
+; (quote-syntax (τ . pat)) ty)))
+; ; predicate version of τ-match
+; (define (τ? ty) (match-type ty tycon pat-class))
+; ;; expression version of τ-match
+; (define (τ-match+erase e)
+; (syntax-parse (infer+erase e)
+; [(e- ty)
+; #:with τ_matched/#f (match-type #'ty tycon pat-class)
+; #:fail-unless (syntax-e #'τ_matched/#f)
+; (format
+; "~a (~a:~a): Expected type of expression ~a to match pattern ~a, got: ~a"
+; (syntax-source e) (syntax-line e) (syntax-column e)
+; (syntax->datum e) (type->str (quote-syntax (τ . pat))) (type->str #'ty))
+; #'(e- τ_matched/#f)]))
+; ;; get syntax bound to specific pat var (as declared in def-tycon)
+; (define-syntax (τ-get stx)
+; (syntax-parse stx #:datum-literals (from)
+; [(_ attr from ty)
+; #:with args (generate-temporary)
+; #:with args.attr (format-id #'args "~a.~a" #'args #'attr)
+; #:with the-pat (quote-syntax (τ . pat))
+; #'(syntax-parse #'ty ;((current-type-eval) #'ty)
+; [typ ;((~literal #%plain-type) ((~literal #%plain-app) f . args))
+; #:fail-unless (τ? #'typ)
+; (format "~a (~a:~a) Expected type with pattern: ~a, got: ~a"
+; (syntax-source #'typ) (syntax-line #'typ) (syntax-column #'typ)
+; (type->str (quote-syntax the-pat)) (type->str #'typ))
+; #:with ((~literal #%plain-type)
+; ((~literal #%plain-lambda) tvs
+; ((~literal let-values) () ((~literal let-values) ()
+; ((~literal #%plain-app) f . args)))))
+; ((current-type-eval) #'typ)
+; #:declare args pat-class ; check shape of arguments
+;; #:fail-unless (typecheck? #'f #'tycon) ; check tycons match
+;; (format "Type error: expected ~a type, got ~a"
+;; (type->str #'τ) (type->str #'ty))
+; (attribute args.attr)])])))
+; (define tycon (λ _ (raise (exn:fail:type:runtime
+; (format "~a: Cannot use type at run time" 'τ)
+; (current-continuation-marks)))))
+; (define-syntax (τ stx)
+; (syntax-parse stx #:literals (lit ...)
+; [(_ (~optional (~or (~and bvs:bound-vars bvs-pat.stx)
+; (~seq #:bind (~and bvs (bvs-pat.x ...)))))
+; . (~and pat ~! args)) ; first check shape
+; #:with (tv (... ...)) (cond [(attribute bvs.x) #'(bvs.x (... ...))]
+; [(attribute bvs) #'bvs]
+; [else null])
+; ; this inner syntax-parse gets the ~! to register
+; ; otherwise, apparently #:declare's get subst into pat (before ~!)
+; (syntax-parse #'args #:literals (lit ...)
+; [pat #,@#'(decls ...) ; then check declarations (eg, valid type)
+; #'(#%type
+; (λ (tv (... ...)) ;(bvs.x (... ...))
+;; (let-syntax ([bvs.x (syntax-parser [bvs.x:id #'(#%type bvs.x)])] (... ...))
+; (let-syntax ([tv (syntax-parser [tv:id #'(#%type tv)])] (... ...))
+; (tycon . args))))])]
+; [_
+; #:with expected-pat
+; #,(if (attribute bvs-test)
+; #'(quote-syntax (τ bvs-pat.stx . pat))
+; #'(quote-syntax (τ . pat)))
+; (type-error #:src stx
+; #:msg (string-append
+; "Improper usage of type constructor ~a: ~a, expected pattern ~a, "
+; #;(format
+; "where: ~a"
+; (string-join
+; (stx-map
+; (λ (typ clss) (format "~a is a ~a" typ clss))
+; #'(ty (... ...)) #'(cls (... ...)))
+; ", ")))
+; #'τ stx #'expected-pat)])))]))
+
+
;; TODO: refine this to enable specifying arity information
;; type constructors currently must have 1+ arguments
;#;(define-syntax (define-type-constructor stx)
@@ -360,18 +800,20 @@
;; syntax classes
(begin-for-syntax
(define-syntax-class type
- ;; stx = surface syntax, as written
- ;; norm = canonical form for the type
+ ;; τ = surface syntax, as written
+ ;; norm = canonical form for the type, ie expanded
+ ;; -dont bother to check if type is already expanded, because this class
+ ;; typically annotates user-written types
(pattern τ
- #:fail-unless (is-type? #'τ)
+ #:with [norm k] (infer+erase #'τ)
+ #:fail-unless (#%type? #'k)
(format "~a (~a:~a) not a valid type: ~a"
(syntax-source #'τ) (syntax-line #'τ) (syntax-column #'τ)
- (type->str #'τ))
- #:attr norm (delay ((current-type-eval) #'τ))))
+ (type->str #'τ))))
(define-syntax-class typed-binding #:datum-literals (:)
- #:attributes (x τ norm)
- (pattern [x:id : ~! τ:type] #:attr norm (delay #'τ.norm))
+ #:attributes (x τ)
+ (pattern [x:id : ~! ty:type] #:attr τ #'ty.norm)
(pattern any
#:fail-when #t
(format
@@ -379,7 +821,7 @@
"Improperly formatted type annotation: ~a; should have shape [x : τ], "
"where τ is a valid type.")
(type->str #'any))
- #:attr x #f #:attr τ #f #:attr norm #f))
+ #:attr x #f #:attr τ #f))
(define (brace? stx)
(define paren-shape/#f (syntax-property stx 'paren-shape))
@@ -400,127 +842,11 @@
(type->str #'any))
#:attr τ #f #:attr norm #f)))
-;; type assignment
-(begin-for-syntax
- ;; macro for nicer syntax
- (define-syntax (⊢ stx)
- (syntax-parse stx #:datum-literals (:)
- [(_ e : τ) #'(assign-type #'e #`τ)]
- [(_ e τ) #'(⊢ e : τ)]))
-
- ;; assign-type Type -> Syntax
- ;; Attaches type τ to (expanded) expression e.
- ;; must eval here, to catch unbound types
- (define (assign-type e τ #:tag [tag 'type])
- (syntax-property e tag (syntax-local-introduce ((current-type-eval) τ))))
-
- ;; typeof : Syntax -> Type or #f
- ;; Retrieves type of given stx, or #f if input has not been assigned a type.
- (define (typeof stx #:tag [tag 'type]) (syntax-property stx tag))
-
- ;; infers the type and erases types in an expression
- (define (infer+erase e)
- (define e+ (expand/df e))
- (list e+ (typeof e+)))
- ;; infers the types and erases types in multiple expressions
- (define (infers+erase es)
- (stx-map infer+erase es))
-
- ;; This is the main "infer" function. All others are defined in terms of this.
- ;; It should be named infer+erase but leaving it for now for backward compat.
- ;; NOTE: differs slightly from infer/type-ctxt+erase in that types are not
- ;; expanded before wrapping in lambda
- ;; - This caused one problem in fomega2.rkt #%app, but I just had to expand
- ;; the types before typechecking, which is acceptable
- (define (infer es #:ctx [ctx null] #:tvs [tvs null] #:tag [tag 'type])
- (syntax-parse ctx #:datum-literals (:)
- [([x : τ] ...) ; dont expand yet bc τ may have references to tvs
- #:with (e ...) es
- #:with (tv ...) tvs
- #:with
- ; old expander pattern
- #;((~literal #%plain-lambda) tvs+
- ((~literal #%expression)
- ((~literal #%plain-lambda) xs+
- ((~literal letrec-syntaxes+values) stxs1 ()
- ((~literal letrec-syntaxes+values) stxs2 ()
- ((~literal #%expression) e+) ...)))))
- ; new expander pattern
- ((~literal #%plain-lambda) tvs+
- ((~literal let-values) () ((~literal let-values) ()
- ((~literal #%expression)
- ((~literal #%plain-lambda) xs+
- ((~literal let-values) () ((~literal let-values) ()
- ((~literal #%expression) e+) ...)))))))
- (expand/df
- #`(λ (tv ...)
- (let-syntax ([tv (syntax-parser [tv:id #'(#%type tv)])] ...)
- (λ (x ...)
- (let-syntax ([x (make-rename-transformer (assign-type #'x #'τ #:tag '#,tag))] ...)
- (#%expression e) ...)))))
- (list #'tvs+ #'xs+ #'(e+ ...)
- (stx-map syntax-local-introduce (stx-map typeof #'(e+ ...))))]
- [([x τ] ...) (infer es #:ctx #'([x : τ] ...) #:tvs tvs)]))
-
- ;; fns derived from infer ---------------------------------------------------
- ;; some are syntactic shortcuts, some are for backwards compat
-
- ;; infers type and erases types in a single expression,
- ;; in the context of the given bindings and their types
- (define (infer/type-ctxt+erase x+τs e)
- (syntax-parse (infer (list e) #:ctx x+τs)
- [(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)]))
- ;; infers type and erases types in multiple expressions,
- ;; in the context of (one set of) given bindings and their tpyes
- (define (infers/type-ctxt+erase ctxt es)
- (stx-cdr (infer es #:ctx ctxt))) ; drop (empty) tyvars from result
- ;; infers and erases types in an expression, in the context of given type vars
- (define (infer/tvs+erase e tvs)
- (syntax-parse (infer (list e) #:tvs tvs)
- [(tvs _ (e+) (τ)) (list #'tvs #'e+ #'τ)]))
-
- ; type parameters, for type checker aspects that require extension
- (define current-typecheck-relation (make-parameter #f))
- (define (typecheck? t1 t2)
- ((current-typecheck-relation) ((current-type-eval) t1) ((current-type-eval) t2)))
- (define (typechecks? τs1 τs2)
- (and (= (stx-length τs1) (stx-length τs2))
- (stx-andmap typecheck? τs1 τs2)))
-
- (define current-type-eval (make-parameter #f))
- (define (type-evals τs) #`#,(stx-map (current-type-eval) τs))
-
- ; get rid of this?
- (define current-promote (make-parameter (λ (x) x)))
-
- ;; term expansion
- ;; 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)
- (local-expand e 'expression null))
-
- (struct exn:fail:type:check exn:fail:user ())
- ;; 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
- (exn:fail:type:check
- (format (string-append "TYPE-ERROR: ~a (~a:~a): " msg)
- (syntax-source stx-src) (syntax-line stx-src) (syntax-column stx-src)
- (type->str args) ...)
- (current-continuation-marks)))))
(define-syntax (define-primop stx)
(syntax-parse stx #:datum-literals (:)
- [(_ op:id : τ)
+ [(_ op:id : τ:type)
#:with op/tc (generate-temporary #'op)
#`(begin
(provide (rename-out [op/tc op]))
@@ -532,7 +858,6 @@
#:with op (format-id stx "~a" #'op)
(syntax/loc stx (app op x (... ...)))])))]))
-(define-for-syntax (mk-pred x) (format-id x "~a?" x))
(define-for-syntax (mk-acc base field) (format-id base "~a-~a" base field))
(begin-for-syntax
