dep-tests.rkt (3035B)
1 #lang s-exp "../dep.rkt" 2 (require "rackunit-typechecking.rkt") 3 4 ; Π → λ ∀ ≻ ⊢ ≫ ⇒ 5 6 ;; examples from Prabhakar's Proust paper 7 8 (check-type (λ ([x : *]) x) : (Π ([x : *]) *)) 9 (typecheck-fail ((λ ([x : *]) x) (λ ([x : *]) x)) 10 #:verb-msg "expected *, given (Π ([x : *]) *)") 11 12 ;; transitivity of implication 13 (check-type (λ ([A : *][B : *][C : *]) 14 (λ ([f : (→ B C)]) 15 (λ ([g : (→ A B)]) 16 (λ ([x : A]) 17 (f (g x)))))) 18 : (∀ (A B C) (→ (→ B C) (→ (→ A B) (→ A C))))) 19 ; unnested 20 (check-type (λ ([A : *][B : *][C : *]) 21 (λ ([f : (→ B C)][g : (→ A B)]) 22 (λ ([x : A]) 23 (f (g x))))) 24 : (∀ (A B C) (→ (→ B C) (→ A B) (→ A C)))) 25 ;; no annotations 26 (check-type (λ (A B C) 27 (λ (f) (λ (g) (λ (x) 28 (f (g x)))))) 29 : (∀ (A B C) (→ (→ B C) (→ (→ A B) (→ A C))))) 30 (check-type (λ (A B C) 31 (λ (f g) 32 (λ (x) 33 (f (g x))))) 34 : (∀ (A B C) (→ (→ B C) (→ A B) (→ A C)))) 35 ;; TODO: partial annotations 36 37 ;; booleans ------------------------------------------------------------------- 38 39 ;; Bool type 40 (define-type-alias Bool (∀ (A) (→ A A A))) 41 42 ;; Bool terms 43 (define T (λ ([A : *]) (λ ([x : A][y : A]) x))) 44 (define F (λ ([A : *]) (λ ([x : A][y : A]) y))) 45 (check-type T : Bool) 46 (check-type F : Bool) 47 (define and (λ ([x : Bool][y : Bool]) ((x Bool) y F))) 48 (check-type and : (→ Bool Bool Bool)) 49 50 ;; And type constructor, ie type-level fn 51 (define-type-alias And 52 (λ ([A : *][B : *]) 53 (∀ (C) (→ (→ A B C) C)))) 54 (check-type And : (→ * * *)) 55 56 ;; And type intro 57 (define ∧ 58 (λ ([A : *][B : *]) 59 (λ ([x : A][y : B]) 60 (λ ([C : *]) 61 (λ ([f : (→ A B C)]) 62 (f x y)))))) 63 (check-type ∧ : (∀ (A B) (→ A B (And A B)))) 64 65 ;; And type elim 66 (define proj1 67 (λ ([A : *][B : *]) 68 (λ ([e∧ : (And A B)]) 69 ((e∧ A) (λ ([x : A][y : B]) x))))) 70 (define proj2 71 (λ ([A : *][B : *]) 72 (λ ([e∧ : (And A B)]) 73 ((e∧ B) (λ ([x : A][y : B]) y))))) 74 ;; bad proj2: (e∧ A) should be (e∧ B) 75 (typecheck-fail 76 (λ ([A : *][B : *]) 77 (λ ([e∧ : (And A B)]) 78 ((e∧ A) (λ ([x : A][y : B]) y)))) 79 #:verb-msg 80 "expected (→ A B C), given (Π ((x : A) (y : B)) B)") 81 (check-type proj1 : (∀ (A B) (→ (And A B) A))) 82 (check-type proj2 : (∀ (A B) (→ (And A B) B))) 83 84 ;((((conj q) p) (((proj2 p) q) a)) (((proj1 p) q) a))))) 85 (define and-commutes 86 (λ ([A : *][B : *]) 87 (λ ([e∧ : (And A B)]) 88 ((∧ B A) ((proj2 A B) e∧) ((proj1 A B) e∧))))) 89 ;; bad and-commutes, dont flip A and B: (→ (And A B) (And A B)) 90 (typecheck-fail 91 (λ ([A : *][B : *]) 92 (λ ([e∧ : (And A B)]) 93 ((∧ A B) ((proj2 A B) e∧) ((proj1 A B) e∧)))) 94 #:verb-msg 95 "#%app: type mismatch: expected A, given C") ; TODO: err msg should be B not C? 96 (check-type and-commutes : (∀ (A B) (→ (And A B) (And B A))))