start over with dep2; basic lam/app working; no instantiation
This commit is contained in:
Stephen Chang
parent
ac832bced0
commit
4e80959d12
|
|
@ -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 ...)))]
|
||||
|
|
|
|||
389
turnstile/examples/dep2.rkt
Normal file
389
turnstile/examples/dep2.rkt
Normal file
|
|
@ -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-)])
|
||||
237
turnstile/examples/tests/dep2-tests.rkt
Normal file
237
turnstile/examples/tests/dep2-tests.rkt
Normal file
|
|
@ -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))))
|
||||
Loading…
Reference in New Issue
Block a user