add dep-ind example with define-datatype

This commit is contained in:
Stephen Chang 2017-08-16 12:39:28 -04:00
parent 7fc8bd8c15
commit 804c82bf24
3 changed files with 834 additions and 2 deletions

View File

@ -1,7 +1,7 @@
#lang turnstile/lang
; second attempt at a basic dependently-typed calculus
; initially copied from dep.rkt
; a basic dependently-typed calculus
; extends dep.rkt
; Π λ ≻ ⊢ ≫ → ∧ (bidir ⇒ ⇐) τ⊑

View File

@ -0,0 +1,695 @@
#lang turnstile/lang
; a basic dependently-typed calculus
; - with inductive datatypes
; Π λ ≻ ⊢ ≫ → ∧ (bidir ⇒ ⇐) τ⊑
(provide (rename-out [#%type *])
Π
= eq-refl eq-elim
; Nat (rename-out [Zero Z][Succ S]) nat-ind #;nat-rec
λ (rename-out [app #%app]) ann
define define-type-alias
)
;; TODO:
;; - map #%datum to S and Z
;; - rename define-type-alias to define
;; - add "assistant" part
;; - provide match and match/lambda so nat-ind can be fn
;; - eg see https://gist.github.com/AndrasKovacs/6769513
;; - add dependent existential
;; - remove debugging code?
;; #;(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
;; set Type : Type
;; alternatively, could define new base type Type,
;; and make #%type typecheck with Type
(begin-for-syntax
(define debug? #f)
(define type-eq-debug? #f)
(define debug-match? #f)
;; 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)
(when type-eq-debug?
(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)) ; assign 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- #%type] [τ_in τ_in- #%type] ...]
-------
[ (∀- (X- ...) (→- τ_in- ... τ_out-)) #%type])
;; abbrevs for Π
;; (→ τ_in τ_out) == (Π (unused : τ_in) τ_out)
(define-simple-macro ( τ_in ... τ_out)
#:with (X ...) (generate-temporaries #'(τ_in ...))
(Π ([X : τ_in] ...) τ_out))
;; (∀ (X) τ) == (∀ ([X : #%type]) τ)
(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- ty]
[ t2 t2- ty]
;; #:do [(printf "t1: ~a\n" (stx->datum #'t1-))
;; (printf "t2: ~a\n" (stx->datum #'t2-))]
; [t1- τ= t2-]
---------------------
[ (=- t1- t2-) #%type])
;; Q: what is the operational meaning of eq-refl?
(define-typed-syntax (eq-refl e)
[ e e- _]
----------
[ (#%app- void-) (= e- e-)])
;; eq-elim: t : T
;; P : (T -> Type)
;; pt : (P t)
;; w : T
;; peq : (= t w)
;; -> (P w)
(define-typed-syntax (eq-elim t P pt w peq)
[ t t- ty]
[ P P- ( ty #%type)]
[ pt pt- (app P- t-)]
[ w w- ty]
[ peq peq- (= t- w-)]
--------------
[ pt- (app 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))])))
;; TODO: fix orig after subst, for err msgs
;; app/eval should not try to ty check anymore
(define-syntax app/eval
(syntax-parser
#;[(_ f . args) #:do[(printf "app/evaling ")
(printf "f: ~a\n" (stx->datum #'f))
(printf "args: ~a\n" (stx->datum #'args))]
#:when #f #'void]
[(_ f:id (_ matcher) (_ _ . args))
#:with (_ m/d . _) (local-expand #'(#%app match/delayed 'dont 'care) 'expression null)
#:when (free-identifier=? #'m/d #'f)
;; TODO: need to attach type?
#'(matcher . args)]
;; TODO: apply to only lambda args or all args?
[(_ (~and f ((~literal #%plain-lambda) (x ...) e)) e_arg ...)
#:do[(when debug?
(printf "apping: ~a\n" (stx->datum #'f))
(printf "args\n")
(pretty-print (stx->datum #'(e_arg ...)))
(printf "expected type\n")
(pretty-print (stx->datum (typeof this-syntax))))]
; #:with (~Π ([X : _] ...) τ_out) (typeof #'f) ; must re-subst in type
;; TODO: need to replace all #%app- in this result with app/eval again
;; and then re-expand
; #:with ((~literal #%plain-app) newf . newargs) #'e
; #:do[(displayln #'newf)(displayln #'newargs)(displayln (stx-car #'e+))]
#:with r-app (datum->syntax (if (identifier? #'e) #'e (stx-car #'e)) '#%app)
;; TODO: is this assign-type needed only for tests?
;; eg, see id tests in dep2-peano.rkt
#:with ty (typeof this-syntax)
#:with e-inst (substs #'(app/eval e_arg ...) #'(r-app x ...) #'e free-identifier=?)
;; some apps may not have type (eg in internal reps)
#:with e+ (if (syntax-e #'ty) (assign-type #'e-inst #'ty) #'e-inst)
#:do[(when debug?
(displayln "res:--------------------")
(pretty-print (stx->datum #'e+))
;; (displayln "actual type:")
;; (pretty-print (stx->datum (typeof #'e+)))
;; (displayln "new type:")
;; (pretty-print (stx->datum (substs #'(e_arg ...) #'(X ...) (typeof #'e+))))
;; (displayln "res expanded:------------------------")
;; (pretty-print
;; (stx->datum (local-expand (substs #'(e_arg ...) #'(x ...) #'e) 'expression null)))
(displayln "res app/eval re-expanding-----------------------"))]
#:with ((~literal let-values) () ((~literal let-values) () e++))
(local-expand
#'(let-syntax (#;[app (make-rename-transformer #'app/eval)]
#;[x (make-variable-like-transformer #'e_arg)]) e+)
'expression null)
#:do[(when debug?
(pretty-print (stx->datum #'e++))
; (pretty-print (stx->datum (typeof #'e++)))
#;(local-expand
#'(let-syntax ([app (make-rename-transformer #'app/eval)]
#;[x (make-variable-like-transformer #'e_arg)]) e+)
'expression null))]
#'e++ #;(substs #'(e_arg ...) #'(x ...) #'e)]
[(_ f . args)
#:do[(when debug?
(printf "not apping\n")
(pretty-print (stx->datum #'f))
(displayln "args")
(pretty-print (stx->datum #'args)))]
#:with f+ (expand/df #'f)
#:with args+ (stx-map expand/df #'args)
;; TODO: need to attach type?
; #:with ty (typeof this-syntax)
(syntax-parse #'f+
[((~literal #%plain-lambda) . _)
#'(app/eval f+ . args+)]
[_
#'(#%app- f+ . args+)])]))
;; TODO: fix orig after subst
(define-typed-syntax app
;; matching, ; TODO: where to put this?
#;[(_ f:id . args)
#:with (_ m/d . _) (local-expand #'(match/delayed 1 2 3 4) 'expression null)
#:when (free-identifier=? #'m/d #'f)
------------
[ (match/nat . args)]]
[(_ e_fn e_arg ...)
#:do[(when debug?
(displayln "TYPECHECKING")
(pretty-print (stx->datum this-syntax)))]
; #: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/eval e_fn- e_arg- ...) #,(substs #'(e_arg- ...) #'(X ...) #'τ_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 ------------------------------------------------------------------
;; TODO: shouldnt need define-type-alias, should be same as define
(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 -----------------------------------------------------------------
(provide define-datatype)
(struct TmpTy ())
(struct TmpTy2 ())
(define-typed-syntax define-datatype
[(_ Name (~datum :) kind [C:id (~datum :) TY #;(~and TY (ar tyin ... tyout))] ...)
; need to expand `TY` but `Name` is still unbound so use tmp id
#:with (TY* ...) (subst #'TmpTy #'Name #'(TY ...))
[ TY* TY- #%type] ...
#:with (_ TmpTy+) (local-expand #'(TmpTy) 'expression null)
;; TODO: ignoring X ... for now
;; TODO: replace TmpTy in origs of τ_in ... τ_out
#:with (( ([X : τ_in] ...) τ_out) ...)
(subst #'Name #'TmpTy+ #'(TY- ...) free-id=?)
#:with (C* ...) (generate-temporaries #'(C ...))
#:with (C** ...) (generate-temporaries #'(C ...))
#:with (Ccase ...) (generate-temporaries #'(C ...))
#:with (C- ...) (generate-temporaries #'(C ...))
;; Can I just use X instead of fld?
#:with ((fld ...) ...) (stx-map generate-temporaries #'((τ_in ...) ...))
#:with ((fld- ...) ...) (stx-map generate-temporaries #'((τ_in ...) ...))
#:with elim-Name (format-id #'Name "elim-~a" #'Name)
#:with match-Name (format-id #'Name "match-~a" #'Name)
#:with match-Name/delayed (format-id #'Name "match-~a/delayed" #'Name)
--------
[ (begin-
(define-base-type Name)
(struct C* (fld ...) #:transparent) ...
(define-typed-syntax C
[:id --- [ C* TY]]
[(_ fld ...)
[ fld fld- τ_in] ...
--------
[ (C* fld- ...) τ_out]]) ...
(define-typed-syntax (elim-Name x P C* ...)
[ x x- Name]
[ P P- ( Name #%type)] ; prop / motive
; [⊢ z ≫ z- ⇐ (app P- Zero)] ; zero
; [⊢ C ≫ C- ⇐ (Π ([k : Nat]) (→ (app P- k) (app P- (Succ k))))] ; succ
;; TODO: the (app P- fld) ... is wrong, should only include recur args
;; for now, each case consumes the number of args for each C,
;; and then an IH for each arg
[ C* C- (Π ([fld : τ_in] ...) ( (app P- fld) ... (app P- (C fld ...))))] ...
-----------
[ (match-Name x- P- C- ...) (app P- x-)])
(struct match-Name/delayed (m))
(define-syntax match-Name
(syntax-parser
#;[(_ . args)
#:do[(printf "trying to match:\n~a\n" (stx->datum #'args))]
#:when #f #'(void)]
[(_ n P Ccase ...)
(syntax-parse #'n
[((~literal #%plain-app) C-:id fld ...)
;; TODO: check C- matches actual C
;; for now, it's just an arity match
#'(app/eval (app/eval Ccase fld ...) (match-Name fld P Ccase ...) ...)] ...
[_ #'(#%app match/delayed 'match-Name (void n P Ccase ...))])]))
)]])
;; ;; #:with res (if (typecheck? #'n- (expand/df #'Z))
;; ;; #'z-
;; ;; #'(s- (nat-ind P- z- s- (sub1 n-))))
;; ----------------
;; [⊢ (match/nat n-
;; P-
;; z-
;; s-
;; #;(λ ([n-1 : Nat][rec : (app P- n-)])
;; (app s- n-1 rec #;(nat-ind P- z- s- n-1))))
;; ⇒ (app P- n-)])
; [≻ (P- d-)])
;; (define-syntax match/nat
;; (syntax-parser
;; [(_ n P zc sc)
;; #:do[(when debug-match?
;; (printf "match/nating: ~a\n" (stx->datum #'(n P zc sc)))
;; #;(printf "zc ty: ~a\n" (stx->datum (typeof #'zc)))
;; #;(printf "sc ty: ~a\n" (stx->datum (typeof #'sc))))]
;; #:when #f #'(void)]
;; [(_ (~and n ((~literal #%plain-app) z0:id)) P zc sc)
;; #:with (_ z1) (local-expand #'(#%app Z) 'expression null)
;; #:when (free-identifier=? #'z0 #'z1)
;; #:do [(when debug-match? (displayln 'zc))]
;; ;; #:when (printf "match eval res zero ety: ~a\n" (stx->datum (typeof this-syntax)))
;; ;; #:when (printf "match eval res zero ty: ~a\n" (stx->datum (typeof #'zc)))
;; (assign-type #'zc #'(app/eval P n))]
;; [(_ (~and n ((~literal #%plain-app) s0:id m)) P zc sc)
;; #:with (_ s1 . _) (local-expand #'(#%app S 'dont-care) 'expression null)
;; #:when (free-identifier=? #'s0 #'s1)
;; #:with (~Π ([_ : _] ...) τ_out) (typeof #'sc)
;; #:do[(when debug-match? (displayln 'sc))]
;; ;; #:when (printf "match eval res succ ety: ~a\n" (stx->datum (typeof this-syntax)))
;; ;; #:when (printf "match eval res succ ty: ~a\n" (stx->datum (typeof #'sc)))
;; ;; #:when (printf "match eval res succ ty: ~a\n" (stx->datum (typeof #'(app/eval (app/eval sc m) (match/nat m P zc sc)))))
;; ; #`(app sc m (nat-rec #,(typeof #'zc) zc sc m))]
;; ; #:with ty (typeof this-syntax)
;; (assign-type
;; #`(app/eval #,(assign-type #'(app/eval sc m) #'τ_out) (match/nat m P zc sc))
;; #'(app/eval P n))
;; ; #'res
;; ; (if (syntax-e #'ty) (assign-type #'res #'ty) #'res)
;; #;(assign-type #`(app/eval #,(assign-type #'(app/eval sc m) #'τ_out) (match/nat m P zc sc)) (typeof this-syntax))]
;; [(_ n P zc sc)
;; #:do[(when debug-match? (displayln "delay match"))]
;; (assign-type #'(#%app match/delayed n P zc sc) #'(app/eval P n))]))
;; #;(define-typed-syntax (nat-rec ty zc sc n) ≫
;; [⊢ ty ≫ ty- ⇐ #%type]
;; [⊢ zc ≫ zc- ⇐ ty-] ; zero case
;; [⊢ sc ≫ sc- ⇐ (→ ty- ty-)] ; succ case
;; [⊢ n ≫ n- ⇐ Nat]
;; ;; #:with res
;; ;; (syntax-parse #'n-
;; ;; [aaa #:do[(printf "matching: ~a\n" (stx->datum #'aaa))] #:when #f #'(void)]
;; ;; [((~literal #%plain-app) (~literal Z)) #'zc-]
;; ;; [((~literal #%plain-app) (~literal S) m) #'(app sc- (nat-rec zc- sc- m))])
;; --------------------
;; ; [⊢ (match/eval n- zc- sc-) ⇒ ty-])
;; [⊢ (match/nat n-
;; zc-
;; (λ ([n-1 : Nat][rec : ty-])
;; (sc- rec)))
;; ⇒ ty-])
; )]])
;; (define-base-type Nat)
;; (struct Z () #:transparent)
;; (struct S (n) #:transparent)
;; (define-typed-syntax Zero
;; [_:id ≫ --- [⊢ (Z) ⇒ Nat]])
;; (define-typed-syntax (Succ n) ≫
;; [⊢ n ≫ n- ⇐ Nat]
;; -----------
;; [⊢ (S n-) ⇒ 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 : (app P Zero)]
;; ;; [s : (Π ([k : Nat]) (→ (app P k) (app P (Succ k))))]
;; ;; [n : Nat])
;; ;; (app 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)))
(struct match/delayed (name args))
;; #;(define-syntax match/eval
;; (syntax-parser
;; [(_ n zc sc) #:do[(printf "matching: ~a\n" (stx->datum #'n))] #:when #f #'(void)]
;; [(_ ((~literal #%plain-app) z0:id) zc sc)
;; #:with (_ z1) (local-expand #'(Z) 'expression null)
;; #:when (free-identifier=? #'z0 #'z1)
;; #'zc]
;; [(_ ((~literal #%plain-app) s0:id m) zc sc)
;; #:with (_ s1 . _) (local-expand #'(S 'dont-care) 'expression null)
;; #:when (free-identifier=? #'s0 #'s1)
;; #:when (displayln 2)
;; #`(app sc (nat-rec #,(typeof #'zc) zc sc m))]
;; [(_ n zc sc) #'(match/delayed n zc sc)]))
;; ;; this is an "eval" form; should not do any more type checking
;; ;; otherwise, will get type errs some some subexprs may still have uninst tys
;; ;; eg, zc and sc were typechecked with paramaterized P instead of inst'ed P
;; (define-syntax match/nat
;; (syntax-parser
;; [(_ n P zc sc)
;; #:do[(when debug-match?
;; (printf "match/nating: ~a\n" (stx->datum #'(n P zc sc)))
;; #;(printf "zc ty: ~a\n" (stx->datum (typeof #'zc)))
;; #;(printf "sc ty: ~a\n" (stx->datum (typeof #'sc))))]
;; #:when #f #'(void)]
;; [(_ (~and n ((~literal #%plain-app) z0:id)) P zc sc)
;; #:with (_ z1) (local-expand #'(#%app Z) 'expression null)
;; #:when (free-identifier=? #'z0 #'z1)
;; #:do [(when debug-match? (displayln 'zc))]
;; ;; #:when (printf "match eval res zero ety: ~a\n" (stx->datum (typeof this-syntax)))
;; ;; #:when (printf "match eval res zero ty: ~a\n" (stx->datum (typeof #'zc)))
;; (assign-type #'zc #'(app/eval P n))]
;; [(_ (~and n ((~literal #%plain-app) s0:id m)) P zc sc)
;; #:with (_ s1 . _) (local-expand #'(#%app S 'dont-care) 'expression null)
;; #:when (free-identifier=? #'s0 #'s1)
;; #:with (~Π ([_ : _] ...) τ_out) (typeof #'sc)
;; #:do[(when debug-match? (displayln 'sc))]
;; ;; #:when (printf "match eval res succ ety: ~a\n" (stx->datum (typeof this-syntax)))
;; ;; #:when (printf "match eval res succ ty: ~a\n" (stx->datum (typeof #'sc)))
;; ;; #:when (printf "match eval res succ ty: ~a\n" (stx->datum (typeof #'(app/eval (app/eval sc m) (match/nat m P zc sc)))))
;; ; #`(app sc m (nat-rec #,(typeof #'zc) zc sc m))]
;; ; #:with ty (typeof this-syntax)
;; (assign-type
;; #`(app/eval #,(assign-type #'(app/eval sc m) #'τ_out) (match/nat m P zc sc))
;; #'(app/eval P n))
;; ; #'res
;; ; (if (syntax-e #'ty) (assign-type #'res #'ty) #'res)
;; #;(assign-type #`(app/eval #,(assign-type #'(app/eval sc m) #'τ_out) (match/nat m P zc sc)) (typeof this-syntax))]
;; [(_ n P zc sc)
;; #:do[(when debug-match? (displayln "delay match"))]
;; (assign-type #'(#%app match/delayed n P zc sc) #'(app/eval P n))]))
;; #;(define-typed-syntax (nat-rec ty zc sc n) ≫
;; [⊢ ty ≫ ty- ⇐ #%type]
;; [⊢ zc ≫ zc- ⇐ ty-] ; zero case
;; [⊢ sc ≫ sc- ⇐ (→ ty- ty-)] ; succ case
;; [⊢ n ≫ n- ⇐ Nat]
;; ;; #:with res
;; ;; (syntax-parse #'n-
;; ;; [aaa #:do[(printf "matching: ~a\n" (stx->datum #'aaa))] #:when #f #'(void)]
;; ;; [((~literal #%plain-app) (~literal Z)) #'zc-]
;; ;; [((~literal #%plain-app) (~literal S) m) #'(app sc- (nat-rec zc- sc- m))])
;; --------------------
;; ; [⊢ (match/eval n- zc- sc-) ⇒ ty-])
;; [⊢ (match/nat n-
;; zc-
;; (λ ([n-1 : Nat][rec : ty-])
;; (sc- rec)))
;; ⇒ ty-])
;; (define-typed-syntax (nat-ind P z s n) ≫
;; [⊢ P ≫ P- ⇐ (→ Nat #%type)]
;; [⊢ z ≫ z- ⇐ (app P- Zero)] ; zero
;; [⊢ s ≫ s- ⇐ (Π ([k : Nat]) (→ (app P- k) (app P- (Succ k))))] ; succ
;; [⊢ n ≫ n- ⇐ Nat]
;; ;; #:with res (if (typecheck? #'n- (expand/df #'Z))
;; ;; #'z-
;; ;; #'(s- (nat-ind P- z- s- (sub1 n-))))
;; ----------------
;; [⊢ (match/nat n-
;; P-
;; z-
;; s-
;; #;(λ ([n-1 : Nat][rec : (app P- n-)])
;; (app s- n-1 rec #;(nat-ind P- z- s- n-1))))
;; ⇒ (app P- n-)])
;; ; [≻ (P- d-)])

View File

@ -0,0 +1,137 @@
#lang s-exp "../dep-ind.rkt"
(require "rackunit-typechecking.rkt")
; Π → λ ∀ ≻ ⊢ ≫ ⇒
;; examples from Prabhakar's Proust paper
;; this file is like dep-peano-tests.rkt except it uses
;; define-datatype from #lang dep-ind.rkt to define Nat,
;; instead of using the builtin Nat from #lang dep.rkt
;; the examples in this file are mostly identical to dep-peano-tests.rkt,
;; except Z is replaced with (Z)
;; Peano nums -----------------------------------------------------------------
(define-datatype Nat : *
[Z : ( Nat)]
[S : ( Nat Nat)])
; TODO: special case 0-arity constructor using id macro
(check-type Z : ( Nat))
(check-type S : ( Nat Nat))
;(check-type Z : Nat -> Z)
(check-type (Z) : Nat -> (Z))
(check-type (S (Z)) : Nat -> (S (Z)))
(check-type (S (S (Z))) : Nat -> (S (S (Z))))
(define-type-alias nat-rec
(λ ([C : *])
(λ ([zc : ( C)][sc : ( C C)])
(λ ([n : Nat])
(elim-Nat n
(λ ([x : Nat]) C)
(λ () zc)
(λ ([x : Nat]) sc))))))
(check-type nat-rec : ( (C) ( ( C) ( C C) ( Nat C))))
;; nat-rec with no annotations
(check-type
(λ (C)
(λ (zc sc)
(λ (n)
(elim-Nat n
(λ (x) C)
(λ () zc)
(λ (x) sc)))))
: ( (C) ( ( C) ( C C) ( Nat C))))
(check-type (nat-rec Nat) : ( ( Nat) ( Nat Nat) ( Nat Nat)))
(check-type ((nat-rec Nat) Z (λ ([n : Nat]) (S n))) : ( Nat Nat))
;; basic identity example, to test eval
(define-type-alias id ((nat-rec Nat) Z (λ ([n : Nat]) (S n))))
(check-type (id (Z)) : Nat -> (Z))
;; this example will err if eval tries to tycheck again
(check-type (id (S (Z))) : Nat)
(check-type (id (S (Z))) : Nat -> (S (Z)))
(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)))
;; infer, and dont curry
(check-type
(λ (n1 n2)
((((nat-rec ( Nat Nat))
(λ () (λ (m) m))
(λ (pm) (λ (x) (S (pm x)))))
n1)
n2))
: ( 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)
;(check-type ((plus (S Z)) Z) : Nat -> 1)
(check-type (plus (Z)) : ( Nat Nat))
(check-type ((plus (Z)) (Z)) : Nat -> (Z))
(check-type ((plus (Z)) (S (Z))) : Nat -> (S (Z)))
(check-type ((plus (S (Z))) (Z)) : Nat -> (S (Z)))
(check-type ((plus (S (Z))) (S (Z))) : Nat -> (S (S (Z))))
(check-type ((plus (S (S (Z)))) (S (Z))) : Nat -> (S (S (S (Z)))))
(check-type ((plus (S (Z))) (S (S (Z)))) : Nat -> (S (S (S (Z)))))
;; plus zero (left)
(check-type (λ ([n : Nat]) (eq-refl n))
: (Π ([n : Nat]) (= ((plus (Z)) n) n)))
;; plus zero (right)
(check-type
(λ ([n : Nat])
(elim-Nat n
(λ ([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 : Nat]) (= ((plus n) (Z)) n)))
;; plus zero identity, no annotations
;; left:
(check-type (λ (n) (eq-refl n))
: (Π ([n : Nat]) (= ((plus (Z)) n) n)))
;; right:
(check-type
(λ (n)
(elim-Nat n
(λ (m) (= ((plus m) (Z)) m))
(λ () (λ () (eq-refl (Z))))
(λ (k) (λ (p)
(eq-elim ((plus k) (Z))
(λ (W) (= (S ((plus k) (Z))) (S W)))
(eq-refl (S ((plus k) (Z))))
k
p)))))
: (Π ([n : Nat]) (= ((plus n) (Z)) n)))
;; nat-ind as a function ; TODO: need matching form or matching lambda
#;(define-typed-alias nat-ind2
(λ ([P : ( Nat *)]
[Zcase : (P Z)]
[Scase : (Π ([k : Nat]) ( (P k) (P (S k))))]
[n : Nat])
(match/nat n ZCase (SCase n (nat-ind2 P ZCase SCase n-1)))))