stlc+cons.rkt (2081B)
1 #lang turnstile/lang 2 (extends "stlc+reco+var.rkt") 3 4 ;; Simply-Typed Lambda Calculus, plus cons 5 ;; Types: 6 ;; - types from stlc+reco+var.rkt 7 ;; - List constructor 8 ;; Terms: 9 ;; - terms from stlc+reco+var.rkt 10 11 ;; TODO: enable HO use of list primitives 12 13 (provide (type-out List) 14 nil isnil cons list head tail 15 reverse length list-ref member) 16 17 (define-type-constructor List) 18 19 (define-typed-syntax nil 20 [(_ ~! τi:type-ann) ≫ 21 -------- 22 [⊢ null- ⇒ (List τi.norm)]] 23 ; minimal type inference 24 [:id ⇐ (~List τ) ≫ 25 -------- 26 [⊢ null-]]) 27 (define-typed-syntax (cons e1 e2) ≫ 28 [⊢ e1 ≫ e1- ⇒ τ1] 29 [⊢ e2 ≫ e2- ⇐ (List τ1)] 30 -------- 31 [⊢ (cons- e1- e2-) ⇒ (List τ1)]) 32 (define-typed-syntax (isnil e) ≫ 33 [⊢ e ≫ e- ⇒ (~List _)] 34 -------- 35 [⊢ (null?- e-) ⇒ Bool]) 36 (define-typed-syntax (head e) ≫ 37 [⊢ e ≫ e- ⇒ (~List τ)] 38 -------- 39 [⊢ (car- e-) ⇒ τ]) 40 (define-typed-syntax (tail e) ≫ 41 [⊢ e ≫ e- ⇒ τ-lst] 42 #:fail-unless (List? #'τ-lst) 43 (format "Expected a list type, got: ~a" (type->str #'τ-lst)) 44 -------- 45 [⊢ (cdr- e-) ⇒ τ-lst]) 46 (define-typed-syntax list 47 [(_) ≫ 48 -------- 49 [≻ nil]] 50 [(_ x . rst) ⇐ (~List τ) ≫ ; has expected type 51 -------- 52 [⊢ (cons (add-expected x τ) (list . rst))]] 53 [(_ x . rst) ≫ ; no expected type 54 -------- 55 [≻ (cons x (list . rst))]]) 56 (define-typed-syntax (reverse e) ≫ 57 [⊢ e ≫ e- ⇒ τ-lst] 58 #:fail-unless (List? #'τ-lst) 59 (format "Expected a list type, got: ~a" (type->str #'τ-lst)) 60 -------- 61 [⊢ (reverse- e-) ⇒ τ-lst]) 62 (define-typed-syntax (length e) ≫ 63 [⊢ e ≫ e- ⇒ τ-lst] 64 #:fail-unless (List? #'τ-lst) 65 (format "Expected a list type, got: ~a" (type->str #'τ-lst)) 66 -------- 67 [⊢ (length- e-) ⇒ Int]) 68 (define-typed-syntax (list-ref e n) ≫ 69 [⊢ e ≫ e- ⇒ (~List τ)] 70 [⊢ n ≫ n- ⇐ Int] 71 -------- 72 [⊢ (list-ref- e- n-) ⇒ τ]) 73 (define-typed-syntax (member v e) ≫ 74 [⊢ e ≫ e- ⇒ (~List τ)] 75 [⊢ v ≫ v- ⇐ τ] 76 -------- 77 [⊢ (member- v- e-) ⇒ Bool])