From 4e80959d1212710442d733d98adc3260606bdcd8 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Mon, 31 Jul 2017 16:35:33 -0400 Subject: [PATCH] start over with dep2; basic lam/app working; no instantiation --- turnstile/examples/dep.rkt | 2 +- turnstile/examples/dep2.rkt | 389 ++++++++++++++++++++++++ turnstile/examples/tests/dep2-tests.rkt | 237 +++++++++++++++ 3 files changed, 627 insertions(+), 1 deletion(-) create mode 100644 turnstile/examples/dep2.rkt create mode 100644 turnstile/examples/tests/dep2-tests.rkt diff --git a/turnstile/examples/dep.rkt b/turnstile/examples/dep.rkt index 7eae980..481e510 100644 --- a/turnstile/examples/dep.rkt +++ b/turnstile/examples/dep.rkt @@ -103,7 +103,7 @@ (define-typed-syntax #%app [(_ e_fn e_arg ...) ≫ ; apply lambda - #:do[(printf "applying (1) ~a\n" (stx->datum #'e_fn))] +; #:do[(printf "applying (1) ~a\n" (stx->datum #'e_fn))] [⊢ e_fn ≫ (~and e_fn- (_ (x:id ...) e ~!)) ⇒ (~Π ([X : τ_inX] ...) τ_outX)] #:do[(printf "e_fn-: ~a\n" (stx->datum #'e_fn-)) (printf "args: ~a\n" (stx->datum #'(e_arg ...)))] diff --git a/turnstile/examples/dep2.rkt b/turnstile/examples/dep2.rkt new file mode 100644 index 0000000..743f394 --- /dev/null +++ b/turnstile/examples/dep2.rkt @@ -0,0 +1,389 @@ +#lang turnstile/lang + +; second attempt at a basic dependently-typed calculus +; initially copied from dep.rkt + +; Π λ ≻ ⊢ ≫ → ∧ (bidir ⇒ ⇐) τ⊑ + +(provide (rename-out [#%type *]) + Π → ∀ +;; = eq-refl eq-elim +;; Nat Z S nat-ind + λ + #%app ann + define define-type-alias +) + +;; #;(begin-for-syntax +;; (define old-ty= (current-type=?)) +;; (current-type=? +;; (λ (t1 t2) +;; (displayln (stx->datum t1)) +;; (displayln (stx->datum t2)) +;; (old-ty= t1 t2))) +;; (current-typecheck-relation (current-type=?))) + +;(define-syntax-category : kind) ; defines #%kind for #%type +;; (define-base-type Nat) + +;; set Type : Type +;; alternatively, could define new base type Type, +;; and make #%type typecheck with Type +(begin-for-syntax + ;; TODO: fix `type` stx class + ;; (define old-type? (current-type?)) + ;; (current-type? + ;; (lambda (t) (or (#%type? t) (old-type? t)))) + (define old-relation (current-typecheck-relation)) + (current-typecheck-relation + (lambda (t1 t2) + ;; assumed #f can only come from (typeof #%type) + ;; (so this wont work when interacting with untyped code) + (or (and (false? (syntax-e t1)) (#%type? t2)) ; set Type : Type + (old-relation t1 t2))))) +(define-for-syntax Type ((current-type-eval) #'#%type)) + +(define-internal-type-constructor →) ; equiv to Π with no uses on rhs +(define-internal-binding-type ∀) ; equiv to Π with #%type for all params + +;; Π expands into combination of internal →- and ∀- +;; uses "let*" syntax where X_i is in scope for τ_i+1 ... +;; TODO: add tests to check this +(define-typed-syntax (Π ([X:id : τ_in] ...) τ_out) ≫ + ;; TODO: check that τ_in and τ_out have #%type? + [[X ≫ X- : τ_in] ... ⊢ [τ_out ≫ τ_out- ⇒ _] [τ_in ≫ τ_in- ⇒ _] ...] + ------- + [⊢ (∀- (X- ...) (→- τ_in- ... τ_out-)) ⇒ #,Type #;#%type]) + +;; abbrevs for Π +(define-simple-macro (→ τ_in ... τ_out) + #:with (X ...) (generate-temporaries #'(τ_in ...)) + (Π ([X : τ_in] ...) τ_out)) +(define-simple-macro (∀ (X ...) τ) + (Π ([X : #%type] ...) τ)) + +;; pattern expanders +(begin-for-syntax + (define-syntax ~Π + (pattern-expander + (syntax-parser + [(_ ([x:id : τ_in] ... (~and (~literal ...) ooo)) τ_out) + #'(~∀ (x ... ooo) (~→ τ_in ... ooo τ_out))] + [(_ ([x:id : τ_in] ...) τ_out) + #'(~∀ (x ...) (~→ τ_in ... τ_out))])))) + +;; ;; equality ------------------------------------------------------------------- +;; (define-internal-type-constructor =) +;; (define-typed-syntax (= t1 t2) ≫ +;; [⊢ t1 ≫ t1- ⇒ _] [⊢ t2 ≫ t2- ⇒ _] +;; ;; #:do [(printf "t1: ~a\n" (stx->datum #'t1-)) +;; ;; (printf "t2: ~a\n" (stx->datum #'t2-))] +;; ; [t1- τ= t2-] +;; --------------------- +;; [⊢ (=- t1- t2-) ⇒ #,(expand/df #'#%type)]) + +;; (define-typed-syntax (eq-refl e) ≫ +;; [⊢ e ≫ e- ⇒ _] +;; ---------- +;; [⊢ (#%app- void-) ⇒ (= e- e-)]) + +;; (define-typed-syntax (eq-elim t P pt w peq) ≫ +;; [⊢ t ≫ t- ⇒ ty] +;; ; [⊢ P ≫ P- ⇒ _] +;; ; [⊢ pt ≫ pt- ⇒ _] +;; ; [⊢ w ≫ w- ⇒ _] +;; ; [⊢ peq ≫ peq- ⇒ _] +;; [⊢ P ≫ P- ⇐ (→ ty #%type)] +;; [⊢ pt ≫ pt- ⇐ (P- t-)] +;; [⊢ w ≫ w- ⇐ ty] +;; [⊢ peq ≫ peq- ⇐ (= t- w-)] +;; -------------- +;; [⊢ (#%app- void-) ⇒ (P- w-)]) + +;; lambda and #%app ----------------------------------------------------------- + +;; TODO: fix `type` stx class +(define-typed-syntax λ + ;; expected ty only + [(_ (y:id ...) e) ⇐ (~Π ([x:id : τ_in] ... ) τ_out) ≫ + [[x ≫ x- : τ_in] ... ⊢ #,(substs #'(x ...) #'(y ...) #'e) ≫ e- ⇐ τ_out] + --------- + [⊢ (λ- (x- ...) e-)]] + ;; both expected ty and annotations + [(_ ([y:id : τ_in*] ...) e) ⇐ (~Π ([x:id : τ_in] ...) τ_out) ≫ +; [(_ ([y:id : τy_in:type] ...) e) ⇐ (~Π ([x:id : τ_in] ...) τ_out) ≫ + #:fail-unless (stx-length=? #'(y ...) #'(x ...)) + "function's arity does not match expected type" + [⊢ τ_in* ≫ τ_in** ⇐ #%type] ... +; #:when (typechecks? (stx-map (current-type-eval) #'(τ_in* ...)) + #:when (typechecks? #'(τ_in** ...) #'(τ_in ...)) +; #:when (typechecks? #'(τy_in.norm ...) #'(τ_in ...)) +; [τy_in τ= τ_in] ... + [[x ≫ x- : τ_in] ... ⊢ #,(substs #'(x ...) #'(y ...) #'e) ≫ e- ⇐ τ_out] + ------- + [⊢ (λ- (x- ...) e-)]] + ;; annotations only + [(_ ([x:id : τ_in] ...) e) ≫ + [[x ≫ x- : τ_in] ... ⊢ [e ≫ e- ⇒ τ_out] [τ_in ≫ τ_in- ⇒ _] ...] + ------- + [⊢ (λ- (x- ...) e-) ⇒ (Π ([x- : τ_in-] ...) τ_out)]]) + +;; ;; classes for matching number literals +;; (begin-for-syntax +;; (define-syntax-class nat +;; (pattern (~or n:exact-nonnegative-integer (_ n:exact-nonnegative-integer)) +;; #:attr val +;; #'n)) +;; (define-syntax-class nats +;; (pattern (n:nat ...) #:attr vals #'(n.val ...))) +;; ; extract list of quoted numbers +;; (define stx->nat (syntax-parser [n:nat (stx-e #'n.val)])) +;; (define (stx->nats stx) (stx-map stx->nat stx)) +;; (define (stx+ ns) (apply + (stx->nats ns))) +;; (define (delta op-stx args) +;; (syntax-parse op-stx +;; [(~literal +-) (stx+ args)] +;; [(~literal zero?-) (apply zero? (stx->nats args))]))) + +(define-typed-syntax #%app + [(_ e_fn e_arg ...) ≫ +; [⊢ e_fn ≫ (~and e_fn- (_ (x:id ...) e ~!)) ⇒ (~Π ([X : τ_inX] ...) τ_outX)] + [⊢ e_fn ≫ e_fn- ⇒ (~Π ([X : τ_in] ...) τ_out)] + #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...]) + (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...]) + [⊢ e_arg ≫ e_arg- ⇐ τ_in] ... ; typechecking args + ----------------------------- + [⊢ (#%app- e_fn- e_arg- ...) ⇒ τ_out]]) + +#;(define-typed-syntax #%app + [(_ e_fn e_arg ...) ≫ ; apply lambda + #:do[(printf "applying (1) ~a\n" (stx->datum #'e_fn))] + [⊢ e_fn ≫ (~and e_fn- (_ (x:id ...) e ~!)) ⇒ (~Π ([X : τ_inX] ...) τ_outX)] + #:do[(printf "e_fn-: ~a\n" (stx->datum #'e_fn-)) + (printf "args: ~a\n" (stx->datum #'(e_arg ...)))] + #:fail-unless (stx-length=? #'[τ_inX ...] #'[e_arg ...]) + (num-args-fail-msg #'e_fn #'[τ_inX ...] #'[e_arg ...]) + [⊢ e_arg ≫ e_argX- ⇒ ty-argX] ... ; typechecking args must be fold; do in 2 steps + #:do[(define (ev e) + (syntax-parse e +; [_ #:do[(printf "eval: ~a\n" (stx->datum e))] #:when #f #'(void)] + [(~or _:id +; ((~literal #%plain-lambda) . _) + (~= _ _) + ~Nat + ((~literal quote) _)) + e] + ;; handle nums + [((~literal #%plain-app) + (~and op (~or (~literal +-) (~literal zero?-))) + . args:nats) + #`#,(delta #'op #'args.vals)] + [((~literal #%plain-app) (~and f ((~literal #%plain-lambda) . b)) . rst) + (expand/df #`(#%app f . #,(stx-map ev #'rst)))] + [(x ...) + ;; #:do[(printf "t before: ~a\n" (typeof e)) + ;; (printf "t after: ~a\n" (typeof #`#,(stx-map ev #'(x ...))))] + (syntax-property #`#,(stx-map ev #'(x ...)) ': (typeof e))] + [_ e] ; other literals + #;[es (stx-map L #'es)]))] + #:with (ty-arg ...) + (stx-map + (λ (t) (ev (substs #'(e_argX- ...) #'(X ...) t))) + #'(ty-argX ...)) + #:with (e_arg- ...) (stx-map (λ (e t) (assign-type e t)) #'(e_argX- ...) #'(ty-arg ...)) + #:with (τ_in ... τ_out) + (stx-map + (λ (t) (ev (substs #'(e_arg- ...) #'(X ...) t))) + #'(τ_inX ... τ_outX)) +; #:do[(printf "vars: ~a\n" #'(X ...))] +; #:when (stx-andmap (λ (t1 t2)(displayln (stx->datum t1)) (displayln (stx->datum t2)) (displayln (typecheck? t1 t2)) #;(typecheck? t1 t2)) #'(ty-arg ...) #'(τ_in ...)) + ;; #:do[(stx-map + ;; (λ (tx t) (printf "ty_in inst: \n~a\n~a\n" (stx->datum tx) (stx->datum t))) + ;; #'(τ_inX ...) #'(τ_in ...))] +; [⊢ e_arg- ≫ _ ⇐ τ_in] ... + #:do[(printf "res e =\n~a\n" (stx->datum (substs #'(e_arg- ...) #'(x ...) #'e))) + (printf "res t = ~a\n" (stx->datum (substs #'(e_arg- ...) #'(X ...) #'τ_out)))] + #:with res-e (let L ([e (substs #'(e_arg- ...) #'(x ...) #'e)]) ; eval + (syntax-parse e + [(~or _:id + ((~literal #%plain-lambda) . _) + (~Π ([_ : _] ...) _) + (~= _ _) + ~Nat) + e] + ;; handle nums + [((~literal #%plain-app) + (~and op (~or (~literal +-) (~literal zero?-))) + . args:nats) + #`#,(delta #'op #'args.vals)] + [((~literal #%plain-app) . rst) + (expand/df #`(#%app . #,(stx-map L #'rst)))] + [_ e] ; other literals + #;[es (stx-map L #'es)])) + ;; #:with res-ty (syntax-parse (substs #'(e_arg- ...) #'(X ...) #'τ_out) + ;; [((~literal #%plain-app) . rst) (expand/df #'(#%app . rst))] + ;; [other-ty #'other-ty]) + -------- + [⊢ res-e #;#,(substs #'(e_arg- ...) #'(x ...) #'e) ⇒ τ_out + #;#,(substs #'(e_arg- ...) #'(X ...) #'τ_out)]] + [(_ e_fn e_arg ... ~!) ≫ ; apply var +; #:do[(printf "applying (2) ~a\n" (stx->datum #'e_fn))] + [⊢ e_fn ≫ e_fn- ⇒ ty-fn] +; #:do[(printf "e_fn- ty: ~a\n" (stx->datum #'ty-fn))] + [⊢ e_fn ≫ _ ⇒ (~Π ([X : τ_inX] ...) τ_outX)] +; #:do[(printf "e_fn- no: ~a\n" (stx->datum #'e_fn-)) +; (printf "args: ~a\n" (stx->datum #'(e_arg ...)))] + ;; #:with e_fn- (syntax-parse #'e_fn* + ;; [((~literal #%plain-app) . rst) (expand/df #'(#%app . rst))] + ;; [other #'other]) + #:fail-unless (stx-length=? #'[τ_inX ...] #'[e_arg ...]) + (num-args-fail-msg #'e_fn #'[τ_inX ...] #'[e_arg ...]) + [⊢ e_arg ≫ e_argX- ⇒ ty-argX] ... ; typechecking args must be fold; do in 2 steps + #:do[(define (ev e) + (syntax-parse e +; [_ #:do[(printf "eval: ~a\n" (stx->datum e))] #:when #f #'(void)] + [(~or _:id +; ((~literal #%plain-lambda) . _) + (~= _ _) + ~Nat + ((~literal quote) _)) + e] + ;; handle nums + [((~literal #%plain-app) + (~and op (~or (~literal +-) (~literal zero?-))) + . args:nats) + #`#,(delta #'op #'args.vals)] + [((~literal #%plain-app) (~and f ((~literal #%plain-lambda) . b)) . rst) + (expand/df #`(#%app f . #,(stx-map ev #'rst)))] + [(x ...) + ;; #:do[(printf "t before: ~a\n" (typeof e)) + ;; (printf "t after: ~a\n" (typeof #`#,(stx-map ev #'(x ...))))] + (syntax-property #`#,(stx-map ev #'(x ...)) ': (typeof e))] + [_ e] ; other literals + #;[es (stx-map L #'es)]))] + #:with (ty-arg ...) + (stx-map + (λ (t) (ev (substs #'(e_argX- ...) #'(X ...) t))) + #'(ty-argX ...)) + #:with (e_arg- ...) (stx-map (λ (e t) (assign-type e t)) #'(e_argX- ...) #'(ty-arg ...)) + #:with (τ_in ... τ_out) + (stx-map + (λ (t) (ev (substs #'(e_arg- ...) #'(X ...) t))) + #'(τ_inX ... τ_outX)) + ;; #:do[(printf "vars: ~a\n" #'(X ...))] +; #:when (stx-andmap (λ (e t1 t2)(displayln (stx->datum e))(displayln (stx->datum t1)) (displayln (stx->datum t2)) (displayln (typecheck? t1 t2)) #;(typecheck? t1 t2)) #'(e_arg ...)#'(ty-arg ...) #'(τ_in ...)) + ;; #:do[(stx-map + ;; (λ (tx t) (printf "ty_in inst: \n~a\n~a\n" (stx->datum tx) (stx->datum t))) + ;; #'(τ_inX ...) #'(τ_in ...))] +; [⊢ e_arg ≫ _ ⇐ τ_in] ... +; #:do[(printf "res e2 =\n~a\n" (stx->datum #'(#%app- e_fn- e_arg- ...))) +; (printf "res t2 = ~a\n" (stx->datum (substs #'(e_arg- ...) #'(X ...) #'τ_out)))] + ;; #:with res-e (syntax-parse #'e_fn- + ;; [((~literal #%plain-lambda) . _) (expand/df #'(#%app e_fn- e_arg- ...))] + ;; [other #'(#%app- e_fn- e_arg- ...)]) + -------- + [⊢ (#%app- e_fn- e_arg- ...) ⇒ τ_out + #;#,(expand/df (substs #'(e_arg- ...) #'(X ...) #'τ_out))]]) + +(define-typed-syntax (ann e (~datum :) τ) ≫ + [⊢ e ≫ e- ⇐ τ] + -------- + [⊢ e- ⇒ τ]) + +;; (define-typed-syntax (if e1 e2 e3) ≫ +;; [⊢ e1 ≫ e1- ⇒ _] +;; [⊢ e2 ≫ e2- ⇒ ty] +;; [⊢ e3 ≫ e3- ⇒ _] +;; #:do[(displayln #'(e1 e2 e3))] +;; -------------- +;; [⊢ (#%app- void-) ⇒ ty]) + +;; top-level ------------------------------------------------------------------ +(define-syntax define-type-alias + (syntax-parser + [(_ alias:id τ);τ:any-type) + #'(define-syntax- alias + (make-variable-like-transformer #'τ))] + #;[(_ (f:id x:id ...) ty) + #'(define-syntax- (f stx) + (syntax-parse stx + [(_ x ...) + #:with τ:any-type #'ty + #'τ.norm]))])) + +(define-typed-syntax define + [(_ x:id (~datum :) τ e:expr) ≫ + [⊢ e ≫ e- ⇐ τ] + #:with y (generate-temporary #'x) + #:with y+props (transfer-props #'e- #'y #:except '(origin)) + -------- + [≻ (begin- + (define-syntax x (make-rename-transformer #'y+props)) + (define- y e-))]] + [(_ x:id e) ≫ + ;This won't work with mutually recursive definitions + [⊢ e ≫ e- ⇒ _] + #:with y (generate-temporary #'x) + #:with y+props (transfer-props #'e- #'y #:except '(origin)) + -------- + [≻ (begin- + (define-syntax x (make-rename-transformer #'y+props)) + (define- y e-))]] + #;[(_ (f [x (~datum :) ty] ... (~or (~datum →) (~datum ->)) ty_out) e ...+) ≫ + #:with f- (add-orig (generate-temporary #'f) #'f) + -------- + [≻ (begin- + (define-syntax- f + (make-rename-transformer (⊢ f- : (→ ty ... ty_out)))) + (define- f- + (stlc+lit:λ ([x : ty] ...) + (stlc+lit:ann (begin e ...) : ty_out))))]]) + + +;; ;; peano nums ----------------------------------------------------------------- +;; (define-typed-syntax Z +;; [_:id ≫ --- [⊢ 0 ⇒ Nat]]) + +;; (define-typed-syntax (S n) ≫ +;; [⊢ n ≫ n- ⇐ Nat] +;; ----------- +;; [⊢ (#%app- +- n- 1) ⇒ Nat]) +;; #;(define-typed-syntax (sub1 n) ≫ +;; [⊢ n ≫ n- ⇐ Nat] +;; #:do[(displayln #'n-)] +;; ----------- +;; [⊢ (#%app- -- n- 1) ⇒ Nat]) + +;; ;; generalized recursor over natural nums +;; ;; (cases dispatched in #%app) +;; (define- (nat-ind- P z s n) (#%app- void)) +;; (define-syntax nat-ind +;; (make-variable-like-transformer +;; (assign-type +;; #'nat-ind- +;; #'(Π ([P : (→ Nat #%type)] +;; [z : (P Z)] +;; [s : (Π ([k : Nat]) (→ (P k) (P (S k))))] +;; [n : Nat]) +;; (P n))))) + +;; #;(define-type-alias nat-ind +;; (λ ([P : (→ Nat #%type)] +;; [z : (P Z)] +;; [s : (Π ([k : Nat]) (→ (P k) (P (S k))))] +;; [n : Nat]) +;; #'(#%app- nat-ind- P z s n))) +;; #;(define-typed-syntax (nat-ind P z s n) ≫ +;; [⊢ P ≫ P- ⇐ (→ Nat #%type)] +;; ; [⊢ b ≫ b- ⇒ _] ; zero +;; ; [⊢ c ≫ c- ⇒ _] ; succ +;; ; [⊢ d ≫ d- ⇒ _] +;; [⊢ z ≫ z- ⇐ (P- Z)] ; zero +;; [⊢ s ≫ s- ⇐ (Π ([k : Nat]) (→ (P- k) (P- (S k))))] ; succ +;; [⊢ n ≫ n- ⇐ Nat] +;; #:with res (if (typecheck? #'n- (expand/df #'Z)) +;; #'z- +;; #'(s- (nat-ind P- z- s- (sub1 n-)))) +;; ---------------- +;; [⊢ res ⇒ (P- n-)]) +;; ; [≻ (P- d-)]) diff --git a/turnstile/examples/tests/dep2-tests.rkt b/turnstile/examples/tests/dep2-tests.rkt new file mode 100644 index 0000000..e3dc4bd --- /dev/null +++ b/turnstile/examples/tests/dep2-tests.rkt @@ -0,0 +1,237 @@ +#lang s-exp "../dep2.rkt" +(require "rackunit-typechecking.rkt") + +; Π → λ ∀ ≻ ⊢ ≫ ⇒ + +;; examples from Prabhakar's Proust paper + +;; the following examples to not require type-level eval +(check-type (λ ([x : *]) x) : (Π ([x : *]) *)) + +(typecheck-fail ((λ ([x : *]) x) (λ ([x : *]) x)) + #:verb-msg "expected *, given (Π ([x : *]) *)") + +(check-type (λ ([A : *][B : *]) + (λ ([x : A]) + (λ ([y : (→ A B)]) + (y x)))) + : (∀ (A B) (→ A (→ (→ A B) B)))) + +;; check alpha equiv +;; TODO: is this correct behavior? +(check-type (λ ([A : *][B : *]) + (λ ([x : A]) + (λ ([y : (→ A B)]) + (y x)))) + : (∀ (Y Z) (→ Y (→ (→ Y Z) Z)))) +(check-type (λ ([Y : *][Z : *]) + (λ ([x : Y]) + (λ ([y : (→ Y Z)]) + (y x)))) + : (∀ (A B) (→ A (→ (→ A B) B)))) +;; check infer direction +(check-type (λ (A B) (λ (x) (λ (y) (y x)))) + : (∀ (A B) (→ A (→ (→ A B) B)))) +(check-type (λ (A B) (λ (x) (λ (y) (y x)))) + : (∀ (X Y) (→ X (→ (→ X Y) Y)))) + +;; transitivity of implication -------------------- +(check-type (λ ([A : *][B : *][C : *]) + (λ ([f : (→ B C)]) + (λ ([g : (→ A B)]) + (λ ([x : A]) + (f (g x)))))) + : (∀ (A B C) (→ (→ B C) (→ (→ A B) (→ A C))))) +;; less currying +(check-type (λ ([A : *][B : *][C : *]) + (λ ([f : (→ B C)][g : (→ A B)]) + (λ ([x : A]) + (f (g x))))) + : (∀ (A B C) (→ (→ B C) (→ A B) (→ A C)))) +;; infer direction (no annotations) +(check-type (λ (A B C) (λ (f) (λ (g) (λ (x) (f (g x)))))) + : (∀ (A B C) (→ (→ B C) (→ (→ A B) (→ A C))))) +;; less currying +(check-type (λ (A B C) (λ (f g) (λ (x) (f (g x))))) + : (∀ (A B C) (→ (→ B C) (→ A B) (→ A C)))) +(check-type (λ (A B C) (λ (f g x) (f (g x)))) + : (∀ (A B C) (→ (→ B C) (→ A B) A C))) +(check-type (λ (A B C f g x) (f (g x))) + : (Π ([A : *][B : *][C : *][f : (→ B C)][g : (→ A B)][x : A]) C)) +(check-type (λ (A B C f g x) (f (g x))) + : (Π ([X : *][Y : *][Z : *][a : (→ Y Z)][b : (→ X Y)][c : X]) Z)) + +;; partial annotations - outer lam with no annotations +(check-type (λ (A B C) + (λ (f g) + (λ ([x : A]) + (f (g x))))) + : (∀ (A B C) (→ (→ B C) (→ A B) (→ A C)))) +(check-type (λ (A B C) + (λ ([f : (→ B C)][g : (→ A B)]) + (λ ([x : A]) + (f (g x))))) + : (∀ (A B C) (→ (→ B C) (→ A B) (→ A C)))) +(typecheck-fail (ann + (λ (A B C) + (λ (f g) + (λ ([x : C]) + (f (g x))))) + : (∀ (A B C) (→ (→ B C) (→ A B) (→ A C)))) + #:with-msg "expected A, given C") +;; partial annotations - inner lam with no annotations +(check-type (λ ([A : *][B : *][C : *]) + (λ (f g) + (λ (x) + (f (g x))))) + : (∀ (A B C) (→ (→ B C) (→ A B) (→ A C)))) +(check-type (λ ([A : *][B : *][C : *]) + (λ ([f : (→ B C)]) + (λ (g) + (λ (x) + (f (g x)))))) + : (∀ (A B C) (→ (→ B C) (→ (→ A B) (→ A C))))) +(check-type (λ ([A : *][B : *][C : *]) + (λ ([f : (→ B C)]) + (λ (g) + (λ ([x : A]) + (f (g x)))))) + : (∀ (A B C) (→ (→ B C) (→ (→ A B) (→ A C))))) +(check-type (λ ([A : *][B : *][C : *]) + (λ ([f : (→ B C)]) + (λ ([g : (→ A B)]) + (λ (x) + (f (g x)))))) + : (∀ (A B C) (→ (→ B C) (→ (→ A B) (→ A C))))) + +;; Peirce's Law (doesnt work) +(typecheck-fail (ann + (λ ([A : *][B : *][C : *]) + (λ ([f : (→ (→ A B) A)]) + (λ ([g : (→ A B)]) ; need concrete (→ A B) (not in type) + (f g)))) + : (∀ (A B C) (→ (→ (→ A B) A) A))) + #:verb-msg "expected (∀ (A B C) (→ (→ (→ A B) A) A)), given (Π ((A : *) (B : *) (C : *)) (Π ((f : (→ (→ A B) A))) (Π ((g : (→ A B))) A)))") + +;; booleans ------------------------------------------------------------------- + +;; Bool base type +(define-type-alias Bool (∀ (A) (→ A A A))) + +;; Bool terms +(define T (λ ([A : *]) (λ ([x : A][y : A]) x))) +(define F (λ ([A : *]) (λ ([x : A][y : A]) y))) +(check-type T : Bool) +(check-type F : Bool) +;; check infer case +(define T2 (λ ([bool : *]) (λ ([x : bool][y : bool]) x))) +(define F2 (λ ([bool : *]) (λ ([x : bool][y : bool]) y))) +(check-type T2 : Bool) +(check-type F2 : Bool) +(define T3 : Bool (λ (bool) (λ (x y) x))) +(define F3 : Bool (λ (bool) (λ (x y) y))) +(check-type T3 : Bool) +(check-type F3 : Bool) + +;; defining `and` requires instantiating polymorphic types +; (define and (λ ([x : Bool][y : Bool]) ((x Bool) y F))) +;(check-type and : (→ Bool Bool Bool)) + +;; ;; And type constructor, ie type-level fn +;; (define-type-alias And +;; (λ ([A : *][B : *]) +;; (∀ (C) (→ (→ A B C) C)))) +;; (check-type And : (→ * * *)) + +;; ;; And type intro +;; (define ∧ +;; (λ ([A : *][B : *]) +;; (λ ([x : A][y : B]) +;; (λ ([C : *]) +;; (λ ([f : (→ A B C)]) +;; (f x y)))))) +;; (check-type ∧ : (∀ (A B) (→ A B (And A B)))) + +;; ;; And type elim +;; (define proj1 +;; (λ ([A : *][B : *]) +;; (λ ([e∧ : (And A B)]) +;; ((e∧ A) (λ ([x : A][y : B]) x))))) +;; (define proj2 +;; (λ ([A : *][B : *]) +;; (λ ([e∧ : (And A B)]) +;; ((e∧ B) (λ ([x : A][y : B]) y))))) +;; ;; bad proj2: (e∧ A) should be (e∧ B) +;; (typecheck-fail +;; (λ ([A : *][B : *]) +;; (λ ([e∧ : (And A B)]) +;; ((e∧ A) (λ ([x : A][y : B]) y)))) +;; #:verb-msg +;; "expected (→ A B C), given (Π ((x : A) (y : B)) B)") +;; (check-type proj1 : (∀ (A B) (→ (And A B) A))) +;; (check-type proj2 : (∀ (A B) (→ (And A B) B))) + +;; ;((((conj q) p) (((proj2 p) q) a)) (((proj1 p) q) a))))) +;; (define and-commutes +;; (λ ([A : *][B : *]) +;; (λ ([e∧ : (And A B)]) +;; ((∧ B A) ((proj2 A B) e∧) ((proj1 A B) e∧))))) +;; ;; bad and-commutes, dont flip A and B: (→ (And A B) (And A B)) +;; (typecheck-fail +;; (λ ([A : *][B : *]) +;; (λ ([e∧ : (And A B)]) +;; ((∧ A B) ((proj2 A B) e∧) ((proj1 A B) e∧)))) +;; #:verb-msg +;; "#%app: type mismatch: expected A, given C") ; TODO: err msg should be B not C? +;; (check-type and-commutes : (∀ (A B) (→ (And A B) (And B A)))) + +;; ;; nats ----------------------------------------------------------------------- +;; (define-type-alias nat (∀ (A) (→ A (→ A A) A))) + +;; (define-type-alias z (λ ([Ty : *]) (λ ([zero : Ty][succ : (→ Ty Ty)]) zero))) +;; (define-type-alias s (λ ([n : nat]) +;; (λ ([Ty : *]) +;; (λ ([zero : Ty][succ : (→ Ty Ty)]) +;; (succ ((n Ty) zero succ)))))) +;; (check-type z : nat) +;; (check-type s : (→ nat nat)) + +;; (define-type-alias one (s z)) +;; (define-type-alias two (s (s z))) +;; (check-type one : nat) +;; (check-type two : nat) + +;; (define-type-alias plus +;; (λ ([x : nat][y : nat]) +;; ((x nat) y s))) +;; (check-type plus : (→ nat nat nat)) + +;; ;; equality ------------------------------------------------------------------- + +;; (check-type (eq-refl one) : (= one one)) +;; (check-type (eq-refl one) : (= (s z) one)) +;; (check-type (eq-refl two) : (= (s (s z)) two)) +;; (check-type (eq-refl two) : (= (s one) two)) +;; (check-type (eq-refl two) : (= two (s one))) +;; (check-type (eq-refl two) : (= (s (s z)) (s one))) +;; (check-type (eq-refl two) : (= (plus one one) two)) +;; (check-not-type (eq-refl two) : (= (plus one one) one)) + +;; ;; symmetry of = +;; (check-type +;; (λ ([A : *][B : *]) +;; (λ ([e : (= A B)]) +;; (eq-elim A (λ ([W : *]) (= W A)) (eq-refl A) B e))) +;; : (∀ (A B) (→ (= A B) (= B A)))) +;; (check-not-type +;; (λ ([A : *][B : *]) +;; (λ ([e : (= A B)]) +;; (eq-elim A (λ ([W : *]) (= W A)) (eq-refl A) B e))) +;; : (∀ (A B) (→ (= A B) (= A B)))) + +;; ;; transitivity of = +;; (check-type +;; (λ ([X : *][Y : *][Z : *]) +;; (λ ([e1 : (= X Y)][e2 : (= Y Z)]) +;; (eq-elim Y (λ ([W : *]) (= X W)) e1 Z e2))) +;; : (∀ (A B C) (→ (= A B) (= B C) (= A C))))