remove dep example

This commit is contained in:
Stephen Chang 2017-08-14 13:48:53 -04:00
parent 7c841dc750
commit 441ec0e5d7
3 changed files with 0 additions and 534 deletions

View File

@ -1,334 +0,0 @@
#lang turnstile/lang
; Π λ ≻ ⊢ ≫ → ∧ (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)
(define-base-type Nat)
(define-internal-type-constructor )
(define-internal-binding-type )
;; TODO: how to do Type : Type
(define-typed-syntax (Π ([X:id : τ_in] ...) τ_out)
[[X X- : τ_in] ... [τ_out τ_out- _][τ_in τ_in- _] ...]
-------
[ (∀- (X- ...) (→- τ_in- ... τ_out-)) #,(expand/df #'#%type)])
;; abbrevs for Π
(define-simple-macro ( τ_in ... τ_out)
#:with (X ...) (generate-temporaries #'(τ_in ...))
(Π ([X : τ_in] ...) τ_out))
(define-simple-macro ( (X ...) τ)
(Π ([X : #%type] ...) τ))
;; ~Π pattern expander
(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: add case with expected type + annotations
;; - check that annotations match expected types
(define-typed-syntax λ
[(_ ([x:id : τ_in] ...) e)
[[x x- : τ_in] ... [e e- τ_out][τ_in τ_in- _] ...]
-------
[ (λ- (x- ...) e-) (Π ([x- : τ_in-] ...) τ_out)]]
[(_ (y:id ...) e) ( ([x:id : τ_in] ...) τ_out)
[[x x- : τ_in] ... #,(substs #'(x ...) #'(y ...) #'e) e- τ_out]
---------
[ (λ- (x- ...) e-)]])
;; 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 ...) ; 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 :) τ:type e:expr)
;[⊢ e ≫ e- ⇐ τ.norm]
#:with y (generate-temporary #'x)
--------
[ (begin-
(define-syntax x (make-rename-transformer ( y : τ.norm)))
(define- y (ann e : τ.norm)))]]
[(_ 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-)])

View File

@ -1,53 +0,0 @@
#lang s-exp "../dep.rkt"
(require "rackunit-typechecking.rkt")
; Π → λ ∀ ≻ ⊢ ≫ ⇒
;; examples from Prabhakar's Proust paper
;; Peano nums -----------------------------------------------------------------
(define-type-alias nat-rec
(λ ([C : *])
(λ ([zc : C][sc : ( C C)])
(λ ([n : Nat])
(nat-ind (λ ([x : Nat]) C)
zc
(λ ([x : Nat]) sc)
n)))))
;(check-type nat-rec : (∀ (C) (→ C (→ C C) (→ Nat C))))
(define-type-alias plus
(λ ([n : Nat])
(((nat-rec ( Nat Nat))
(λ ([m : Nat]) m)
(λ ([pm : ( Nat Nat)])
(λ ([x : Nat])
(S (pm x)))))
n)))
(check-type plus : ( Nat ( Nat Nat)))
;(check-type ((plus Z) Z) : Nat -> 0)
;(check-type ((plus (S Z)) (S Z)) : Nat -> 2)
;(check-type ((plus (S Z)) Z) : Nat -> 1)
;; TODO: implement nat-ind reductions
;; plus zero left
;; (check-type
;; (λ ([n : Nat]) (eq-refl n))
;; : (Π ([n : Nat]) (= ((plus Z) n) n)))
;; (check-type
;; (λ ([n : Nat])
;; (nat-ind (λ ([m : Nat]) (= ((plus m) Z) m))
;; (eq-refl Z)
;; (λ ([k : Nat])
;; (λ ([p : (= ((plus k) Z) k)])
;; (eq-elim ((plus k) Z)
;; (λ ([W : Nat]) (= (S ((plus k) Z)) (S W)))
;; (eq-refl (S ((plus k) Z)))
;; k
;; p)))
;; n))
;; : (Π ([n : Nat]) (= ((plus n) Z) n)))

View File

@ -1,147 +0,0 @@
#lang s-exp "../dep.rkt"
(require "rackunit-typechecking.rkt")
; Π → λ ∀ ≻ ⊢ ≫ ⇒
;; examples from Prabhakar's Proust paper
(check-type (λ ([x : *]) x) : (Π ([x : *]) *))
(typecheck-fail ((λ ([x : *]) x) (λ ([x : *]) x))
#:verb-msg "expected *, given (Π ([x : *]) *)")
;; 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)))))
; unnested
(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))))
;; 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 g)
(λ (x)
(f (g x)))))
: ( (A B C) ( ( B C) ( A B) ( A C))))
;; TODO: partial annotations
;; booleans -------------------------------------------------------------------
;; Bool 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)
(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))))