add bool and nat examples; start eq-refl; need to fix app/eval
This commit is contained in:
Stephen Chang
parent
4e80959d12
commit
31bc8cebec
|
|
@ -7,7 +7,8 @@
|
|||
|
||||
(provide (rename-out [#%type *])
|
||||
Π → ∀
|
||||
;; = eq-refl eq-elim
|
||||
= eq-refl
|
||||
;;eq-elim
|
||||
;; Nat Z S nat-ind
|
||||
λ
|
||||
#%app ann
|
||||
|
|
@ -37,6 +38,8 @@
|
|||
(define old-relation (current-typecheck-relation))
|
||||
(current-typecheck-relation
|
||||
(lambda (t1 t2)
|
||||
;; (pretty-print (stx->datum t1))
|
||||
;; (pretty-print (stx->datum 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
|
||||
|
|
@ -53,7 +56,7 @@
|
|||
;; TODO: check that τ_in and τ_out have #%type?
|
||||
[[X ≫ X- : τ_in] ... ⊢ [τ_out ≫ τ_out- ⇒ _] [τ_in ≫ τ_in- ⇒ _] ...]
|
||||
-------
|
||||
[⊢ (∀- (X- ...) (→- τ_in- ... τ_out-)) ⇒ #,Type #;#%type])
|
||||
[⊢ (∀- (X- ...) (→- τ_in- ... τ_out-)) ⇒ #%type])
|
||||
|
||||
;; abbrevs for Π
|
||||
(define-simple-macro (→ τ_in ... τ_out)
|
||||
|
|
@ -72,20 +75,20 @@
|
|||
[(_ ([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)])
|
||||
;; 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-) ⇒ #%type])
|
||||
|
||||
;; (define-typed-syntax (eq-refl e) ≫
|
||||
;; [⊢ e ≫ e- ⇒ _]
|
||||
;; ----------
|
||||
;; [⊢ (#%app- void-) ⇒ (= e- e-)])
|
||||
(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]
|
||||
|
|
@ -145,15 +148,29 @@
|
|||
;; [(~literal +-) (stx+ args)]
|
||||
;; [(~literal zero?-) (apply zero? (stx->nats args))])))
|
||||
|
||||
;; TODO: fix orig after subst
|
||||
(define-syntax app/eval
|
||||
(syntax-parser
|
||||
;; TODO: apply to only lambda args or all args?
|
||||
[(_ (~and f ((~literal #%plain-lambda) (x ...) e)) e_arg ...)
|
||||
;; TODO: need to replace all #%app- in this result with app/eval again
|
||||
;; and then re-expand
|
||||
(substs #'(e_arg ...) #'(x ...) #'e)]
|
||||
[(_ f . args)
|
||||
#'(#%app- f . args)]))
|
||||
|
||||
;; TODO: fix orig after subst
|
||||
(define-typed-syntax #%app
|
||||
[(_ e_fn e_arg ...) ≫
|
||||
; #:do[(printf "applying (1) ~a\n" (stx->datum #'e_fn))]
|
||||
; [⊢ e_fn ≫ (~and e_fn- (_ (x:id ...) e ~!)) ⇒ (~Π ([X : τ_inX] ...) τ_outX)]
|
||||
[⊢ e_fn ≫ e_fn- ⇒ (~Π ([X : τ_in] ...) τ_out)]
|
||||
; #:do[(printf "applying (1) ~a\n" (stx->datum #'e_fn-))]
|
||||
#: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]])
|
||||
[⊢ (app/eval e_fn- e_arg- ...) ⇒ #,(substs #'(e_arg- ...) #'(X ...) #'τ_out)]])
|
||||
|
||||
#;(define-typed-syntax #%app
|
||||
[(_ e_fn e_arg ...) ≫ ; apply lambda
|
||||
|
|
@ -299,6 +316,7 @@
|
|||
;; [⊢ (#%app- void-) ⇒ ty])
|
||||
|
||||
;; top-level ------------------------------------------------------------------
|
||||
;; TODO: shouldnt need define-type-alias, should be same as define
|
||||
(define-syntax define-type-alias
|
||||
(syntax-parser
|
||||
[(_ alias:id τ);τ:any-type)
|
||||
|
|
|
|||
|
|
@ -116,7 +116,9 @@
|
|||
;; booleans -------------------------------------------------------------------
|
||||
|
||||
;; Bool base type
|
||||
;; TODO: use define instead of define-type-alias
|
||||
(define-type-alias Bool (∀ (A) (→ A A A)))
|
||||
(check-type Bool : *)
|
||||
|
||||
;; Bool terms
|
||||
(define T (λ ([A : *]) (λ ([x : A][y : A]) x)))
|
||||
|
|
@ -124,98 +126,120 @@
|
|||
(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)))
|
||||
(define T2 (λ ([abool : *]) (λ ([x : abool][y : abool]) x)))
|
||||
(define F2 (λ ([abool : *]) (λ ([x : abool][y : abool]) y)))
|
||||
(check-type T2 : Bool)
|
||||
(check-type F2 : Bool)
|
||||
(define T3 : Bool (λ (bool) (λ (x y) x)))
|
||||
(define F3 : Bool (λ (bool) (λ (x y) y)))
|
||||
(define T3 : Bool (λ (abool) (λ (x y) x)))
|
||||
(define F3 : Bool (λ (abool) (λ (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))
|
||||
(define and (λ ([x : Bool][y : Bool]) ((x Bool) y F)))
|
||||
(check-type and : (→ Bool Bool Bool))
|
||||
(define or (λ ([x : Bool][y : Bool]) ((x Bool) T y)))
|
||||
(check-type or : (→ Bool Bool Bool))
|
||||
(define not (λ ([x : Bool]) ((x Bool) F T)))
|
||||
(check-type not : (→ 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 constructor, ie type-level fn
|
||||
(define-type-alias And
|
||||
(λ ([P : *][Q : *])
|
||||
(∀ (C) (→ (→ P Q 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 intro (logical conj)
|
||||
(define ∧
|
||||
(λ ([P : *][Q : *])
|
||||
(λ ([p : P][q : Q])
|
||||
(λ ([C : *])
|
||||
(λ ([f : (→ P Q C)])
|
||||
(f p q))))))
|
||||
(check-type ∧ : (∀ (P Q) (→ P Q (And P Q))))
|
||||
|
||||
;; ;; 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)))
|
||||
;; `And` type elim
|
||||
(define proj1
|
||||
(λ ([P : *][Q : *])
|
||||
(λ ([e : (And P Q)])
|
||||
((e P) (λ ([x : P][y : Q]) x)))))
|
||||
(define proj2
|
||||
(λ ([P : *][Q : *])
|
||||
(λ ([e : (And P Q)])
|
||||
((e Q) (λ ([x : P][y : Q]) y)))))
|
||||
;; bad proj2: (e A) should be (e B)
|
||||
(typecheck-fail
|
||||
(λ ([P : *][Q : *])
|
||||
(λ ([e : (And P Q)])
|
||||
((e P) (λ ([x : P][y : Q]) y))))
|
||||
#:verb-msg
|
||||
"expected (→ P Q C), given (Π ((x : P) (y : Q)) Q)")
|
||||
(check-type proj1 : (∀ (P Q) (→ (And P Q) P)))
|
||||
(check-type proj2 : (∀ (P Q) (→ (And P Q) Q)))
|
||||
|
||||
;; ;((((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))))
|
||||
;; proj1, no annotations
|
||||
(check-type (λ (P Q) (λ (e) ((e P) (λ (x y) x))))
|
||||
: (∀ (P Q) (→ (And P Q) P)))
|
||||
;; proj2, no annotations
|
||||
(check-type (λ (P Q) (λ (e) ((e Q) (λ (x y) y))))
|
||||
: (∀ (P Q) (→ (And P Q) Q)))
|
||||
(typecheck-fail (ann (λ (P Q) (λ (e) ((e Q) (λ (x y) x))))
|
||||
: (∀ (P Q) (→ (And P Q) Q)))
|
||||
#:with-msg "expected C, given P") ; TODO: err msg, fix orig
|
||||
(typecheck-fail (ann (λ (P Q) (λ (e) ((e P) (λ (x y) y))))
|
||||
: (∀ (P Q) (→ (And P Q) Q)))
|
||||
#:with-msg "expected C, given Q") ; TODO: err msg
|
||||
|
||||
;; ;; nats -----------------------------------------------------------------------
|
||||
;; (define-type-alias nat (∀ (A) (→ A (→ A A) A)))
|
||||
;((((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 P, given C") ; TODO: err msg
|
||||
(check-type and-commutes : (∀ (A B) (→ (And A B) (And B 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))
|
||||
;; nats -----------------------------------------------------------------------
|
||||
(define-type-alias nat (∀ (A) (→ A (→ A A) A)))
|
||||
(check-type 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 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 plus
|
||||
;; (λ ([x : nat][y : nat])
|
||||
;; ((x nat) y s)))
|
||||
;; (check-type plus : (→ nat nat nat))
|
||||
(define-type-alias one (s z))
|
||||
(define-type-alias two (s (s z)))
|
||||
(check-type one : nat)
|
||||
(check-type two : nat)
|
||||
|
||||
;; ;; equality -------------------------------------------------------------------
|
||||
(define-type-alias plus
|
||||
(λ ([x : nat][y : nat])
|
||||
((x nat) y s)))
|
||||
(check-type plus : (→ nat nat nat))
|
||||
(check-type (λ (x y) ((x nat) y s)) : (→ nat nat nat))
|
||||
|
||||
;; (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))
|
||||
;; equality -------------------------------------------------------------------
|
||||
|
||||
(check-type (eq-refl one) : (= one one))
|
||||
(typecheck-fail (ann (eq-refl one) : (= two one))
|
||||
#:verb-msg "expected (= two one), given (= 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)))
|
||||
;; the following example requires recursive expansion after eval/app
|
||||
;(check-type (eq-refl two) : (= (plus one one) two))
|
||||
;(check-not-type (eq-refl two) : (= (plus one one) one))
|
||||
|
||||
;; ;; symmetry of =
|
||||
;; (check-type
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user