diff options
| -rw-r--r-- | base.rkt | 28 | ||||
| -rw-r--r-- | stlc-dll.rkt | 250 | ||||
| -rw-r--r-- | stlc-ext.rkt | 211 | ||||
| -rw-r--r-- | stlc-fix.rkt | 83 | ||||
| -rw-r--r-- | stlc-full.rkt | 579 | ||||
| -rw-r--r-- | stlc-hor.rkt | 154 | ||||
| -rw-r--r-- | stlc-imp.rkt | 112 | ||||
| -rw-r--r-- | stlc-pred.rkt | 84 | ||||
| -rw-r--r-- | stlc-rec.rkt | 99 | ||||
| -rw-r--r-- | stlc-ref.rkt | 106 | ||||
| -rw-r--r-- | stlc.rkt | 56 | ||||
| -rw-r--r-- | tests/stlc-imp.rkt | 29 | ||||
| -rw-r--r-- | tests/stlc-pred.rkt | 29 | ||||
| -rw-r--r-- | tests/stlc.rkt | 8 |
14 files changed, 975 insertions, 853 deletions
@@ -12,10 +12,12 @@ [`(λ ,x ,e) (format "λ~a.[~a]" x (fmt e))] [`((λ ,x ,e1) ,e2) (format "~a = ~a; ~a" x (fmt e2) (fmt e1))] [`(λ (,x : ,t) ,e) (format "~a: ~a; ~a" x (fmt t) (fmt e))] - [`((λ (,x : ,t) ,e1) ,e2) (format "~a: ~a; ~a = ~a; ~a" x (fmt t) x (fmt e2) (fmt e1))] + [`((λ (,x : ,t) ,e1) ,e2) + (format "~a: ~a; ~a = ~a; ~a" x (fmt t) x (fmt e2) (fmt e1))] [`(λ ,x ,e ,env) (format "λ~a.[~a]" x (fmt e))] [`(μ ,x ,t) (format "μ~a.~a" x (fmt t))] - [`(let (,x : ,t) ,e ,in) (format "~a: ~a; ~a = ~a; ~a" x (fmt t) x (fmt e) (fmt in))] + [`(let (,x : ,t) ,e ,in) + (format "~a: ~a; ~a = ~a; ~a" x (fmt t) x (fmt e) (fmt in))] [`(let ,x ,e ,in) (format "~a = ~a; ~a" x (fmt e) (fmt in))] [`(set ,x ,e ,in) (format "~a := ~a; ~a" x (fmt e) (fmt in))] [`(,a → ,b) (format "(~a → ~a)" (fmt a) (fmt b))] @@ -25,25 +27,21 @@ [`(! ,a) (format "!~a" (fmt a))] [`(,a ,b) (format "(~a ~a)" (fmt a) (fmt b))] [(hash-table (keys values) ...) - (format "{~a}" (foldl (λ (k v acc) (format "~a: ~a;" (fmt k) (fmt v))) "" keys values))] - [expr (format "~a" expr)])) + (format "{~a}" + (foldl + (λ (k v acc) + (format "~a: ~a;" (fmt k) (fmt v))) + "" keys values))] + [_ (format "~a" expr)])) -;; Removes typing annotations and similar constructs, for interpretation -(define (strip expr) - (match expr - [`(,e : ,_) (strip e)] - [`(type ,_ ,_ ,e) (strip e)] - [`(fold ,_ ,e) `(fold ,(strip e))] - [`(unfold ,_ ,e) `(unfold ,(strip e))] - [`(,e ...) `(,@(map strip e))] - [e e])) - -;; Define aliases from higher-level constructs to their core forms +;; Aliases from higher-level constructs to their core forms. +;; This lets us elide many typing annotations. (define (desugar expr) (match expr ['⟨⟩ 'sole] [`(ref ,e) (desugar `(new ,e))] [`(deref ,e) (desugar `(! ,e))] + [`(,e ⇑ ,k) (desugar `(,e :: ,k))] ; set-with-continuation [`(set ,e1 ,e2 ,in) diff --git a/stlc-dll.rkt b/stlc-dll.rkt index 31c5bcc..1eef6d7 100644 --- a/stlc-dll.rkt +++ b/stlc-dll.rkt @@ -1,204 +1,266 @@ #lang racket (require "lib.rkt" "base.rkt") (require (only-in "stlc-rec.rkt" replace)) -(require (only-in "stlc-ext.rkt" expand)) -(provide interpret check infer level-type level-body equiv-type) +(require (only-in "stlc-ext.rkt" type->whnf)) +(provide (all-defined-out)) ;; The Simply-Typed Lambda Calculus with higher-order *impredicative* references, ;; plus sums products booleans ascryption etc, to implement doubly-linked lists -;; (interpret Expr Table[Sym, Expr] Table[Sym, Expr]): Value ⊕ Err +;; Checks an expression for syntactic well-formedness. +(define (stlc-dll/expr? expr) + (match expr + [x #:when (symbol? x) #t] + [n #:when (natural? n) #t] + [b #:when (boolean? b) #t] + [`(,e : ,t) + (and (stlc-dll/expr? e) (stlc-dll/type? t))] + [`(type ,t1 ,t2 ,e) + (and (stlc-dll/type? t1) (stlc-dll/type? t2) (stlc-dll/expr? e))] + [(or + `(inc ,e) + `(car ,e) `(cdr ,e) + `(inl ,e) `(inr ,e) + `(new ,e) `(! ,e) + `(fold ,e) `(unfold ,e)) + (stlc-dll/expr? e)] + [(or + `(pair ,e1 ,e2) + `(set ,e1 ,e2) + `(,e1 ,e2)) + (and (stlc-dll/expr? e1) (stlc-dll/expr? e2))] + [`(if ,c ,e1 ,e2) + (and (stlc-dll/expr? c) (stlc-dll/expr? e1) (stlc-dll/expr? e2))] + [`(case ,c (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) + (and (symbol? x1) (symbol? x2) + (stlc-dll/expr? c) (stlc-dll/expr? e1) (stlc-dll/expr? e2))] + [`(λ (,x : ,t) ,e) + (and (symbol? x) (stlc-dll/type? t) (stlc-dll/expr? e))] + [_ #f])) + +;; Checks a type for syntactic well-formedness. +(define (stlc-dll/type? type) + (match type + ; Symbols are only valid if previously bound (by `type` or `μ`). + ; We can't check that here, however. + [x #:when (symbol? x) #t] + [`(Ref ,t) (stlc-dll/type? t)] + [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2)) + (and (stlc-dll/type? t1) (stlc-dll/type? t2))] + [`(,t1 → ,k ,t2) + (and (stlc-dll/type? t1) (natural? k) (stlc-dll/type? t2))] + [`(μ ,x ,t) + (and (symbol? x) (stlc-dll/type? t))] + [_ #f])) + +;; Checks a value for syntactic well-formedness. +(define (stlc-dll/value? expr) + (match expr + [x #:when (symbol? x) #t] + [n #:when (natural? n) #t] + [b #:when (boolean? b) #t] + [(or `(inl ,v) `(inr ,v)) + (stlc-dll/value? v)] + [(or `(pair ,v1 ,v2) `(,v1 ,v2)) + (and (stlc-dll/value? v1) (stlc-dll/value? v2))] + [`(λ (,x : ,t) ,e ,env) + (and (symbol? x) (stlc-dll/type? t) (stlc-dll/expr? e) (dict? env))] + [_ #f])) + + (define (interpret expr) - (interpret-core (strip (desugar expr)) #hash() (make-hash))) + (interpret/core (desugar expr) #hash() (make-hash))) ;; Γ: a Table[Symbol, Expr] representing the context: ;; the current bindings in scope introduced by λx.[] ;; Σ: a Table[Symbol, Expr] representing the heap: ;; the current references on the heap generated by (gensym). mutable ;; Interprets a *desugared* expression *stripped* of type annotations. -(define (interpret-core expr Γ Σ) +(define/contract (interpret/core expr Γ Σ) + (-> stlc-dll/expr? dict? dict? stlc-dll/value?) (match expr ['sole 'sole] [n #:when (natural? n) n] [b #:when (boolean? b) b] [r #:when (dict-has-key? Σ r) r] [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] + [f #:when (symbol? f) f] [`(inc ,e) - (match (interpret-core e Γ Σ) + (match (interpret/core e Γ Σ) [n #:when (natural? n) (+ n 1)] [e (format "incrementing an unknown value ~a" e)])] [`(if ,c ,e1 ,e2) - (match (interpret-core c Γ Σ) - ['#t (interpret-core e1 Γ Σ)] - ['#f (interpret-core e2 Γ Σ)] + (match (interpret/core c Γ Σ) + ['#t (interpret/core e1 Γ Σ)] + ['#f (interpret/core e2 Γ Σ)] [e (err (format "calling if on unknown expression ~a" e))])] [`(pair ,e1 ,e2) - `(pair ,(interpret-core e1 Γ Σ) ,(interpret-core e2 Γ Σ))] + `(pair ,(interpret/core e1 Γ Σ) ,(interpret/core e2 Γ Σ))] [`(car ,e) - (match (interpret-core e Γ Σ) + (match (interpret/core e Γ Σ) [`(pair ,e1 ,e2) e1] [e (err (format "calling car on unknown expression ~a" e))])] [`(cdr ,e) - (match (interpret-core e Γ Σ) + (match (interpret/core e Γ Σ) [`(pair ,e1 ,e2) e2] [e (err (format "calling cdr on unknown expression ~a" e))])] - [`(inl ,e) `(inl ,(interpret-core e Γ Σ))] - [`(inr ,e) `(inr ,(interpret-core e Γ Σ))] + [`(inl ,e) `(inl ,(interpret/core e Γ Σ))] + [`(inr ,e) `(inr ,(interpret/core e Γ Σ))] [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) - (match (interpret-core e Γ Σ) - [`(inl ,e) (interpret-core e1 (dict-set Γ x1 e) Σ)] - [`(inr ,e) (interpret-core e2 (dict-set Γ x2 e) Σ)] + (match (interpret/core e Γ Σ) + [`(inl ,e) (interpret/core e1 (dict-set Γ x1 e) Σ)] + [`(inr ,e) (interpret/core e2 (dict-set Γ x2 e) Σ)] [e (err (format "calling case on unknown expression ~a" e))])] [`(new ,e) (let ([r (gensym)]) (dict-set! Σ r e) r)] [`(! ,e) - (let ([r (interpret-core e Γ Σ)]) + (let ([r (interpret/core e Γ Σ)]) (if (dict-has-key? Σ r) - (interpret-core (dict-ref Σ r) Γ Σ) + (interpret/core (dict-ref Σ r) Γ Σ) (err (format "attempting to deref unknown reference ~a" r))))] [`(set ,e1 ,e2) - (let ([r (interpret-core e1 Γ Σ)]) - (if (dict-has-key? Σ r) (dict-set! Σ r (interpret-core e2 Γ Σ)) + (let ([r (interpret/core e1 Γ Σ)]) + (if (dict-has-key? Σ r) (dict-set! Σ r (interpret/core e2 Γ Σ)) (err (format "attempting to update unknown reference ~a" r)))) 'sole] - [`(fold ,e) `(fold ,(interpret-core e Γ Σ))] + [`(fold ,e) `(fold ,(interpret/core e Γ Σ))] [`(unfold ,e) - (match (interpret-core e Γ Σ) + (match (interpret/core e Γ Σ) [`(fold ,e) e] [e (err (format "attempting to unfold unknown expression ~a" e))])] - [`(λ ,x ,e) `(λ ,x ,e ,Γ)] + [`(λ (,x : ,t) ,e) `(λ ,x ,e ,Γ)] [`(,e1 ,e2) - (match (interpret-core e1 Γ Σ) + (match (interpret/core e1 Γ Σ) [`(λ ,x ,e1 ,env) - (interpret-core e1 (dict-set env x (interpret-core e2 Γ Σ)) Σ)] - [e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])] - - [e (err (format "attempting to interpret unknown expression ~a" e))])) + (interpret/core e1 (dict-set env x (interpret/core e2 Γ Σ)) Σ)] + [e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])])) ;; Checks that an expression is of a type, and returns #t or #f (or a bubbled-up error) ;; with: a type in weak-head normal form (!!) ;; Γ: a Table[Symbol, Expr ⊕ Type] representing the context: ;; the current bindings in scope introduced by λx.[] and μx.[] and τx.[] -;; (check Expr Type Table[Sym, Type]): Bool (define (check expr with) - (check-core (desugar expr) with #hash())) -(define (check-core expr with Γ) + (check/core (desugar expr) with #hash())) +(define/contract (check/core expr with Γ) + (-> stlc-dll/expr? stlc-dll/type? dict? boolean?) (match expr [`(type ,t1 ,t2 ,in) - (check-core in with (dict-set Γ `(type ,t1) t2))] + (check/core in with (dict-set Γ `(type ,t1) t2))] [`(if ,c ,e1 ,e2) - (and (check-core c 'Bool Γ) - (check-core e1 with Γ) (check-core e2 with Γ))] + (and (check/core c 'Bool Γ) + (check/core e1 with Γ) (check/core e2 with Γ))] [`(pair ,e1 ,e2) (match with - [`(,t1 × ,t2) (and (check-core e1 t1 Γ) (check-core e2 t2 Γ))] + [`(,t1 × ,t2) (and (check/core e1 t1 Γ) (check/core e2 t2 Γ))] [_ #f])] [`(inl ,e) (match with - [`(,t1 ⊕ ,t2) (check-core e t1 Γ)] + [`(,t1 ⊕ ,t2) (check/core e t1 Γ)] [_ #f])] [`(inr ,e) (match with - [`(,t1 ⊕ ,t2) (check-core e t2 Γ)] + [`(,t1 ⊕ ,t2) (check/core e t2 Γ)] [_ #f])] [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) - (match (infer-core e Γ) ; avoid needing type annotation on e + (match (infer/core e Γ) ; avoid needing type annotation on e [`(,a1 ⊕ ,a2) - (and (check-core e1 with (dict-set Γ x1 a1)) - (check-core e2 with (dict-set Γ x2 a2)))] + (and (check/core e1 with (dict-set Γ x1 a1)) + (check/core e2 with (dict-set Γ x2 a2)))] [_ #f])] [`(new ,e) (match with - [`(Ref ,t) (check-core e t Γ)] + [`(Ref ,t) (check/core e t Γ)] [_ #f])] [`(! ,e) - (check-core e `(Ref ,with) Γ)] + (check/core e `(Ref ,with) Γ)] [`(fold ,e) (match with - [`(μ ,x ,t) (check-core e t (dict-set Γ `(type ,x) `(μ ,x ,t)))] + [`(μ ,x ,t) (check/core e t (dict-set Γ `(type ,x) `(μ ,x ,t)))] [_ #f])] [`(λ (,x : ,t) ,e) (match with [`(,t1 → ,k ,t2) - (and (equiv-type t t1 Γ) (check-core e t2 (dict-set Γ x t)) + (and (equiv-type t t1 Γ) (check/core e t2 (dict-set Γ x t)) (> k (level-body e (dict-set Γ x t1))))] ; KNOB [`(,t1 → ,t2) (err (format "missing level annotation on function type"))] [_ #f])] - [_ (equiv-type (infer-core expr Γ) with Γ)])) + [_ (equiv-type (infer/core expr Γ) with Γ)])) ;; Checks if two types are equivalent up to α-conversion in context -;; (equiv-type Type Type Table[Sym Type]): Bool (define (equiv-type e1 e2 Γ) - (equiv-type-core e1 e2 Γ Γ)) -(define (equiv-type-core e1 e2 Γ1 Γ2) + (equiv-type/core e1 e2 Γ Γ)) +(define/contract (equiv-type/core e1 e2 Γ1 Γ2) + (-> stlc-dll/type? stlc-dll/type? dict? dict? boolean?) (match* (e1 e2) ; bound identifiers: if a key exists in the context, look it up [(x1 x2) #:when (dict-has-key? Γ1 x1) - (equiv-type-core (dict-ref Γ1 x1) x2 Γ1 Γ2)] + (equiv-type/core (dict-ref Γ1 x1) x2 Γ1 Γ2)] [(x1 x2) #:when (dict-has-key? Γ2 x2) - (equiv-type-core x1 (dict-ref Γ2 x2) Γ1 Γ2)] + (equiv-type/core x1 (dict-ref Γ2 x2) Γ1 Γ2)] ; recursive types: self-referential names can be arbitrary [(`(μ ,x1 ,t1) `(μ ,x2 ,t2)) (let ([name gensym]) - (equiv-type-core t1 t2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))] + (equiv-type/core t1 t2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))] ; check for syntactic equivalence on remaining forms [(`(,l1 ...) `(,l2 ...)) - (foldl (λ (x1 x2 acc) (if (equiv-type-core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)] + (foldl (λ (x1 x2 acc) (if (equiv-type/core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)] [(v1 v2) (equal? v1 v2)])) ;; Infers a type from a given expression, if possible, or errors out. ;; Returns a type in weak-head normal form for structural matching. -;; (infer Expr Table[Sym, Type]): Type (define (infer expr) - (infer-core (desugar expr) #hash())) -(define (infer-core expr Γ) + (infer/core (desugar expr) #hash())) +(define/contract (infer/core expr Γ) + (-> stlc-dll/expr? dict? stlc-dll/type?) (match expr ['sole 'Unit] [n #:when (natural? n) 'Nat] [b #:when (boolean? b) 'Bool] [x #:when (dict-has-key? Γ x) - (expand (dict-ref Γ x) Γ)] + (type->whnf (dict-ref Γ x) Γ)] + [f #:when (symbol? f) + (err (format "attempting to infer type of free variable ~a" f))] [`(type ,t1 ,t2 ,in) - (infer-core in (dict-set Γ `(type ,t1) t2))] + (infer/core in (dict-set Γ `(type ,t1) t2))] [`(,e : ,t) ; we have a manual type annotation, so we must expand to weak-head normal form - (if (check-core e (expand t Γ) Γ) (expand t Γ) + (if (check/core e (type->whnf t Γ) Γ) (type->whnf t Γ) (err (format "annotated expression ~a is not of annotated type ~a" e t)))] [`(inc ,e) - (if (check-core e 'Nat Γ) 'Nat - (err (format "calling inc on incorrect type ~a" (infer-core e Γ))))] + (if (check/core e 'Nat Γ) 'Nat + (err (format "calling inc on incorrect type ~a" (infer/core e Γ))))] [`(if ,c ,e1 ,e2) - (if (check-core c 'Bool Γ) - (let ([t (infer-core e1 Γ)]) - (if (check-core e2 t Γ) t + (if (check/core c 'Bool Γ) + (let ([t (infer/core e1 Γ)]) + (if (check/core e2 t Γ) t (err (format "condition has branches of differing types ~a and ~a" - t (infer-core e2 Γ))))) - (err (format "condition ~a has incorrect type ~a" c (infer-core c Γ))))] + t (infer/core e2 Γ))))) + (err (format "condition ~a has incorrect type ~a" c (infer/core c Γ))))] [`(pair ,e1 ,e2) - `(,(infer-core e1 Γ) × ,(infer-core e2 Γ))] + `(,(infer/core e1 Γ) × ,(infer/core e2 Γ))] [`(car ,e) - (match (infer-core e Γ) + (match (infer/core e Γ) [`(,t1 × ,t2) t1] [t (err (format "calling car on incorrect type ~a" t))])] [`(cdr ,e) - (match (infer-core e Γ) + (match (infer/core e Γ) [`(,t1 × ,t2) t2] [t (err (format "calling cdr on incorrect type ~a" t))])] @@ -207,53 +269,51 @@ [`(inr ,e) (err (format "unable to infer the type of a raw inr"))] [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) - (match (infer-core e Γ) + (match (infer/core e Γ) [`(,a1 ⊕ ,a2) - (let ([b1 (infer-core e1 (dict-set Γ x1 a1))] - [b2 (infer-core e2 (dict-set Γ x2 a2))]) + (let ([b1 (infer/core e1 (dict-set Γ x1 a1))] + [b2 (infer/core e2 (dict-set Γ x2 a2))]) (if (equiv-type b1 b2 Γ) b1 (err (format "case ~a is not of consistent type!" `(case (,a1 ⊕ ,a2) (,x1 ⇒ ,b1) (,x2 ⇒ ,b2))))))] [t (err (format "calling case on incorrect type ~a" t))])] [`(new ,e) - `(Ref ,(infer-core e Γ))] + `(Ref ,(infer/core e Γ))] [`(! ,e) - (match (infer-core e Γ) + (match (infer/core e Γ) [`(Ref ,t) t] [t (err (format "attempting to deref term ~a of type ~a" e t))])] [`(set ,e1 ,e2) - (match (infer-core e1 Γ) + (match (infer/core e1 Γ) [`(Ref ,t) - (if (check-core e2 t Γ) 'Unit + (if (check/core e2 t Γ) 'Unit (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type" - e1 t e2 (infer-core e2 Γ))))] + e1 t e2 (infer/core e2 Γ))))] [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] [`(unfold ,e) - (match (infer-core e Γ) + (match (infer/core e Γ) [`(μ ,x ,t) (replace t x `(μ ,x ,t))] [t (err (format "expected ~a to be recursive, got ~a" e t))])] [`(λ (,x : ,t1) ,e) - (let* ([t2 (infer-core e (dict-set Γ x t1))] - [t1 (expand t1 Γ)] ; type annotation, must expand + (let* ([t2 (infer/core e (dict-set Γ x t1))] + [t1 (type->whnf t1 Γ)] ; type annotation, must expand [k (+ 1 (level-body e (dict-set Γ x t1)))]) ; KNOB `(,t1 → ,k ,t2))] [`(,e1 ,e2) - (match (infer-core e1 Γ) + (match (infer/core e1 Γ) [`(,t1 → ,k ,t2) - (if (check-core e2 t1 Γ) t2 - (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer-core e2 Γ))))] + (if (check/core e2 t1 Γ) t2 + (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer/core e2 Γ))))] [`(,t1 → ,t2) (err (format "missing level annotation on function type"))] - [t (err (format "expected → type on application body, got ~a" t))])] - - [e (err (format "attempting to infer an unknown expression ~a" e))])) + [t (err (format "expected → type on application body, got ~a" t))])])) ;; Checks if a type is well-formed in the current context. ;; BIG ASSUMPTION: types in the current context are well-formed -;; (well-formed Type Context): Bool -(define (well-formed t Γ) +(define/contract (well-formed t Γ) + (-> stlc-dll/type? dict? boolean?) (match t [x #:when (dict-has-key? Γ x) #t] [(or 'Unit 'Nat 'Bool) #t] @@ -266,8 +326,8 @@ ;; Checks if a type is well-kinded with respect to a level in the current context ;; BIG ASSUMPTION: types in the current context are well-formed -;; (well-kinded Type Level Context): Bool -(define (well-kinded t l Γ) +(define/contract (well-kinded t l Γ) + (-> stlc-dll/type? natural? dict? boolean?) (match t [x #:when (dict-has-key? Γ x) #t] [(or 'Unit 'Nat 'Bool) (>= l 0)] @@ -284,8 +344,8 @@ [_ #f])) ;; Infers the level of a (well-formed) type. -;; (level-type Type): Natural -(define (level-type t Γ) +(define/contract (level-type t Γ) + (-> stlc-dll/type? dict? natural?) (match t [x #:when (dict-has-key? Γ x) (level-type (dict-ref Γ x) Γ)] @@ -303,13 +363,13 @@ [t #:when (symbol? t) 0])) ; μ-type variables, not in Γ ;; Infers the level of a (well-formed) expression. -;; (level-body Expr Context): Natural -(define (level-body e Γ) +(define/contract (level-body e Γ) + (-> stlc-dll/expr? dict? natural?) (match e ['sole 0] [n #:when (natural? n) 0] [x #:when (dict-has-key? Γ x) ; free variables, get their level - (level-type (expand (dict-ref Γ x) Γ) Γ)] + (level-type (type->whnf (dict-ref Γ x) Γ) Γ)] [(or `(,e : ,_) `(λ (,_ : ,_) ,e) `(inc ,e) `(new ,e) `(! ,e) `(car ,e) `(cdr ,e) `(inl ,e) `(inr ,e) `(fold ,e) `(unfold ,e) `(fold (μ ,_ ,_) ,e) `(unfold (μ ,_ ,_) ,e)) diff --git a/stlc-ext.rkt b/stlc-ext.rkt index 2662135..c76db93 100644 --- a/stlc-ext.rkt +++ b/stlc-ext.rkt @@ -1,107 +1,172 @@ #lang racket (require "lib.rkt") (require "base.rkt") -(provide interpret check infer expand equiv-type equiv-term) +(provide (all-defined-out)) ;; The Simply-Typed Lambda Calculus, with simple extensions ;; Unit/String/Natural/Boolean, pairs, sums, lists, ascryption -;; (interpret Expr Table[Sym, Expr]): Value +;; Checks an expression for syntactic well-formedness. +(define (stlc-ext/expr? expr) + (match expr + [(or 'sole 'nil) #t] + [s #:when (string? s) #t] + [n #:when (natural? n) #t] + [b #:when (boolean? b) #t] + [x #:when (symbol? x) #t] + + [(or + `(inc ,e) + `(car ,e) `(cdr ,e) + `(inl ,e) `(inr ,e) + `(head ,e) `(tail ,e) `(nil? ,e)) + (stlc-ext/expr? e)] + [(or + `(pair ,e1 ,e2) + `(cons ,e1 ,e2) + `(,e1 ,e2)) + (and (stlc-ext/expr? e1) (stlc-ext/expr? e2))] + + [`(if ,c ,e1 ,e2) + (and (stlc-ext/expr? c) (stlc-ext/expr? e1) (stlc-ext/expr? e2))] + [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) + (and (stlc-ext/expr? e) (stlc-ext/expr? e1) (stlc-ext/expr? e2) + (symbol? x1) (symbol? x2))] + [`(type ,t1 ,t2 ,e) + (and (stlc-ext/type? t1) (stlc-ext/type? t2) (stlc-ext/expr? e))] + [`(λ (,x : ,t) ,e) + (and (symbol? x) (stlc-ext/type? t) (stlc-ext/expr? e))] + [_ #f])) + +;; Checks a type for syntactic well-formedness. +(define (stlc-ext/type? type) + (match type + [t #:when (symbol? t) #t] + [`(List ,t) (stlc-ext/type? t)] + [(or + `(,t1 → ,t2) + `(,t1 × ,t2) + `(,t1 ⊕ ,t2)) + (and (stlc-ext/type? t1) (stlc-ext/type? t2))] + [_ #f])) + +;; Checks a value for syntactic well-formedness. +(define (stlc-ext/value? value) + (match value + [(or 'sole 'nil) #t] + [s #:when (string? s) #t] + [n #:when (natural? n) #t] + [b #:when (boolean? b) #t] + [x #:when (symbol? x) #t] + [(or + `(pair ,v1 ,v2) + `(cons ,v1 ,v2) + `(,v1 ,v2)) + (and (stlc-ext/value? v1) (stlc-ext/value? v2))] + [`(λ ,x ,e ,env) + (and (symbol? x) (stlc-ext/expr? e) (dict? env))] + [_ #f])) + +;; Interprets an expression down to a value, in a given context. (define (interpret expr) - (interpret-core (strip (desugar expr)) #hash())) -(define (interpret-core expr Γ) + (interpret/core (desugar expr) #hash())) +(define/contract (interpret/core expr Γ) + (-> stlc-ext/expr? dict? stlc-ext/value?) (match expr ['sole 'sole] [s #:when (string? s) s] [n #:when (natural? n) n] [b #:when (boolean? b) b] [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] + [f #:when (symbol? f) f] + + [`(,e : ,t) (interpret/core e Γ)] + [`(type ,t1 ,t2 ,e) (interpret/core e Γ)] [`(inc ,e) - (match (interpret-core e Γ) + (match (interpret/core e Γ) [n #:when (natural? n) (+ n 1)] [e (format "incrementing an unknown value ~a" e)])] [`(if ,c ,e1 ,e2) - (match (interpret-core c Γ) - ['#t (interpret-core e1 Γ)] - ['#f (interpret-core e2 Γ)] + (match (interpret/core c Γ) + ['#t (interpret/core e1 Γ)] + ['#f (interpret/core e2 Γ)] [e (err (format "calling if on unknown expression ~a" e))])] [`(pair ,e1 ,e2) - `(pair ,(interpret-core e1 Γ) ,(interpret-core e2 Γ))] + `(pair ,(interpret/core e1 Γ) ,(interpret/core e2 Γ))] [`(car ,e) - (match (interpret-core e Γ) + (match (interpret/core e Γ) [`(pair ,e1 ,e2) e1] [e (err (format "calling car on unknown expression ~a" e))])] [`(cdr ,e) - (match (interpret-core e Γ) + (match (interpret/core e Γ) [`(pair ,e1 ,e2) e2] [e (err (format "calling cdr on unknown expression ~a" e))])] - [`(inl ,e) `(inl ,(interpret-core e Γ))] - [`(inr ,e) `(inr ,(interpret-core e Γ))] + [`(inl ,e) `(inl ,(interpret/core e Γ))] + [`(inr ,e) `(inr ,(interpret/core e Γ))] [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) - (match (interpret-core e Γ) - [`(inl ,e) (interpret-core e1 (dict-set Γ x1 e))] - [`(inr ,e) (interpret-core e2 (dict-set Γ x2 e))] + (match (interpret/core e Γ) + [`(inl ,e) (interpret/core e1 (dict-set Γ x1 e))] + [`(inr ,e) (interpret/core e2 (dict-set Γ x2 e))] [e (err (format "calling case on unknown expression ~a" e))])] ['nil 'nil] [`(nil? ,e) - (match (interpret-core e Γ) + (match (interpret/core e Γ) ['nil '#t] [`(cons ,e1 ,e2) '#f] [e (err (format "calling isnil on unknown expression ~a" e))])] [`(cons ,e1 ,e2) - `(cons ,(interpret-core e1 Γ) ,(interpret-core e2 Γ))] + `(cons ,(interpret/core e1 Γ) ,(interpret/core e2 Γ))] [`(head ,e) - (match (interpret-core e Γ) - [`(cons ,e1 ,e2) (interpret-core e1 Γ)] + (match (interpret/core e Γ) + [`(cons ,e1 ,e2) (interpret/core e1 Γ)] [e (err (format "calling head on unknown expression ~a" e))])] [`(tail ,e) - (match (interpret-core e Γ) - [`(cons ,e1 ,e2) (interpret-core e2 Γ)] + (match (interpret/core e Γ) + [`(cons ,e1 ,e2) (interpret/core e2 Γ)] [e (err (format "calling tail on unknown expression ~a" e))])] - [`(λ ,x ,e) `(λ ,x ,e ,Γ)] + [`(λ (,x : ,t) ,e) `(λ ,x ,e ,Γ)] [`(,e1 ,e2) - (match (interpret-core e1 Γ) + (match (interpret/core e1 Γ) [`(λ ,x ,e ,env) - (interpret-core e (dict-set env x (interpret-core e2 Γ)))] - [e (err (format "applying arg ~a to unknown expression ~a" e2 e))])] - - [e (err (format "interpreting an unknown expression ~a" e))])) + (interpret/core e (dict-set env x (interpret/core e2 Γ)))] + [e (err (format "applying arg ~a to unknown expression ~a" e2 e))])])) -;; (check Expr Type Table[Sym, Type]): Bool +;; Checks an expression against some type, in a given context. (define (check expr with) - (check-core (desugar expr) with #hash())) -(define (check-core expr with Γ) + (check/core (desugar expr) with #hash())) +(define/contract (check/core expr with Γ) + (-> stlc-ext/expr? stlc-ext/type? dict? boolean?) (match expr [`(type ,t1 ,t2 ,in) - (check-core in with (dict-set Γ t1 t2))] + (check/core in with (dict-set Γ t1 t2))] [`(if ,c ,e1 ,e2) - (and (check-core c 'Bool Γ) - (check-core e1 with Γ) (check-core e2 with Γ))] + (and (check/core c 'Bool Γ) + (check/core e1 with Γ) (check/core e2 with Γ))] [`(pair ,e1 ,e2) (match with - [`(,t1 × ,t2) (and (check-core e1 t1 Γ) (check-core e2 t2 Γ))] + [`(,t1 × ,t2) (and (check/core e1 t1 Γ) (check/core e2 t2 Γ))] [_ #f])] [`(inl ,e) (match with - [`(,t1 ⊕ ,t2) (check-core e t1 Γ)] + [`(,t1 ⊕ ,t2) (check/core e t1 Γ)] [_ #f])] [`(inr ,e) (match with - [`(,t1 ⊕ ,t2) (check-core e t2 Γ)] + [`(,t1 ⊕ ,t2) (check/core e t2 Γ)] [_ #f])] [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) (match (infer-core e Γ) [`(,a1 ⊕ ,a2) - (and (check-core e1 with (dict-set Γ x1 a1)) - (check-core e2 with (dict-set Γ x2 a2)))] + (and (check/core e1 with (dict-set Γ x1 a1)) + (check/core e2 with (dict-set Γ x2 a2)))] [_ #f])] ['nil @@ -111,43 +176,46 @@ [`(cons ,f1 ,f2) (match with [`(List ,t) - (and (check-core f1 t Γ) - (check-core f2 `(List ,t) Γ))] + (and (check/core f1 t Γ) + (check/core f2 `(List ,t) Γ))] [_ #f])] [`(λ (,x : ,t) ,e) (match with [`(,t1 → ,t2) - (and (equiv-type t1 t Γ) (check-core e t2 (dict-set Γ x t1)))] + (and (equiv-type t1 t Γ) (check/core e t2 (dict-set Γ x t1)))] [_ #f])] [_ (equiv-type (infer-core expr Γ) with Γ)])) -;; (infer Expr Table[Sym, Type]): Type +;; Infers a type from some expression, in a given context. (define (infer expr) (infer-core (desugar expr) #hash())) -(define (infer-core expr Γ) +(define/contract (infer-core expr Γ) + (-> stlc-ext/expr? dict? stlc-ext/type?) (match expr ['sole 'Unit] [s #:when (string? s) 'Str] [n #:when (natural? n) 'Nat] [b #:when (boolean? b) 'Bool] [x #:when (dict-has-key? Γ x) - (expand (dict-ref Γ x) Γ)] + (type->whnf (dict-ref Γ x) Γ)] + [f #:when (symbol? f) + (err (format "attempting to infer type of free variable ~a" f))] [`(type ,t1 ,t2 ,in) (infer-core in (dict-set Γ t1 t2))] [`(,e : ,t) - (if (check-core e (expand t Γ) Γ) (expand t Γ) + (if (check/core e (type->whnf t Γ) Γ) (type->whnf t Γ) (err (format "annotated expression ~a is not of annotated type ~a" e t)))] [`(inc ,e) - (if (check-core e 'Nat Γ) 'Nat + (if (check/core e 'Nat Γ) 'Nat (err (format "calling inc on incorrect type ~a" (infer-core e Γ))))] [`(if ,c ,e1 ,e2) - (if (check-core c 'Bool Γ) + (if (check/core c 'Bool Γ) (let ([t (infer-core e1 Γ)]) - (if (check-core e2 t Γ) t + (if (check/core e2 t Γ) t (err (format "condition has branches of differing types ~a and ~a" t (infer-core e2 Γ))))) (err (format "condition ~a has incorrect type ~a" c (infer-core c Γ))))] @@ -174,8 +242,8 @@ [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) (match (infer-core e Γ) [`(,a1 ⊕ ,a2) - (let ([b1 (infer-core e1 (dict-set Γ x1 (expand a1 Γ)))] - [b2 (infer-core e2 (dict-set Γ x2 (expand a2 Γ)))]) + (let ([b1 (infer-core e1 (dict-set Γ x1 (type->whnf a1 Γ)))] + [b2 (infer-core e2 (dict-set Γ x2 (type->whnf a2 Γ)))]) (if (equiv-type b1 b2 Γ) b1 (err (format "case ~a is not of consistent type!" `(case (,a1 ⊕ ,a2) b1 b2)))))] [t (err (format "calling case on incorrect type ~a" t))])] @@ -183,7 +251,7 @@ ['nil (err (format "unable to infer type of empty list!"))] [`(cons ,e1 ,e2) (let ([t (infer-core e1 Γ)]) - (if (check-core e2 `(List ,t) Γ) `(List ,t) + (if (check/core e2 `(List ,t) Γ) `(List ,t) (err (format "list ~a is not of consistent type!" `(cons ,e1 ,e2)))))] [`(head ,e) (match (infer-core e Γ) @@ -195,61 +263,58 @@ [t (err (format "calling tail on incorrect type ~a" t))])] [`(λ (,x : ,t) ,e) - `(,(expand t Γ) → ,(infer-core e (dict-set Γ x t)))] + `(,(type->whnf t Γ) → ,(infer-core e (dict-set Γ x t)))] [`(,e1 ,e2) (match (infer-core e1 Γ) [`(,t1 → ,t2) - (if (check-core e2 t1 Γ) t2 + (if (check/core e2 t1 Γ) t2 (err (format "inferred argument type ~a does not match arg ~a" t1 e2)))] - [t (err (format "expected → type on application body, got ~a" t))])] - - [e (err (format "inferring an unknown expression ~a" e))])) + [t (err (format "expected → type on application body, got ~a" t))])])) ;; Expands a type alias into weak-head normal form, for literal matching. -;; (expand Type Table[Id, Expr ⊕ Type]): Type -(define (expand t Γ) +(define (type->whnf t Γ) (if (dict-has-key? Γ `(type ,t)) - (expand (dict-ref Γ `(type ,t)) Γ) t)) + (type->whnf (dict-ref Γ `(type ,t)) Γ) t)) ;; Checks if two types are equivalent up to α-conversion in context ;; (equiv-type Expr Expr Table[Sym Expr]): Bool (define (equiv-type e1 e2 Γ) - (equiv-type-core e1 e2 Γ Γ)) -(define (equiv-type-core e1 e2 Γ1 Γ2) + (equiv-type/core e1 e2 Γ Γ)) +(define (equiv-type/core e1 e2 Γ1 Γ2) (match* (e1 e2) ; bound identifiers: if a key exists in the context, look it up [(x1 x2) #:when (dict-has-key? Γ1 x1) - (equiv-type-core (dict-ref Γ1 x1) x2 Γ1 Γ2)] + (equiv-type/core (dict-ref Γ1 x1) x2 Γ1 Γ2)] [(x1 x2) #:when (dict-has-key? Γ2 x2) - (equiv-type-core x1 (dict-ref Γ2 x2) Γ1 Γ2)] + (equiv-type/core x1 (dict-ref Γ2 x2) Γ1 Γ2)] ; check for syntactic equivalence on remaining forms [(`(,l1 ...) `(,l2 ...)) - (foldl (λ (x1 x2 acc) (if (equiv-type-core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)] + (foldl (λ (x1 x2 acc) (if (equiv-type/core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)] [(v1 v2) (equal? v1 v2)])) ;; Checks if two terms are equivalent up to α-conversion in context ;; (equiv-term Expr Expr Table[Sym Expr]): Bool (define (equiv-term e1 e2 Γ) - (equiv-term-core e1 e2 Γ Γ)) -(define (equiv-term-core e1 e2 Γ1 Γ2) + (equiv-term/core e1 e2 Γ Γ)) +(define (equiv-term/core e1 e2 Γ1 Γ2) (match* (e1 e2) ; bound identifiers: if a key exists in the context, look it up [(x1 x2) #:when (dict-has-key? Γ1 x1) - (equiv-term-core (dict-ref Γ1 x1) x2 Γ1 Γ2)] + (equiv-term/core (dict-ref Γ1 x1) x2 Γ1 Γ2)] [(x1 x2) #:when (dict-has-key? Γ2 x2) - (equiv-term-core x1 (dict-ref Γ2 x2) Γ1 Γ2)] + (equiv-term/core x1 (dict-ref Γ2 x2) Γ1 Γ2)] ; function expressions: parameter names can be arbitrary [(`(λ (,x1 : ,t1) ,e1) `(λ (,x2 : ,t2) ,e2)) (let ([name gensym]) - (and (equiv-term-core e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)) - (equiv-term-core t1 t2 Γ1 Γ2)))] + (and (equiv-term/core e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)) + (equiv-term/core t1 t2 Γ1 Γ2)))] [(`(λ ,x1 ,e1) `(λ ,x2 ,e2)) (let ([name gensym]) - (equiv-term-core e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))] + (equiv-term/core e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))] ; check for syntactic equivalence on remaining forms [(`(,l1 ...) `(,l2 ...)) - (foldl (λ (x1 x2 acc) (if (equiv-term-core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)] + (foldl (λ (x1 x2 acc) (if (equiv-term/core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)] [(v1 v2) (equal? v1 v2)])) diff --git a/stlc-fix.rkt b/stlc-fix.rkt index 420aa15..06d0369 100644 --- a/stlc-fix.rkt +++ b/stlc-fix.rkt @@ -1,74 +1,87 @@ #lang racket (require "lib.rkt") (require "base.rkt") +(require (only-in "stlc.rkt" stlc/type?)) ;; The Simply-Typed Lambda Calculus, with general recursion -;; (interpret Expr Context): Value +;; Checks an expression for syntactic well-formedness. +(define/contract (stlc-fix/expr? expr) + (-> any/c boolean?) + (match expr + [x #:when (symbol? x) #t] + [`(fix ,e) (stlc-fix/expr? e)] + [`(λ (,x : ,t) ,e) (and (symbol? x) (stlc/type? t) (stlc-fix/expr? e))] + [`(,e1 ,e2) (and (stlc-fix/expr? e1) (stlc-fix/expr? e2))] + [_ #f])) + +;; Checks a value for syntactic well-formedness. +(define (stlc-fix/value? value) + (match value + [x #:when (symbol? x) #t] + [`(,v1 ,v2) (and (stlc-fix/value? v1) (stlc-fix/value? v2))] + [`(λ ,x ,e ,env) (and (symbol? x) (stlc-fix/expr? e) (dict? env))] + [_ #f])) + +;; Interprets an expression down to a value, in a given context. (define (interpret expr) - (interpret-core (strip (desugar expr)) #hash())) -(define (interpret-core expr Γ) + (interpret/core (desugar expr) #hash())) +(define/contract (interpret/core expr Γ) + (-> stlc-fix/expr? dict? stlc-fix/value?) (match expr ['sole 'sole] - [n #:when (natural? n) n] [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] + [x #:when (symbol? x) x] [`(fix ,e) - (match (interpret-core e Γ) + (match (interpret/core e Γ) [`(λ ,x ,e ,env) ; FIXME: unsure what should be Γ and what should be env - (interpret-core e (dict-set env x `(fix (λ ,x ,e ,Γ))))] + (interpret/core e (dict-set env x `(fix (λ ,x ,e ,Γ))))] [e (err (format "applying fix to unknown expression ~a" e))])] - [`(λ ,id ,body) `(λ ,id ,body ,Γ)] - [`(λ ,id ,body ,env) `(λ ,id ,body ,env)] + [`(λ (,id : ,t) ,body) `(λ ,id ,body ,Γ)] [`(,body ,arg) - (match (interpret-core body Γ) + (match (interpret/core body Γ) [`(λ ,id ,body ,env) - (interpret-core body (dict-set env id (interpret-core arg Γ)))] - [e (err (format "applying arg ~a to unknown expression ~a" arg e))])] + (interpret/core body (dict-set env id (interpret/core arg Γ)))] + [e (err (format "applying arg ~a to unknown expression ~a" arg e))])])) - [e (err (format "interpreting an unknown expression ~a" e))])) - -;; (check Expr Type Context): Bool +;; Checks an expression against some type, in a given context. (define (check expr with) - (check-core (desugar expr) with #hash())) -(define (check-core expr with Γ) + (check/core (desugar expr) with #hash())) +(define/contract (check/core expr with Γ) ; FIXME + (-> stlc-fix/expr? stlc/type? dict? boolean?) (let ([with (if (dict-has-key? Γ with) (dict-ref Γ with) with)]) (match expr [`(fix ,e) - (check-core (infer-core e) `(,with → ,with) Γ)] - + (check/core (infer/core e) `(,with → ,with) Γ)] [`(λ (,x : ,t) ,e) (match with [`(,t1 → ,t2) (and (equal? t1 t) - (check-core e t2 (dict-set Γ x t1)))] + (check/core e t2 (dict-set Γ x t1)))] [_ #f])] + [_ (equal? (infer/core expr Γ) with)]))) - [_ (equal? (infer-core expr Γ) with)]))) - -;; (infer Expr Context): Type +;; Infers a type from some expression, in a given context. (define (infer expr) - (infer-core (desugar expr) #hash())) -(define (infer-core expr Γ) + (infer/core (desugar expr) #hash())) +(define/contract (infer/core expr Γ) + (-> stlc-fix/expr? dict? stlc/type?) (match expr - ['sole 'Unit] - [n #:when (natural? n) 'Nat] [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] - + [f #:when (symbol? f) + (err (format "attempting to infer type of free variable ~a" f))] [`(fix ,e) - (match (infer-core e Γ) + (match (infer/core e Γ) [`(,t → ,t) t] [t (err (format "fix expects a term of type t → t, got ~a" t))])] - [`(λ (,x : ,t) ,e) - `(,t → ,(infer-core e (dict-set Γ x t)))] + `(,t → ,(infer/core e (dict-set Γ x t)))] [`(,e1 ,e2) - (match (infer-core e1 Γ) + (match (infer/core e1 Γ) [`(,t1 → ,t2) - (if (check-core e2 t1 Γ) t2 + (if (check/core e2 t1 Γ) t2 (err (format "inferred argument type ~a does not match arg ~a" t1 e2)))] - [t (err (format "expected → type on application body, got ~a" t))])] - - [e (err (format "inferring an unknown expression ~a" e))])) + [t (err (format "expected → type on application body, got ~a" t))])])) diff --git a/stlc-full.rkt b/stlc-full.rkt index b25b56c..0ea8637 100644 --- a/stlc-full.rkt +++ b/stlc-full.rkt @@ -9,9 +9,12 @@ ;; - impredicative references built on a levels system ;; - explicit level stratification syntax ;; - automatic level collection -;; -;; This system is impredicative. It can be made predicative by tweaking -;; the sections of the code labeled with "KNOB". +;; - [todo] implicit level stratification + +;; Whether the system is *predicative* or *impredicative*. +;; The predicative system disallows quantification over references. +;; The impredicative system allows so by tweaking level rules. +(define impredicative? #f) (define-syntax-rule (print msg) (eprintf "~a~%" msg)) @@ -42,116 +45,101 @@ (define (all? proc lst) (foldl (λ (x acc) (if (proc x) acc #f)) #t lst)) -;; Whether a given level is a syntactically valid level. -;; This does not account for context, and so all symbols are valid levels. -(define (level? level) - (match level - [n #:when (natural? n) #t] - ; Symbols are only valid if previously bound (by `level`). - ; We can't check that here, however. - [s #:when (symbol? s) #t] - ; Levels may be a list of symbols, or a list of symbols followed by a natural. - [`(+ ,l ... ,n) #:when (natural? n) - (all? (λ (s) (symbol? s)) l)] - [`(+ ,l ...) - (all? (λ (s) (symbol? s)) l)] - [_ #f])) - -;; Whether a given type is a syntactically valid type. -;; This does not account for context, and so all symbols are valid types. -(define (type? type) - (match type - [(or 'Unit 'Bool 'Nat) #t] - ; Symbols are only valid if previously bound (by `type` or `μ`). - ; We can't check that here, however. - [s #:when (symbol? s) #t] - [`(Ref ,t) (type? t)] - [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2)) (and (type? t1) (type? t2))] - [`(,t1 → ,l ,t2) (and (type? t1) (level? l) (type? t2))] - [`(μ ,x ,t) (and (symbol? x) (type? t))] - [_ #f])) - -;; Whether a given expression is a syntactically valid expression. +;; Checks an expression for syntactic well-formedness. ;; This does not account for context, and so all symbols are valid exprs. -(define (expr? expr) +(define (stlc-full/expr? expr) (match expr - ['sole #t] + ; Symbols are only valid if previously bound by `λ` or `case` (or if `'sole`). + ; We can't check that here, however. + [x #:when (symbol? x) #t] [n #:when (natural? n) #t] [b #:when (boolean? b) #t] - ; Symbols are only valid if previously bound by `λ` or `case`. - ; We can't check that here, however. - [s #:when (symbol? s) #t] - - [`(,e : ,t) (and (expr? e) (type? t))] + [`(,e : ,t) + (and (stlc-full/expr? e) (stlc-full/type? t))] [`(type ,t1 ,t2 ,e) - (and (type? t1) (type? t2) (expr? e))] - - ; Note that level must only introduce new variables as levels. - [`(level ,l ,e) - (and (symbol? l) (expr? e))] - ; Kind of want to call ⇑ :: on analogy with : - [`(,e ⇑ ,l) - (and (expr? e) (level? l))] - - [(or `(new ,e) `(! ,e)) (expr? e)] - ; [`(ptr ,a) (symbol? a)] - [`(set ,e1 ,e2) (and (expr? e1) (expr? e2))] - - [`(inc ,e) (expr? e)] + (and (stlc-full/type? t1) (stlc-full/type? t2) (stlc-full/expr? e))] + [`(,e :: ,l) + (and (stlc-full/expr? e) (stlc-full/level? l))] + [`(level ,l ,e) ; note that level must only introduce new variables as levels + (and (symbol? l) (stlc-full/expr? e))] + [(or + `(inc ,e) + `(car ,e) `(cdr ,e) + `(inl ,e) `(inr ,e) + `(new ,e) `(! ,e) + `(fold ,e) `(unfold ,e)) + (stlc-full/expr? e)] + [(or + `(pair ,e1 ,e2) + `(set ,e1 ,e2) + `(,e1 ,e2)) + (and (stlc-full/expr? e1) (stlc-full/expr? e2))] [`(if ,c ,e1 ,e2) - (and (expr? c) (expr? e1) (expr? e2))] - - [`(pair ,e1 ,e2) - (and (expr? e1) (expr? e2))] - [(or `(car ,e) `(cdr ,e)) (expr? e)] - - [(or `(inl ,e) `(inr ,e)) (expr? e)] + (and (stlc-full/expr? c) (stlc-full/expr? e1) (stlc-full/expr? e2))] [`(case ,c (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) (and (symbol? x1) (symbol? x2) - (expr? c) (expr? e1) (expr? e2))] - - [(or `(fold ,e) `(unfold ,e)) (expr? e)] - + (stlc-full/expr? c) (stlc-full/expr? e1) (stlc-full/expr? e2))] [`(λ (,x : ,t) ,e) - (and (symbol? x) (type? t) (expr? e))] - [`(,e1 ,e2) (and (expr? e1) (expr? e2))] + (and (symbol? x) (stlc-full/type? t) (stlc-full/expr? e))] [_ #f])) -;; Whether a term is a value or a computation. What's that little rhyme about this again? -;; A value is, a computation/expr/term does? -(define (value? expr) +;; Checks a value for syntactic well-formedness. +;; This does not account for context, and so all symbols are valid values. +;; A value is, a computation/expr/term does... +(define (stlc-full/value? expr) (match expr - ['sole #t] + [x #:when (symbol? x) #t] [n #:when (natural? n) #t] [b #:when (boolean? b) #t] + [`(ptr ,l ,a) + (and (stlc-full/level? l) (symbol? a))] + [(or `(inl ,v) `(inr ,v)) + (stlc-full/value? v)] + [(or `(pair ,v1 ,v2) `(,v1 ,v2)) + (and (stlc-full/value? v1) (stlc-full/value? v2))] + [`(λ (,x : ,t) ,e ,env) + (and (symbol? x) (stlc-full/type? t) (stlc-full/expr? e) (dict? env))] + [_ #f])) - ; [`(,v : ,t) (and (expr? v) (type? t))] - ; [`(type ,t1 ,t2 ,b) - ; (and (type? t1) (type? t2) (value? v))] - - ; [(or `(level ,l ,v) `(,v ⇑ ,l)) - ; (and (level? l) (value? v))] - - [`(ptr ,l ,a) (and (level? l) (symbol? a))] - - [`(pair ,v1 ,v2) - (and (value? v1) (value? v2))] - - [(or `(inl ,v) `(inr ,v)) (value? v)] - - ; [(or `(fold ,v) `(unfold ,v)) (value? v)] +;; Checks a level for syntactic well-formedness. +;; This does not account for context, and so all symbols are valid levels. +(define (stlc-full/level? level) + (match level + ; Symbols are only valid if previously bound (by `level`). + ; We can't check that here, however. + [x #:when (symbol? x) #t] + [n #:when (natural? n) #t] + ; Levels may be a list of symbols, or a list of symbols followed by a natural. + [`(+ ,l ... ,n) #:when (natural? n) + (all? (λ (s) (symbol? s)) l)] + [`(+ ,l ...) + (all? (λ (s) (symbol? s)) l)] + [_ #f])) - [`(λ (,x : ,t) ,e ,env) - (and (symbol? x) (type? t) (expr? e) (dict? env))] +;; Checks a type for syntactic well-formedness. +;; This does not account for context, and so all symbols are valid types. +(define (stlc-full/type? type) + (match type + ; Symbols are only valid if previously bound (by `type` or `μ`). + ; We can't check that here, however. + [x #:when (symbol? x) #t] + [`(Ref ,t) (stlc-full/type? t)] + [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2)) + (and (stlc-full/type? t1) (stlc-full/type? t2))] + [`(,t1 → ,l ,t2) + (and (stlc-full/type? t1) (stlc-full/level? l) (stlc-full/type? t2))] + [`(μ ,x ,t) + (and (symbol? x) (stlc-full/type? t))] [_ #f])) -(define (ptr? expr) +(define (stlc-full/ptr? expr) (match expr - [`(ptr ,l ,a) (and (level? l) (symbol? a))] + [`(ptr ,l ,a) (and (stlc-full/level? l) (symbol? a))] [_ #f])) ;; Creates a new multiset from a list. -(define/contract (list->multiset l) (-> list? dict?) +(define/contract (list->multiset l) + (-> list? dict?) (foldl (λ (x acc) (if (dict-has-key? acc x) @@ -160,20 +148,23 @@ #hash() l)) ;; Creates a new list from a multiset. -(define/contract (multiset->list m) (-> dict? list?) +(define/contract (multiset->list m) + (-> dict? list?) (foldl (λ (x acc) (append acc (build-list (dict-ref m x) (λ (_) x)))) '() (dict-keys m))) ;; Adds a symbol to a multiset. -(define/contract (multiset-add m1 s) (-> dict? symbol? dict?) +(define/contract (multiset-add m1 s) + (-> dict? symbol? dict?) (if (dict-has-key? m1 s) (dict-set m1 s (+ (dict-ref m1 s) 1)) (dict-set m1 s 1))) ;; Queries two multisets for equality. -(define/contract (multiset-eq m1 m2) (-> dict? dict? boolean?) +(define/contract (multiset-eq m1 m2) + (-> dict? dict? boolean?) (if (equal? (length m1) (length m2)) #f (foldl (λ (x acc) @@ -183,7 +174,8 @@ #t (dict-keys m2)))) ;; Unions two multisets. Shared members take the maximum count of each other. -(define/contract (multiset-union m1 m2) (-> dict? dict? dict?) +(define/contract (multiset-union m1 m2) + (-> dict? dict? dict?) (foldl (λ (x acc) (if (dict-has-key? acc x) @@ -192,7 +184,8 @@ m1 (dict-keys m2))) ;; Intersects two multisets. Shared members take the minimum count of each other. -(define/contract (multiset-intersect m1 m2) (-> dict? dict? dict?) +(define/contract (multiset-intersect m1 m2) + (-> dict? dict? dict?) (foldl (λ (x acc) (if (dict-has-key? m1 x) @@ -201,16 +194,18 @@ #hash() (dict-keys m2))) ;; Checks if a level is at its "base" form. -(define/contract (level-base? l) (-> level? boolean?) +(define/contract (level-base? l) + (-> stlc-full/level? boolean?) (match l - [n #:when (natural? n) (zero? n)] [s #:when (symbol? s) #t] + [n #:when (natural? n) (zero? n)] [`(+ ,s ... ,n) #:when (natural? n) (zero? n)] ; should be avoided [`(+ ,s ...) #t])) ;; Syntactic equality between levels is not trivial. ;; This helper function defines it. -(define/contract (level-eq? l1 l2) (-> level? level? boolean?) +(define/contract (level-eq? l1 l2) + (-> stlc-full/level? stlc-full/level? boolean?) (match* (l1 l2) [(n1 n2) #:when (and (natural? n1) (natural? n2)) (equal? n1 n2)] @@ -222,12 +217,13 @@ ;; Levels can carry natural numbers, and so we define a stratification between them. ;; Note: this returns FALSE if the levels are incomparable (i.e. (level-geq 'a 'b)) -(define/contract (level-geq? l1 l2) (-> level? level? boolean?) +(define/contract (level-geq? l1 l2) + (-> stlc-full/level? stlc-full/level? boolean?) (match* (l1 l2) - [(n1 n2) #:when (and (natural? n1) (natural? n2)) - (>= n1 n2)] [(s1 s2) #:when (and (symbol? s1) (symbol? s2)) (equal? s1 s2)] + [(n1 n2) #:when (and (natural? n1) (natural? n2)) + (>= n1 n2)] [(`(+ ,s1 ... ,n1) `(+ ,s2 ... ,n2)) #:when (and (natural? n1) (natural? n2)) (and (level-eq? `(+ ,@s1) `(+ ,@s2)) (level-geq? n1 n2))] [(`(+ ,s1 ... ,n) `(+ ,s2 ...)) #:when (natural? n) @@ -239,12 +235,13 @@ ;; We define a maximum of two levels. ;; This can return one of the two levels or an entirely new level. -(define/contract (level-max l1 l2) (-> level? level? level?) +(define/contract (level-max l1 l2) + (-> stlc-full/level? stlc-full/level? stlc-full/level?) (match* (l1 l2) - [(n1 n2) #:when (and (natural? n1) (natural? n2)) - (max n1 n2)] [(s1 s2) #:when (and (symbol? s1) (symbol? s2)) (if (equal? s1 s2) s1 `(+ ,s1 ,s2))] + [(n1 n2) #:when (and (natural? n1) (natural? n2)) + (max n1 n2)] [(`(+ ,s1 ... ,n1) `(+ ,s2 ... ,n2)) #:when (and (natural? n1) (natural? n2)) (if (equal? s1 s2) `(+ ,@s1 ,(max n1 n2)) @@ -269,7 +266,8 @@ (level-union `(+ ,@s1) `(+ ,@s2))])) ;; A helper function to perform the union of levels. -(define/contract (level-union l1 l2) (-> level-base? level-base? level-base?) +(define/contract (level-union l1 l2) + (-> level-base? level-base? level-base?) (match* (l1 l2) [(0 l) l] [(l 0) l] @@ -277,12 +275,13 @@ `(+ ,@(multiset->list (multiset-union (list->multiset s1) (list->multiset s2))))])) ;; We define addition in terms of our syntactic constructs. -(define/contract (level-add l1 l2) (-> level? level? level?) +(define/contract (level-add l1 l2) + (-> stlc-full/level? stlc-full/level? stlc-full/level?) (match* (l1 l2) - [(n1 n2) #:when (and (natural? n1) (natural? n2)) - (+ n1 n2)] [(s1 s2) #:when (and (symbol? s1) (symbol? s2)) `(+ ,s1 ,s2)] + [(n1 n2) #:when (and (natural? n1) (natural? n2)) + (+ n1 n2)] [(`(+ ,s1 ... ,n1) `(+ ,s2 ... ,n2)) #:when (and (natural? n1) (natural? n2)) (level-add (level-add `(+ ,@s1) `(+ ,@s2)) (+ n1 n2))] [(`(+ ,s1 ... ,n) `(+ ,s2 ...)) #:when (natural? n) @@ -302,7 +301,8 @@ ;; Decrements a level by 1. ;; ASSUMPTION: the level is not a base level (i.e. there is some n to dec) -(define/contract (level-dec l) (-> level? level?) +(define/contract (level-dec l) + (-> stlc-full/level? stlc-full/level?) (match l [n #:when (and (natural? n) (not (zero? n))) (- n 1)] [`(+ ,s ... 1) `(+ ,@s)] @@ -310,18 +310,20 @@ [_ (err (format "attempting to decrement base level ~a" l))])) ;; Returns the "base" form of a level. -(define/contract (level-base l) (-> level? level?) +(define/contract (level-base l) + (-> stlc-full/level? stlc-full/level?) (match l - [n #:when (natural? n) 0] [s #:when (symbol? s) s] + [n #:when (natural? n) 0] [`(+ ,s ... ,n) #:when (natural? n) `(+ ,@s)] [`(+ ,s ...) `(+ ,@s)])) ;; Returns the "offset" portion of a level. -(define/contract (level-offset l) (-> level? level?) +(define/contract (level-offset l) + (-> stlc-full/level? stlc-full/level?) (match l - [n #:when (natural? n) n] [s #:when (symbol? s) 0] + [n #:when (natural? n) n] [`(+ ,s ... ,n) #:when (natural? n) n] [`(+ ,s ...) 0])) @@ -330,30 +332,32 @@ ;; Otherwise, levels are syntactically inferred. ;; ASSUMPTION: the type is well-formed in the given context (i.e. all symbols bound). ;; This is not checked via contracts due to (presumably) massive performance overhead. -(define/contract (level-type t Γ) (-> type? dict? level?) +(define/contract (level-type t Γ) + (-> stlc-full/type? dict? stlc-full/level?) (match t [(or 'Unit 'Bool 'Nat) 0] [s #:when (symbol? s) 0] ; HACK: μ-type variables, not in Γ - [`(Ref ,t) ; KNOB + [`(Ref ,t) (let ([l (level-type t Γ)]) - (if (level-base? l) l - (level-add l 1)))] + (if (and impredicative? (level-base? l)) + l (level-add l 1)))] [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2)) (level-max (level-type t1 Γ) (level-type t2 Γ))] - [`(,t1 → ,l ,t2) ; KNOB + [`(,t1 → ,l ,t2) ; FIXME: knob?? (if (and (level-geq? l (level-type t1 Γ)) (level-geq? l (level-type t2 Γ))) l (err (format "annotated level ~a is less than inferred levels ~a and ~a!")))] [`(μ ,x ,t) (level-type t (dict-set Γ x `(μ ,x ,t)))])) ;; Infers the level of a (well-formed) expression. -(define/contract (level-expr e Γ) (-> expr? dict? level?) +(define/contract (level-expr e Γ) + (-> stlc-full/expr? dict? stlc-full/level?) (match e ['sole 0] [n #:when (natural? n) 0] [b #:when (boolean? b) 0] [x #:when (dict-has-key? Γ x) ; free variables - (level-type (expand-whnf (dict-ref Γ x) Γ) Γ)] + (level-type (type->whnf (dict-ref Γ x) Γ) Γ)] [s #:when (symbol? s) 0] ; local variables [`(,e : ,t) @@ -365,12 +369,12 @@ [`(level ,l ,e) ; NOTE: is this correct? (level-expr e Γ)] - [`(,e ⇑ ,l) + [`(,e :: ,l) (level-add l (level-expr e Γ))] - [`(new ,e) ; KNOB + [`(new ,e) ; FIXME; knob?? (let ([l (level-expr e Γ)]) - (if (level-base? l) l (level-add l 1)))] + (if (level-base? l) l (level-add l 1)))] [`(if ,c ,e1 ,e2) (level-max (level-expr c Γ) @@ -393,7 +397,8 @@ ;; Whether a given type is a semantically valid type. ;; We assume any type in Γ is semantically valid. ;; Otherwise, we would infinitely recurse re: μ. -(define/contract (well-formed? t Γ) (-> type? dict? boolean?) +(define/contract (well-formed? t Γ) + (-> stlc-full/type? dict? boolean?) (match t [(or 'Unit 'Bool 'Nat) #t] [s #:when (symbol? s) (dict-has-key? Γ `(type s))] @@ -406,7 +411,8 @@ (well-formed? t (dict-set Γ `(type ,x) `(μ ,x ,t)))])) ;; Whether a given type at a given level is semantically valid. -(define/contract (well-kinded? t l Γ) (-> type? level? dict? boolean?) +(define/contract (well-kinded? t l Γ) + (-> stlc-full/type? stlc-full/level? dict? boolean?) (match t [(or 'Unit 'Bool 'Nat) (level-geq? l 0)] [s #:when (symbol? s) @@ -428,16 +434,17 @@ ;; Our heap is a Dict[Level, List[Dict[Addr, Expr]]]. In other words: ;; - the heap is first stratified by algebraic levels, i.e. α, β, α+β, etc ;; - those heaps are then stratified by n: the level as a natural number. -;; - this is -(define (heap? heap) +#; +(define (stlc-full/heap? heap) (match heap [`((,level-var . (,subheap ...)) ...) - (and (all? (λ (l) (level? l)) level-var) + (and (all? (λ (l) (stlc-full/level? l)) level-var) (all? (λ (n) (dict? n)) subheap))] [_ #f])) ;; Extends a list to have at least n+1 elements. Takes a default-generating procedure. -(define/contract (list-extend l n default) (-> list? natural? procedure? list?) +(define/contract (list-extend l n default) + (-> list? natural? procedure? list?) (if (>= n (length l)) (build-list (+ n 1) (λ (k) @@ -447,91 +454,101 @@ l)) ;; Models the allocation of an (unsized) memory pointer at an arbitrary heap level. -(define/contract (alloc! Σ l) (-> dict? level? ptr?) +(define/contract (alloc! Σ l) + (-> dict? stlc-full/level? stlc-full/ptr?) (let ([addr (gensym)] [base (level-base l)] [offset (level-offset l)]) - (if (dict-has-key? Σ base) - (let ([base-heap (dict-ref Σ base)]) - (if (>= offset (length base-heap)) - (dict-set! Σ base ; FIXME: we probably should error if location is occupied - (let ([offset-heap (make-hash)]) - (dict-set! offset-heap addr 'null) ; FIXME: probably should not be null - (list-set (list-extend base-heap offset make-hash) offset offset-heap))) - (let ([offset-heap (list-ref base-heap offset)]) - (dict-set! offset-heap addr 'null)))) - (dict-set! Σ base + (if (dict-has-key? Σ base) + (let ([base-heap (dict-ref Σ base)]) + (if (>= offset (length base-heap)) + (dict-set! Σ base ; FIXME: we probably should error if location is occupied (let ([offset-heap (make-hash)]) - (dict-set! offset-heap addr 'null) - (list-set (build-list (+ offset 1) (λ (_) (make-hash))) offset offset-heap)))) - `(ptr ,l ,addr))) + (dict-set! offset-heap addr 'null) ; FIXME: probably should not be null + (list-set (list-extend base-heap offset make-hash) offset offset-heap))) + (let ([offset-heap (list-ref base-heap offset)]) + (dict-set! offset-heap addr 'null)))) + (dict-set! Σ base + (let ([offset-heap (make-hash)]) + (dict-set! offset-heap addr 'null) + (list-set (build-list (+ offset 1) (λ (_) (make-hash))) offset offset-heap)))) + `(ptr ,l ,addr))) ;; Updates the heap given a pointer to a memory location and a value. -(define/contract (write! Σ p v) (-> dict? ptr? value? ptr?) +(define/contract (write! Σ p v) + (-> dict? stlc-full/ptr? stlc-full/value? stlc-full/ptr?) (match p [`(ptr ,l ,a) (let ([base (level-base l)] [offset (level-offset l)]) - (if (dict-has-key? Σ base) - (let ([base-heap (dict-ref Σ base)]) - (if (< offset (length base-heap)) - (dict-set! (list-ref base-heap offset) a v) - (err (format "writing to invalid memory location ~a!" p)))) - (err (format "writing to invalid memory location ~a!" p))))]) + (if (dict-has-key? Σ base) + (let ([base-heap (dict-ref Σ base)]) + (if (< offset (length base-heap)) + (dict-set! (list-ref base-heap offset) a v) + (err (format "writing to invalid memory location ~a!" p)))) + (err (format "writing to invalid memory location ~a!" p))))]) p) ;; Returns the corresponding value of a pointer to a memory location on the heap. -(define/contract (read! Σ p) (-> dict? ptr? value?) +(define/contract (read! Σ p) + (-> dict? stlc-full/ptr? stlc-full/value?) (match p [`(ptr ,l ,a) (let ([base (level-base l)] [offset (level-offset l)]) - (if (dict-has-key? Σ base) - (let ([base-heap (dict-ref Σ base)]) - (if (< offset (length base-heap)) - (dict-ref (list-ref base-heap offset) a) - (err (format "reading from invalid memory location ~a!" p)))) - (err (format "reading from invalid memory location ~a!" p))))])) + (if (dict-has-key? Σ base) + (let ([base-heap (dict-ref Σ base)]) + (if (< offset (length base-heap)) + (dict-ref (list-ref base-heap offset) a) + (err (format "reading from invalid memory location ~a!" p)))) + (err (format "reading from invalid memory location ~a!" p))))])) ;; Models the deallocation of all memory locations of level `l` or higher. ;; For complexity and performance purposes, we only support deallocating base levels. -(define/contract (dealloc! Σ l) (-> dict? level-base? void?) +(define/contract (dealloc! Σ l) + (-> dict? level-base? void?) (for-each - (λ (key) (if (level-geq? key l) (dict-remove! Σ key) (void))) + (λ (key) + (if (level-geq? key l) + (dict-remove! Σ key) (void))) (dict-keys Σ))) ;; Whether two types are equivalent in a context. ;; We define equivalence as equivalence up to α-renaming. -(define/contract (equiv-type t1 t2 Γ) (-> type? type? dict? boolean?) - (equiv-type-core t1 t2 Γ Γ)) -(define (equiv-type-core t1 t2 Γ1 Γ2) +(define/contract (equiv-type t1 t2 Γ) + (-> stlc-full/type? stlc-full/type? dict? boolean?) + (equiv-type/core t1 t2 Γ Γ)) +(define (equiv-type/core t1 t2 Γ1 Γ2) (match* (t1 t2) ; bound identifiers: if a key exists in the context, look it up [(x1 x2) #:when (dict-has-key? Γ1 `(type ,x1)) - (equiv-type-core (dict-ref Γ1 `(type ,x1)) x2 Γ1 Γ2)] + (equiv-type/core (dict-ref Γ1 `(type ,x1)) x2 Γ1 Γ2)] [(x1 x2) #:when (dict-has-key? Γ2 `(type ,x2)) - (equiv-type-core x1 (dict-ref Γ2 `(type ,x2)) Γ1 Γ2)] + (equiv-type/core x1 (dict-ref Γ2 `(type ,x2)) Γ1 Γ2)] ; recursive types: self-referential names can be arbitrary [(`(μ ,x1 ,t1) `(μ ,x2 ,t2)) (let ([name gensym]) - (equiv-type-core t1 t2 (dict-set Γ1 `(type ,x1) name) (dict-set Γ2 `(type ,x2) name)))] + (equiv-type/core t1 t2 (dict-set Γ1 `(type ,x1) name) (dict-set Γ2 `(type ,x2) name)))] ; check for syntactic equivalence on remaining forms [(`(,l1 ...) `(,l2 ...)) - (foldl (λ (x1 x2 acc) (if (equiv-type-core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)] + (foldl (λ (x1 x2 acc) (if (equiv-type/core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)] [(v1 v2) (equal? v1 v2)])) ;; Whether two expressions are equivalent in a context. ;; We define equivalence as equivalence up to α-renaming. -; (define/contract (equiv-expr e1 e2 Γ) (-> expr? expr? dict? boolean?) +; (define/contract (equiv-expr e1 e2 Γ) +; (-> stlc-full/expr? stlc-full/expr? dict? boolean?) ; (equiv-expr-core e1 e2 Γ Γ)) ; (define (equiv-expr-core e1 e2 Γ1 Γ2) ; (match* (e1 e2))) ;; Expands a type alias into weak-head normal form, for literal matching. -(define/contract (expand-whnf t Γ) (-> type? dict? type?) +(define/contract (type->whnf t Γ) + (-> stlc-full/type? dict? stlc-full/type?) (if (dict-has-key? Γ `(type ,t)) - (expand-whnf (dict-ref Γ `(type ,t)) Γ) t)) + (type->whnf (dict-ref Γ `(type ,t)) Γ) t)) ;; Replaces all references to a type alias with another alias. -(define/contract (replace-type type key value) (-> type? type? type? type?) +(define/contract (replace-type type key value) + (-> stlc-full/type? stlc-full/type? stlc-full/type? stlc-full/type?) (match type ; Do not accidentally replace shadowed bindings [`(μ ,x _) #:when (equal? x key) type] @@ -541,218 +558,216 @@ ;; Evaluates an expression to a value. ;; Follows the call-by-value evaluation strategy. -(define/contract (call-by-value expr) (-> expr? value?) - (cbv-core expr #hash() (make-hash))) -(define (cbv-core expr Γ Σ) ; ℓ +(define (call-by-value expr) + (cbv/core (desugar expr) #hash() (make-hash))) +(define/contract (cbv/core expr Γ Σ) ; ℓ + (-> stlc-full/expr? dict? dict? stlc-full/value?) (match expr ['sole 'sole] [n #:when (natural? n) n] [b #:when (boolean? b) b] [p #:when (dict-has-key? Σ p) p] [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] + [f #:when (symbol? f) f] [`(,e : ,t) - (cbv-core e Γ Σ)] + (cbv/core e Γ Σ)] [`(type ,t1 ,t2 ,e) - (cbv-core e (dict-set Γ `(type ,t1) t2) Σ)] + (cbv/core e (dict-set Γ `(type ,t1) t2) Σ)] ; The (level ...) syntax introduces new level *variables*. [`(level ,l ,e) - (let ([v (cbv-core e (dict-set Γ `(level ,l) 'level) Σ)]) - (dealloc! Σ l) v)] ; they are then freed at the end of scope - [`(,e ⇑ ,l) - (cbv-core e Γ Σ)] + (let ([v (cbv/core e (dict-set Γ `(level ,l) 'level) Σ)]) + (dealloc! Σ l) v)] ; they are then freed at the end of scope + [`(,e :: ,l) + (cbv/core e Γ Σ)] [`(new ,e) (let ([p (alloc! Σ (level-expr e Γ))]) - (write! Σ p (cbv-core e Γ Σ)))] + (write! Σ p (cbv/core e Γ Σ)))] [`(! ,e) - (match (cbv-core e Γ Σ) + (match (cbv/core e Γ Σ) [`(ptr ,l ,a) (read! Σ `(ptr ,l ,a))] [e (err (format "attempting to deref unknown expression ~a, expected ptr" e))])] [`(set ,e1 ,e2) ; FIXME: we do NOT check levels before writing here - (match (cbv-core e1 Γ Σ) - [`(ptr ,l ,a) (write! Σ `(ptr ,l ,a) (cbv-core e2 Γ Σ))] + (match (cbv/core e1 Γ Σ) + [`(ptr ,l ,a) (write! Σ `(ptr ,l ,a) (cbv/core e2 Γ Σ))] [e (err (format "attempting to write to unknown expression ~a, expected ptr" e))])] [`(inc ,e) - (match (cbv-core e Γ Σ) + (match (cbv/core e Γ Σ) [n #:when (natural? n) (+ n 1)] [e (err (format "incrementing an unknown value ~a" e))])] [`(if ,c ,e1 ,e2) - (match (cbv-core c Γ Σ) - ['#t (cbv-core e1 Γ Σ)] - ['#f (cbv-core e2 Γ Σ)] + (match (cbv/core c Γ Σ) + ['#t (cbv/core e1 Γ Σ)] + ['#f (cbv/core e2 Γ Σ)] [e (err (format "calling if on unknown expression ~a" e))])] [`(pair ,e1 ,e2) - `(pair ,(cbv-core e1 Γ Σ) ,(cbv-core e2 Γ Σ))] + `(pair ,(cbv/core e1 Γ Σ) ,(cbv/core e2 Γ Σ))] [`(car ,e) - (match (cbv-core e Γ Σ) + (match (cbv/core e Γ Σ) [`(pair ,e1 ,e2) e1] [e (err (format "calling car on unknown expression ~a" e))])] [`(cdr ,e) - (match (cbv-core e Γ Σ) + (match (cbv/core e Γ Σ) [`(pair ,e1 ,e2) e2] [e (err (format "calling cdr on unknown expression ~a" e))])] [`(inl ,e) - `(inl ,(cbv-core e Γ Σ))] + `(inl ,(cbv/core e Γ Σ))] [`(inr ,e) - `(inr ,(cbv-core e Γ Σ))] + `(inr ,(cbv/core e Γ Σ))] [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) - (match (cbv-core e Γ Σ) - [`(inl ,e) (cbv-core e1 (dict-set Γ x1 e) Σ)] - [`(inr ,e) (cbv-core e2 (dict-set Γ x2 e) Σ)] + (match (cbv/core e Γ Σ) + [`(inl ,e) (cbv/core e1 (dict-set Γ x1 e) Σ)] + [`(inr ,e) (cbv/core e2 (dict-set Γ x2 e) Σ)] [e (err (format "calling case on unknown expression ~a" e))])] - [`(fold ,e) `(fold ,(cbv-core e Γ Σ))] + [`(fold ,e) `(fold ,(cbv/core e Γ Σ))] [`(unfold ,e) - (match (cbv-core e Γ Σ) + (match (cbv/core e Γ Σ) [`(fold ,e) e] [e (err (format "attempting to unfold unknown expression ~a" e))])] [`(λ (,x : ,t) ,e) `(λ (,x : ,t) ,e ,Γ)] [`(,e1 ,e2) - (match (cbv-core e1 Γ Σ) + (match (cbv/core e1 Γ Σ) [`(λ (,x : ,t) ,e1 ,env) - (cbv-core e1 (dict-set env x (cbv-core e2 Γ Σ)) Σ)] - [e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])] - - [e (err (format "attempting to interpret unknown expression ~a" e))])) + (cbv/core e1 (dict-set env x (cbv/core e2 Γ Σ)) Σ)] + [e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])])) ;; Checks that an expression is of a type, and returns #t or #f, or a bubbled-up error. ;; `with` must be a type in weak-head normal form for structural matching. -(define/contract (check expr with) (-> expr? type? boolean?) - (check-core expr with #hash())) -(define (check-core expr with Γ) +(define (check expr with) + (check/core (desugar expr) with #hash())) +(define/contract (check/core expr with Γ) + (-> stlc-full/expr? stlc-full/type? dict? boolean?) (match expr - ['sole 'Unit] - [n #:when (natural? n) 'Nat] - [b #:when (boolean? b) 'Bool] - ; We expand into weak-head normal form as the binding may be whatever. - [x #:when (dict-has-key? Γ x) - (expand-whnf (dict-ref Γ x) Γ)] - [`(type ,t1 ,t2 ,e) - (check-core e with (dict-set Γ `(type ,t1) t2))] + (check/core e with (dict-set Γ `(type ,t1) t2))] [`(level ,l ,e) ; We add the level to the context just to note it is valid. - (check-core e with (dict-set Γ `(level ,l) 'level))] + (check/core e with (dict-set Γ `(level ,l) 'level))] [`(new ,e) (match with - [`(Ref ,t) (check-core e t Γ)] + [`(Ref ,t) (check/core e t Γ)] [_ #f])] [`(! ,e) - (check-core e `(Ref ,with) Γ)] + (check/core e `(Ref ,with) Γ)] [`(if ,c ,e1 ,e2) - (and (check-core c 'Bool Γ) - (check-core e1 with Γ) (check-core e2 with Γ))] + (and (check/core c 'Bool Γ) + (check/core e1 with Γ) (check/core e2 with Γ))] [`(pair ,e1 ,e2) (match with - [`(,t1 × ,t2) (and (check-core e1 t1 Γ) (check-core e2 t2 Γ))] + [`(,t1 × ,t2) (and (check/core e1 t1 Γ) (check/core e2 t2 Γ))] [_ #f])] [`(inl ,e) (match with - [`(,t1 ⊕ ,t2) (check-core e t1 Γ)] + [`(,t1 ⊕ ,t2) (check/core e t1 Γ)] [_ #f])] [`(inr ,e) (match with - [`(,t1 ⊕ ,t2) (check-core e t2 Γ)] + [`(,t1 ⊕ ,t2) (check/core e t2 Γ)] [_ #f])] ; We do not technically need case in check form. ; We keep it here to avoid needing type annotations on `c`. [`(case ,c (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) - (match (infer-core c Γ) + (match (infer/core c Γ) [`(,a1 ⊕ ,a2) - (and (check-core e1 with (dict-set Γ x1 a1)) - (check-core e2 with (dict-set Γ x2 a2)))] + (and (check/core e1 with (dict-set Γ x1 a1)) + (check/core e2 with (dict-set Γ x2 a2)))] [_ #f])] [`(fold ,e) (match with - [`(μ ,x ,t) (check-core e t (dict-set Γ `(type ,x) `(μ ,x ,t)))] + [`(μ ,x ,t) (check/core e t (dict-set Γ `(type ,x) `(μ ,x ,t)))] [_ #f])] [`(λ (,x : ,t) ,e) (match with - [`(,t1 → ,l ,t2) ; KNOB - (and (equiv-type t t1 Γ) (check-core e t2 (dict-set Γ x t)) - (> l (level-expr e (dict-set Γ x t1))))] - [`(,t1 → ,t2) (err (format "missing level annotation on function type"))] + [`(,t1 → ,l ,t2) + (and (equiv-type t t1 Γ) (check/core e t2 (dict-set Γ x t)) + (if impredicative? + (> l (level-expr e (dict-set Γ x t1))) + (>= l (level-expr e (dict-set Γ x t1)))))] [_ #f])] - [_ (equiv-type (infer-core expr Γ) with Γ)])) + [_ (equiv-type (infer/core expr Γ) with Γ)])) ;; Infers a type from a given expression, if possible. Errors out otherwise. ;; Returns a type in weak-head normal form for structural matching. -(define/contract (infer expr) (-> expr? type?) - (infer-core expr #hash())) +(define (infer expr) + (infer/core (desugar expr) #hash())) ;; Γ is our context: a dictionary from symbols to types??? i forget actually ;; note: our context plays many roles. -(define (infer-core expr Γ) +(define/contract (infer/core expr Γ) + (-> stlc-full/expr? dict? stlc-full/type?) (match expr ['sole 'Unit] [n #:when (natural? n) 'Nat] [b #:when (boolean? b) 'Bool] ; We expand into weak-head normal form as the binding may be to another binding. [x #:when (dict-has-key? Γ x) - (expand-whnf (dict-ref Γ x) Γ)] + (type->whnf (dict-ref Γ x) Γ)] + [f #:when (symbol? f) + (err (format "attempting to infer type of free variable ~a" f))] [`(type ,t1 ,t2 ,e) - (infer-core e (dict-set Γ `(type ,t1) t2))] + (infer/core e (dict-set Γ `(type ,t1) t2))] [`(,e : ,t) - (if (check-core e (expand-whnf t Γ) Γ) (expand-whnf t Γ) + (if (check/core e (type->whnf t Γ) Γ) (type->whnf t Γ) (err (format "expression ~a is not of annotated type ~a" e t)))] [`(level ,l ,e) ; We add the level to the context just to note it is valid. - (infer-core e (dict-set Γ `(level ,l) 'level))] - [`(,e ⇑ ,l) ; We retrieve the level from the context to check it is valid. + (infer/core e (dict-set Γ `(level ,l) 'level))] + [`(,e :: ,l) ; We retrieve the level from the context to check it is valid. (if (dict-has-key? Γ `(level ,(level-base l))) - (infer-core e Γ) + (infer/core e Γ) (err (format "level ~a not found in context, was it introduced?")))] [`(new ,e) - `(Ref ,(infer-core e Γ))] + `(Ref ,(infer/core e Γ))] [`(ptr ,a) (err (format "cannot infer type from raw pointer ~a" `(ptr ,a)))] [`(! ,e) - (match (infer-core e Γ) + (match (infer/core e Γ) [`(Ref ,t) t] [t (err (format "attempting to deref term ~a of type ~a" e t))])] [`(set ,e1 ,e2) ; FIXME: this does not account for explicit allocation syntax! - (match (infer-core e1 Γ) ; should we check levels? + (match (infer/core e1 Γ) ; should we check levels? [`(Ref ,t) - (if (check-core e2 t Γ) 'Unit + (if (check/core e2 t Γ) 'Unit (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type" - e1 t e2 (infer-core e2 Γ))))] + e1 t e2 (infer/core e2 Γ))))] [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] [`(inc ,e) - (if (check-core e 'Nat Γ) 'Nat - (err (format "calling inc on incorrect type ~a, expected Nat" (infer-core e Γ))))] + (if (check/core e 'Nat Γ) 'Nat + (err (format "calling inc on incorrect type ~a, expected Nat" (infer/core e Γ))))] [`(if ,c ,e1 ,e2) - (if (check-core c 'Bool Γ) - (let ([t (infer-core e1 Γ)]) - (if (check-core e2 t Γ) t - (err (format "if ~a is not of consistent type!" - `(if Bool ,t ,(infer-core e2 Γ)))))) + (if (check/core c 'Bool Γ) + (let ([t (infer/core e1 Γ)]) + (if (check/core e2 t Γ) t + (err (format "if ~a is not of consistent type!" + `(if Bool ,t ,(infer/core e2 Γ)))))) (err (format "if ~a has incorrect type ~a on condition, expected Bool" - c (infer-core c Γ))))] + c (infer/core c Γ))))] [`(pair ,e1 ,e2) - `(,(infer-core e1 Γ) × ,(infer-core e2 Γ))] + `(,(infer/core e1 Γ) × ,(infer/core e2 Γ))] [`(car ,e) - (match (infer-core e Γ) + (match (infer/core e Γ) [`(,t1 × ,t2) t1] [t (err (format "calling car on incorrect type ~a, expected a product" t))])] [`(cdr ,e) - (match (infer-core e Γ) + (match (infer/core e Γ) [`(,t1 × ,t2) t2] [t (err (format "calling cdr on incorrect type ~a, expected a product" t))])] @@ -761,34 +776,32 @@ [`(inr ,e) (err (format "unable to infer the type of a raw inr"))] [`(case ,c (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) - (match (infer-core c Γ) + (match (infer/core c Γ) [`(,a1 ⊕ ,a2) - (let ([b1 (infer-core e1 (dict-set Γ x1 a1))] - [b2 (infer-core e2 (dict-set Γ x2 a2))]) - (if (equiv-type b1 b2 Γ) b1 - (err (format "case ~a is not of consistent type!" - `(case (,a1 ⊕ ,a2) (,x1 ⇒ ,b1) (,x2 ⇒ ,b2))))))] + (let ([b1 (infer/core e1 (dict-set Γ x1 a1))] + [b2 (infer/core e2 (dict-set Γ x2 a2))]) + (if (equiv-type b1 b2 Γ) b1 + (err (format "case ~a is not of consistent type!" + `(case (,a1 ⊕ ,a2) (,x1 ⇒ ,b1) (,x2 ⇒ ,b2))))))] [t (err (format "case has incorrect type ~a on condition, expected a sum" t))])] [`(unfold ,e) - (match (infer-core e Γ) + (match (infer/core e Γ) [`(μ ,x ,t) (replace-type t x `(μ ,x ,t))] [t (err (format "expected ~a to be of recursive type, got ~a" e t))])] - [`(λ (,x : ,t1) ,e) ; KNOB - (let* ([t2 (infer-core e (dict-set Γ x t1))] - [t1 (expand-whnf t1 Γ)] [l (+ 1 (level-expr e (dict-set Γ x t1)))]) - `(,t1 → ,l ,t2))] + [`(λ (,x : ,t1) ,e) + (let* ([t2 (infer/core e (dict-set Γ x t1))] + [t1 (type->whnf t1 Γ)] + [l (level-expr e (dict-set Γ x t1))]) + `(,t1 → ,(if impredicative? (+ l 1) l) ,t2))] [`(,e1 ,e2) - (match (infer-core e1 Γ) + (match (infer/core e1 Γ) [`(,t1 → ,l ,t2) ; should we check levels here? probably redundant - (if (check-core e2 t1 Γ) t2 + (if (check/core e2 t1 Γ) t2 (err (format "inferred argument type ~a does not match arg ~a of type ~a" - t1 e2 (infer-core e2 Γ))))] - [`(,t1 → ,t2) (err (format "missing level annotation on function type"))] - [t (err (format "expected → type on application body, got ~a" t))])] - - [_ (err (format "attempting to infer an unknown expression ~a" expr))])) + t1 e2 (infer/core e2 Γ))))] + [t (err (format "expected → type on application body, got ~a" t))])])) ;; Define aliases from higher-level constructs to lower-level core forms. @@ -798,7 +811,7 @@ ['⟨⟩ 'sole] [`(ref ,e) (desugar `(new ,e))] [`(deref ,e) (desugar `(! ,e))] - [`(,e :: ,k) (desugar `(,e ⇑ ,k))] + [`(,e ⇑ ,k) (desugar `(,e :: ,k))] ; set-with-continuation [`(set ,e1 ,e2 ,in) @@ -826,7 +839,7 @@ ;; (type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))) (check-equal? - (call-by-value (desugar ' + (call-by-value ' (let (next : ((μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) → 1 (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)))) (λ (self : (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))) @@ -839,31 +852,31 @@ (pair 413 (pair (new (inr sole)) (new (inr sole)))))) - (next my_list))))) + (next my_list)))) '(inr sole)) (check-equal? - (infer (desugar ' + (infer ' (type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) (λ (self : DoublyLinkedList) (case (unfold self) (some ⇒ ((! (cdr (cdr some))) : DoublyLinkedList)) - (none ⇒ ((fold (inr sole)) : DoublyLinkedList))))))) + (none ⇒ ((fold (inr sole)) : DoublyLinkedList)))))) '((μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) → 1 (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)))) (check-true (equiv-type - (infer (desugar ' + (infer ' (type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) (λ (self : DoublyLinkedList) (case (unfold self) (some ⇒ (! (cdr (cdr some)))) - (none ⇒ ((fold (inr sole)) : DoublyLinkedList))))))) + (none ⇒ ((fold (inr sole)) : DoublyLinkedList)))))) '(DoublyLinkedList → 1 DoublyLinkedList) #hash(((type DoublyLinkedList) . (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)))))) (check-true - (check (desugar ' + (check ' (type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) (let (get : (DoublyLinkedList → 1 (Nat ⊕ Unit))) (λ self @@ -885,5 +898,5 @@ (pair 413 (pair (new ((fold (inr sole)) : DoublyLinkedList)) (new ((fold (inr sole)) : DoublyLinkedList)))))) - (prev my_list))))))) + (prev my_list)))))) 'DoublyLinkedList)) diff --git a/stlc-hor.rkt b/stlc-hor.rkt new file mode 100644 index 0000000..ad568c9 --- /dev/null +++ b/stlc-hor.rkt @@ -0,0 +1,154 @@ +#lang racket +(require "lib.rkt") +(require "base.rkt") +(provide (all-defined-out)) + +;; The Simply-Typed Lambda Calculus with higher-order references + +;; Whether the system is *predicative* or *impredicative*. +;; The predicative system disallows quantification over references. +;; The impredicative system allows so by tweaking level rules. +(define impredicative? #f) + +;; Checks an expression for syntactic well-formedness. +(define (stlc-hor/expr? expr) + (match expr + [x #:when (symbol? x) #t] + [n #:when (natural? n) #t] + [(or `(new ,e) `(! ,e)) (stlc-hor/expr? e)] + [(or `(set ,e1 ,e2) `(,e1 ,e2)) (and (stlc-hor/expr? e1) (stlc-hor/expr? e2))] + [`(λ (,x : ,t) ,e) (and (symbol? x) (stlc-hor/type? t) (stlc-hor/expr? e))] + [_ #f])) + +;; Checks a type for syntactic well-formedness. +(define (stlc-hor/type? type) + (match type + [t #:when (symbol? t) #t] + [`(,t1 → ,k ,t2) (and (natural? k) (stlc-hor/type? t1) (stlc-hor/type? t2))] + [_ #f])) + +;; Checks a value for syntactic well-formedness. +(define (stlc-hor/value? value) + (match value + [x #:when (symbol? x) #t] + [n #:when (natural? n) #t] + [`(,v1 ,v2) (and (stlc-hor/value? v1) (stlc-hor/value? v2))] + [`(λ ,x ,e ,env) (and (symbol? x) (stlc-hor/expr? e) (dict? env))] + [_ #f])) + +;; Interprets an expression down to a value, in a given context. +(define (interpret expr) + (interpret/core (desugar expr) #hash() (make-hash))) +(define/contract (interpret/core expr Γ Σ) + (-> stlc-hor/expr? dict? dict? stlc-hor/value?) + (match expr + [r #:when (dict-has-key? Σ r) r] + [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] + [f #:when (symbol? f) f] + + [`(new ,e) + (let ([r (gensym)]) + (dict-set! Σ r e) r)] + [`(! ,e) + (let ([r (interpret/core e Γ Σ)]) + (if (dict-has-key? Σ r) + (interpret/core (dict-ref Σ r) Γ Σ) + (err (format "attempting to deref unknown reference ~a" r))))] + [`(set ,e1 ,e2) + (let ([r (interpret/core e1 Γ Σ)]) + (if (dict-has-key? Σ r) (dict-set! Σ r (interpret/core e2 Γ Σ)) + (err (format "attempting to update unknown reference ~a" r)))) + 'sole] + + [`(λ ,x ,e) `(λ ,x ,e ,Γ)] + [`(,e1 ,e2) + (match (interpret/core e1 Γ Σ) + [`(λ ,x ,e1 ,env) + (interpret/core e1 (dict-set env x (interpret/core e2 Γ Σ)) Σ)] + [e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])])) + +;; Checks an expression against some type, in a given context. +(define (check expr with) + (check/core (desugar expr) with #hash())) +(define/contract (check/core expr with Γ) + (-> stlc-hor/expr? stlc-hor/type? dict? boolean?) + (match expr + [`(new ,e) + (match with + [`(Ref ,t) (check/core e t Γ)] + [_ #f])] + [`(! ,e) + (check/core e `(Ref ,with) Γ)] + + [`(λ (,x : ,t) ,e) + (match with + [`(,t1 → ,k ,t2) + (and (equal? t t1) (check/core e t2 (dict-set Γ x t)) + (if impredicative? + (> k (level-expr e (dict-set Γ x t1))) + (>= k (level-expr e (dict-set Γ x t1)))))] + [_ #f])] + + [_ (equal? (infer/core expr Γ) with)])) + +;; Infers a type from some expression, in a given context. +(define (infer expr) + (infer/core (desugar expr) #hash())) +(define/contract (infer/core expr Γ) + (-> stlc-hor/expr? dict? stlc-hor/type?) + (match expr + ['sole 'Unit] + [n #:when (natural? n) 'Nat] + [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] + [f #:when (symbol? f) + (err (format "attempting to infer type of free variable ~a" f))] + + [`(new ,e) `(Ref ,(infer/core e Γ))] + [`(! ,e) + (match (infer/core e Γ) + [`(Ref ,t) t] + [t (err "attempting to deref term not of Ref type!")])] + [`(set ,e1 ,e2) + (match (infer/core e1 Γ) + [`(Ref ,t) + (if (check/core e2 t Γ) 'Unit + (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type" + e1 t e2 (infer/core e2 Γ))))] + [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] + + [`(λ (,x : ,t1) ,e) + (let ([t2 (infer/core e (dict-set Γ x t1))] + [k (level-expr e (dict-set Γ x t1))]) + `(,t1 → ,(if impredicative? (+ k 1) k) ,t2))] + [`(,e1 ,e2) + (match (infer/core e1 Γ) + [`(,t1 → ,k ,t2) + (if (check/core e2 t1 Γ) t2 + (err (format "inferred argument type ~a does not match arg ~a of type ~a" + t1 e2 (infer/core e2 Γ))))] + [t (err (format "expected → type on application body, got ~a" t))])])) + +;; Get the level associated with a type. This is known at compile time. +(define/contract (level-type type) + (-> stlc-hor/type? natural?) + (match type + [(or 'Unit 'Nat) 0] + [`(Ref ,t) + (let ([k (level-type t)]) + (if (and impredicative? (zero? k)) 0 (+ 1 k)))] + [`(,t1 → ,k ,t2) + (if (and (>= k (level-type t1)) (>= k (level-type t2))) k + (err (format "annotated level ~a is less than inferred levels of ~a and ~a!" + k t1 t2)))] + [t (err (format "attempting to infer the level of unknown type ~a" t))])) + +;; Get the level of an arbitrary expression. This is not known until runtime. +(define/contract (level-expr expr Γ) + (-> stlc-hor/expr? dict? natural?) + (match expr + ['sole 0] + [n #:when (natural? n) 0] + [x #:when (dict-has-key? Γ x) (level-type (dict-ref Γ x))] + [(or `(new ,e) `(! ,e) `(λ (,_ : ,_) ,e)) (level-expr e Γ)] + [(or `(set ,e1 ,e2) `(,e1 ,e2)) (max (level-expr e1 Γ) (level-expr e2 Γ))] + [x #:when (symbol? x) 0])) ; local variables, not in Γ diff --git a/stlc-imp.rkt b/stlc-imp.rkt deleted file mode 100644 index c550359..0000000 --- a/stlc-imp.rkt +++ /dev/null @@ -1,112 +0,0 @@ -#lang racket -(require "lib.rkt") -(require "base.rkt") -(require (only-in "stlc-ref.rkt" interpret)) -(provide check infer level-type level-body) - -;; The Simply-Typed Lambda Calculus with higher-order *impredicative* references - -; Γ, x: τ₁ ⊢ e: τ₂ k > max-level(Γ, τ₁, τ₂) -; --------------------------------------------- -; Γ ⊢ λx:τ₁.e : τ₁ →ᵏ τ₂ - -; Γ ⊢ e₁: τ₁ →ᵏ τ₂ Γ ⊢ e₂: τ₁ -; -------------------------------- -; Γ ⊢ (e₁ e₂): τ₂ - -; -------------------------- -; Nat::Type₀, Unit::Type₀ - -; τ::Type₀ -; --------------- -; Ref τ :: Type₀ - -; τ::Typeᵢ, i ≥ 0 -; --------------- -; Ref τ :: Typeᵢ₊₁ - -; τ₁::Typeᵢ, τ₂::Typeⱼ, k > max-level(τ₁, τ₂) -; ----------------------------------------- -; τ₁ →ᵏ τ₂ :: Typeₖ -(require (only-in "stlc-ref.rkt" interpret)) - -;; (check Expr Type Table[Sym, Type]): Bool -(define (check expr with) - (check-core (desugar expr) with #hash())) -(define (check-core expr with Γ) - (match expr - [`(new ,e) - (match with - [`(Ref ,t) (check-core e t Γ)] - [_ #f])] - [`(! ,e) - (check-core e `(Ref ,with) Γ)] - - [`(λ (,x : ,t) ,e) - (match with - [`(,t1 → ,k ,t2) - (and (equal? t t1) (check-core e t2 (dict-set Γ x t)) - (> k (level-body e (dict-set Γ x t1))))] ; KNOB - [_ #f])] - - [_ (equal? (infer-core expr Γ) with)])) - -;; (infer Expr Table[Sym, Type]): Type -(define (infer expr) - (infer-core (desugar expr) #hash())) -(define (infer-core expr Γ) - (match expr - ['sole 'Unit] - [n #:when (natural? n) 'Nat] - [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] - - [`(new ,e) `(Ref ,(infer-core e Γ))] - [`(! ,e) - (match (infer-core e Γ) - [`(Ref ,t) t] - [t (err "attempting to deref term not of Ref type!")])] - [`(set ,e1 ,e2) - (match (infer-core e1 Γ) - [`(Ref ,t) - (if (check-core e2 t Γ) 'Unit - (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type" - e1 t e2 (infer-core e2 Γ))))] - [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] - - [`(λ (,x : ,t1) ,e) - (let* ([t2 (infer-core e (dict-set Γ x t1))] - [k (+ 1 (level-body e (dict-set Γ x t1)))]) ; KNOB - `(,t1 → ,k ,t2))] - [`(,e1 ,e2) - (match (infer-core e1 Γ) - [`(,t1 → ,k ,t2) - (if (check-core e2 t1 Γ) t2 - (err (format "inferred argument type ~a does not match arg ~a of type ~a" - t1 e2 (infer-core e2 Γ))))] - [t (err (format "expected → type on application body, got ~a" t))])] - - [e (err (format "attempting to infer an unknown expression ~a" e))])) - -;; (level-type Type): Natural -(define (level-type t) - (match t - ['Unit 0] - ['Nat 0] - [`(,t1 → ,k ,t2) - (if (and (>= k (level-type t1)) (>= k (level-type t2))) k - (err (format "annotated level ~a is less than inferred levels of ~a and ~a!" - k t1 t2)))] - [`(Ref ,t) - (let ([k (level-type t)]) - (if (zero? k) 0 (+ 1 k)))] ; KNOB - [t (err (format "attempting to infer the level of unknown type ~a" t))])) - -;; (level-body Expr Table[Sym, Type]): Natural -(define (level-body e Γ) - (match e - ['sole 0] - [n #:when (natural? n) 0] - [x #:when (dict-has-key? Γ x) (level-type (dict-ref Γ x))] - [(or `(new ,e) `(! ,e) `(λ (,_ : ,_) ,e)) (level-body e Γ)] - [(or `(set ,e1 ,e2) `(,e1 ,e2)) (max (level-body e1 Γ) (level-body e2 Γ))] - [x #:when (symbol? x) 0])) ; local variables, not in Γ diff --git a/stlc-pred.rkt b/stlc-pred.rkt deleted file mode 100644 index 197ad74..0000000 --- a/stlc-pred.rkt +++ /dev/null @@ -1,84 +0,0 @@ -#lang racket -(require "lib.rkt") -(require "base.rkt") -(require (only-in "stlc-ref.rkt" interpret)) -(provide check infer level-type level-body) - -;; The Simply-Typed Lambda Calculus with higher-order *predicative* references - -;; (check Expr Type Table[Sym, Type]): Bool -(define (check expr with) - (check-core (desugar expr) with #hash())) -(define (check-core expr with Γ) - (match expr - [`(new ,e) - (match with - [`(Ref ,t) (check-core e t Γ)] - [_ #f])] - - [`(λ (,x : ,t) ,e) - (match with - [`(,t1 → ,k ,t2) - (and (equal? t t1) (check-core e t2 (dict-set Γ x t1)) - (>= k (level-body e (dict-set Γ x t1))))] ; KNOB - [_ #f])] - - [_ (equal? (infer-core expr Γ) with)])) - -;; (infer Expr Table[Sym, Type]): Type -(define (infer expr) - (infer-core (desugar expr) #hash())) -(define (infer-core expr Γ) - (match expr - ['sole 'Unit] - [n #:when (natural? n) 'Nat] - [x #:when (dict-has-key? Γ x) - (dict-ref Γ x)] - - [`(new ,e) `(Ref ,(infer-core e Γ))] - [`(! ,e) - (match (infer-core e Γ) - [`(Ref ,t) t] - [t (err "attempting to deref term not of Ref type!")])] - [`(set ,e1 ,e2) - (match (infer-core e1 Γ) - [`(Ref ,t) - (if (check-core e2 t Γ) 'Unit - (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type" - e1 t e2 (infer-core e2 Γ))))] - [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] - - [`(λ (,x : ,t1) ,e) - (let* ([t2 (infer-core e (dict-set Γ x t1))] - [k (level-body e (dict-set Γ x t1))]) ; KNOB - `(,t1 → ,k ,t2))] - [`(,e1 ,e2) - (match (infer-core e1 Γ) - [`(,t1 → ,k ,t2) - (if (check-core e2 t1 Γ) t2 - (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer-core e2 Γ))))] - [t (err (format "expected → type on application body, got ~a" t))])] - - [e (err (format "attempting to infer an unknown expression ~a" e))])) - -;; (level-type Type): Natural -(define (level-type t) - (match t - [(or 'Unit 'Nat) 0] - [`(,t1 → ,k ,t2) - (if (and (>= k (level-type t1)) (>= k (level-type t2))) k - (err (format "annotated level ~a is less than inferred levels of ~a and ~a!" - k t1 t2)))] - [`(Ref ,t) (+ 1 (level-type t))] ; (KNOB) - [t (err (format "attempting to infer the level of unknown type ~a" t))])) - -;; (level-body Expr Table[Sym, Type]): Natural -(define (level-body e Γ) - (match e - ['sole 0] - [n #:when (natural? n) 0] - [x #:when (dict-has-key? Γ x) - (level-type (dict-ref Γ x))] - [(or `(new ,e) `(! ,e) `(λ (,_ : ,_) ,e)) (level-body e Γ)] - [(or `(set ,e1 ,e2) `(,e1 ,e2)) (max (level-body e1 Γ) (level-body e2 Γ))] - [x #:when (symbol? x) 0])) diff --git a/stlc-rec.rkt b/stlc-rec.rkt index 84103bb..3266150 100644 --- a/stlc-rec.rkt +++ b/stlc-rec.rkt @@ -5,87 +5,104 @@ ;; The Simply-Typed Lambda Calculus with iso-recursive types -; Γ ⊢ e: [x ↦ μx.t] t -; ------------------------ -; Γ ⊢ fold [μx.t] e: μx.t - -; Γ ⊢ e: μx.t -; ----------------------------------- -; Γ ⊢ unfold [μx.t] e: [x ↦ μx.t] t - -;; (interpret Expr Table[Sym, Expr]): Value +;; Checks an expression for syntactic well-formedness. +(define (stlc-rec/expr? expr) + (match expr + [x #:when (symbol? x) #t] + [(or `(fold ,e) `(unfold ,e)) (stlc-rec/expr? e)] + [`(,e1 ,e2) (and (stlc-rec/expr? e1) (stlc-rec/expr? e2))] + [`(λ (,x : ,t) ,e) (and (symbol? x) (stlc-rec/type? t) (stlc-rec/expr? e))] + [_ #f])) + +;; Checks a type for syntactic well-formedness. +(define (stlc-rec/type? type) + (match type + [t #:when (symbol? t) #t] + [`(,t1 → ,t2) (and (stlc-rec/type? t1) (stlc-rec/type? t2))] + [_ #f])) + +;; Checks a value for syntactic well-formedness. +(define (stlc-rec/value? value) + (match value + [x #:when (symbol? x) #t] + [`(,v1 ,v2) (and (stlc-rec/value? v1) (stlc-rec/value? v2))] + [`(λ ,x ,e ,env) (and (symbol? x) (stlc-rec/expr? e) (dict? env))] + [_ #f])) + +;; Interprets an expression down to a value, in a given context. (define (interpret expr) - (interpret-core (strip (desugar expr)) #hash())) -(define (interpret-core expr Γ) + (interpret/core (desugar expr) #hash())) +(define/contract (interpret/core expr Γ) + (-> stlc-rec/expr? dict? stlc-rec/value?) (match expr ['sole 'sole] - [n #:when (natural? n) n] [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] + [n #:when (natural? n) n] + [f #:when (symbol? f) f] - [`(fold ,e) `(fold ,(interpret-core e Γ))] + [`(fold ,e) `(fold ,(interpret/core e Γ))] [`(unfold ,e) - (match (interpret-core e Γ) + (match (interpret/core e Γ) [`(fold ,e) e] [e `(unfold e)])] - [`(λ ,x ,e) `(λ ,x ,e ,Γ)] + [`(λ (,x : ,t) ,e) `(λ ,x ,e ,Γ)] [`(,e1 ,e2) - (match (interpret-core e1 Γ) + (match (interpret/core e1 Γ) [`(λ ,x ,e ,env) - (interpret-core e (dict-set env x (interpret-core e2 Γ)))] - [e (err (format "applying arg ~a to unknown expression ~a" e2 e))])] - - [e (err (format "interpreting an unknown expression ~a" e))])) + (interpret/core e (dict-set env x (interpret/core e2 Γ)))] + [e (err (format "applying arg ~a to unknown expression ~a" e2 e))])])) -;; (check Expr Type Table[Sym, Type]): Bool +;; Checks an expression against some type, in a given context. (define (check expr with) - (check-core (desugar expr) with #hash())) -(define (check-core expr with Γ) + (check/core (desugar expr) with #hash())) +(define/contract (check/core expr with Γ) + (-> stlc-rec/expr? stlc-rec/type? dict? boolean?) (match expr [`(fold (μ ,x ,t) ,e) (match with - [`(μ ,x ,t) (check-core e t (dict-set Γ x `(μ ,x ,t)))] + [`(μ ,x ,t) (check/core e t (dict-set Γ x `(μ ,x ,t)))] [_ #f])] [`(λ (,x : ,t) ,e) (match with [`(,t1 → ,t2) - (and (equal? t1 t) (check-core e t2 (dict-set Γ x t1)))] + (and (equal? t1 t) (check/core e t2 (dict-set Γ x t1)))] [_ #f])] - [_ (equal? (infer-core expr Γ) with)])) + [_ (equal? (infer/core expr Γ) with)])) -;; (infer Expr Table[Sym, Type]): Type +;; Infers a type from some expression, in a given context. (define (infer expr) - (infer-core (desugar expr) #hash())) -(define (infer-core expr Γ) + (infer/core (desugar expr) #hash())) +(define/contract (infer/core expr Γ) + (-> stlc-rec/expr? dict? stlc-rec/type?) (match expr ['sole 'Unit] - [n #:when (natural? n) 'Nat] - [b #:when (boolean? b) 'Bool] [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] + [b #:when (boolean? b) 'Bool] + [n #:when (natural? n) 'Nat] + [f #:when (symbol? f) + (err (format "attempting to infer type of free variable ~a" f))] [`(fold (μ ,x ,t) ,e) - (if (check-core e t (dict-set Γ x `(μ ,x ,t))) `(μ ,x ,t) + (if (check/core e t (dict-set Γ x `(μ ,x ,t))) `(μ ,x ,t) (err (format "expected ~a to be of type ~a, got ~a" e t (infer e (dict-set Γ x `(μ ,x ,t))))))] [`(unfold (μ ,x ,t) ,e) - (if (check-core e `(μ ,x ,t)) (replace t x `(μ ,x ,t)) + (if (check/core e `(μ ,x ,t)) (replace t x `(μ ,x ,t)) (err (format "expected ~a to be of type ~a, got ~a" - e `(μ ,x ,t) (infer-core e Γ))))] + e `(μ ,x ,t) (infer/core e Γ))))] [`(λ (,x : ,t) ,e) - `(,t → ,(infer-core e (dict-set Γ x t)))] - + `(,t → ,(infer/core e (dict-set Γ x t)))] [`(,e1 ,e2) - (match (infer-core e1 Γ) + (match (infer/core e1 Γ) [`(,t1 → ,t2) - (if (check-core e2 t1 Γ) t2 + (if (check/core e2 t1 Γ) t2 (err (format "inferred argument type ~a does not match arg ~a" t1 e2)))] - [t (err (format "expected → type on application body, got ~a" t))])] - - [e (err (format "attempting to infer an unknown expression ~a" e))])) + [t (err (format "expected → type on application body, got ~a" t))])])) ;; Replace all references to an expression with a value. (define (replace expr key value) diff --git a/stlc-ref.rkt b/stlc-ref.rkt index d0afec0..4f5ac91 100644 --- a/stlc-ref.rkt +++ b/stlc-ref.rkt @@ -1,92 +1,120 @@ #lang racket (require "lib.rkt") (require "base.rkt") -(provide interpret check infer) +(provide (all-defined-out)) ;; The Simply-Typed Lambda Calculus with references -;; (interpret Expr Table[Sym, Expr] Table[Sym, Expr]): Value +; todo: rewrite to use call-by-reference or call-by-value or call-by-name explicitly + +;; Checks an expression for syntactic well-formedness. +(define (stlc-ref/expr? expr) + (match expr + [x #:when (symbol? x) #t] + [n #:when (natural? n) #t] + [(or `(new ,e) `(! ,e)) (stlc-ref/expr? e)] + [(or `(set ,e1 ,e2) `(,e1 ,e2)) (and (stlc-ref/expr? e1) (stlc-ref/expr? e2))] + [`(λ (,x : ,t) ,e) (and (symbol? x) (stlc-ref/type? t) (stlc-ref/expr? e))] + [_ #f])) + +;; Checks a type for syntactic well-formedness. +(define (stlc-ref/type? type) + (match type + [t #:when (symbol? t) #t] + [`(Ref ,t) (stlc-ref/type? t)] + [`(,t1 → ,t2) (and (stlc-ref/type? t1) (stlc-ref/type? t2))] + [_ #f])) + +;; Checks a value for syntactic well-formedness. +(define (stlc-ref/value? value) + (match value + [x #:when (symbol? x) #t] + [n #:when (natural? n) #t] + [`(,v1 ,v2) (and (stlc-ref/value? v1) (stlc-ref/value? v2))] + [`(λ ,x ,e ,env) (and (symbol? x) (stlc-ref/expr? e) (dict? env))] + [_ #f])) + +;; Interprets an expression down to a value, in a given context. (define (interpret expr) - (interpret-core (strip (desugar expr)) #hash() (make-hash))) -(define (interpret-core expr Γ Σ) + (interpret/core (desugar expr) #hash() (make-hash))) +(define/contract (interpret/core expr Γ Σ) + (-> stlc-ref/expr? dict? dict? stlc-ref/value?) (match expr - ['sole 'sole] - [n #:when (natural? n) n] [r #:when (dict-has-key? Σ r) r] [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] + [f #:when (symbol? f) f] [`(new ,e) (let ([r (gensym)]) (dict-set! Σ r e) r)] [`(! ,e) - (let ([r (interpret-core e Γ Σ)]) + (let ([r (interpret/core e Γ Σ)]) (if (dict-has-key? Σ r) - (interpret-core (dict-ref Σ r) Γ Σ) + (interpret/core (dict-ref Σ r) Γ Σ) (err (format "attempting to deref unknown reference ~a" r))))] [`(set ,e1 ,e2) - (let ([r (interpret-core e1 Γ Σ)]) - (if (dict-has-key? Σ r) (dict-set! Σ r (interpret-core e2 Γ Σ)) + (let ([r (interpret/core e1 Γ Σ)]) + (if (dict-has-key? Σ r) (dict-set! Σ r (interpret/core e2 Γ Σ)) (err (format "attempting to update unknown reference ~a" r)))) 'sole] - [`(λ ,x ,e) `(λ ,x ,e ,Γ)] - [`(λ ,x ,e ,env) `(λ ,x ,e ,env)] ; ??? + [`(λ (,x : ,t) ,e) `(λ ,x ,e ,Γ)] [`(,e1 ,e2) - (match (interpret-core e1 Γ Σ) + (match (interpret/core e1 Γ Σ) [`(λ ,x ,e1 ,env) - (interpret-core e1 (dict-set env x (interpret-core e2 Γ Σ)) Σ)] - [e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])] - - [e (err (format "attempting to interpret unknown expression ~a" e))])) + (interpret/core e1 (dict-set env x (interpret/core e2 Γ Σ)) Σ)] + [e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])])) -;; (check Expr Type Table[Sym, Type]): Bool +;; Checks an expression against some type, in a given context. (define (check expr with) - (check-core (desugar expr) with #hash())) -(define (check-core expr with Γ) + (check/core (desugar expr) with #hash())) +(define/contract (check/core expr with Γ) + (-> stlc-ref/expr? stlc-ref/type? dict? boolean?) (match expr [`(new ,e) (match with - [`(Ref ,t) (check-core e t Γ)] + [`(Ref ,t) (check/core e t Γ)] [_ #f])] - [`(! ,e) (check-core e `(Ref ,with) Γ)] + [`(! ,e) (check/core e `(Ref ,with) Γ)] [`(λ (,x : ,t) ,e) (match with [`(,t1 → ,t2) - (and (equal? t1 t) (check-core e t2 (dict-set Γ x t1)))] + (and (equal? t1 t) (check/core e t2 (dict-set Γ x t1)))] [_ #f])] - [_ (equal? (infer-core expr Γ) with)])) + [_ (equal? (infer/core expr Γ) with)])) -;; (infer Expr Table[Sym, Type]): Type +;; Infers a type from some expression, in a given context. (define (infer expr) - (infer-core (desugar expr) #hash())) -(define (infer-core expr Γ) + (infer/core (desugar expr) #hash())) +(define/contract (infer/core expr Γ) + (-> stlc-ref/expr? dict? stlc-ref/type?) (match expr ['sole 'Unit] - [n #:when (natural? n) 'Nat] [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] + [n #:when (natural? n) n] + [f #:when (symbol? f) + (err (format "attempting to infer type of free variable ~a" f))] - [`(new ,e) `(Ref ,(infer-core e Γ))] + [`(new ,e) `(Ref ,(infer/core e Γ))] [`(! ,e) - (match (infer-core e Γ) + (match (infer/core e Γ) [`(Ref ,t) t] [t (err "attempting to deref term not of Ref type!")])] [`(set ,e1 ,e2) - (match (infer-core e1 Γ) + (match (infer/core e1 Γ) [`(Ref ,t) - (if (check-core e2 t Γ) 'Unit + (if (check/core e2 t Γ) 'Unit (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type" - e1 t e2 (infer-core e2 Γ))))] + e1 t e2 (infer/core e2 Γ))))] [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] [`(λ (,x : ,t) ,e) - `(,t → ,(infer-core e (dict-set Γ x t)))] + `(,t → ,(infer/core e (dict-set Γ x t)))] [`(,e1 ,e2) - (match (infer-core e1 Γ) + (match (infer/core e1 Γ) [`(,t1 → ,t2) - (if (check-core e2 t1 Γ) t2 + (if (check/core e2 t1 Γ) t2 (err (format "inferred argument type ~a does not match arg ~a" t1 e2)))] - [t (err (format "expected → type on application body, got ~a" t))])] - - [e (err (format "attempting to infer an unknown expression ~a" e))])) + [t (err (format "expected → type on application body, got ~a" t))])])) @@ -1,23 +1,48 @@ #lang racket (require "lib.rkt") (require "base.rkt") -(provide interpret check infer) +(provide (all-defined-out)) ;; The Simply-Typed Lambda Calculus -;; (interpret Expr Context): Value -(define (interpret expr [Γ #hash()]) - (match (strip expr) +;; Checks an expression for syntactic well-formedness. +(define (stlc/expr? expr) + (match expr + [x #:when (symbol? x) #t] + [`(,e1 ,e2) (and (stlc/expr? e1) (stlc/expr? e2))] + [`(λ (,x : ,t) ,e) (and (symbol? x) (stlc/type? t) (stlc/expr? e))] + [_ #f])) + +;; Checks a type for syntactic well-formedness. +(define (stlc/type? type) + (match type + [t #:when (symbol? t) #t] + [`(,t1 → ,t2) (and (stlc/type? t1) (stlc/type? t2))] + [_ #f])) + +;; Checks a value for syntactic well-formedness. +(define (stlc/value? value) + (match value + [x #:when (symbol? x) #t] + [`(,v1 ,v2) (and (stlc/value? v1) (stlc/value? v2))] + [`(λ ,x ,e ,env) (and (symbol? x) (stlc/expr? e) (dict? env))] + [_ #f])) + +;; Interprets an expression down to a value, in a given context. +(define/contract (interpret expr [Γ #hash()]) + (->* (stlc/expr?) (dict?) stlc/value?) + (match expr [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] - [`(λ ,x ,e) `(λ ,x ,e ,Γ)] + [f #:when (symbol? f) f] + [`(λ (,x : ,t) ,e) `(λ ,x ,e ,Γ)] [`(,e1 ,e2) (match (interpret e1 Γ) [`(λ ,x ,e ,env) (interpret e (dict-set env x (interpret e2 Γ)))] - [e `(,e ,(interpret e2 Γ))])] - [e e])) + [e `(,e ,(interpret e2 Γ))])])) -;; (check Expr Type Context): Bool -(define (check expr with [Γ #hash()]) +;; Checks an expression against some type, in a given context. +(define/contract (check expr with [Γ #hash()]) + (->* (stlc/expr? stlc/type?) (dict?) boolean?) (match expr [`(λ (,x : ,t) ,e) (match with @@ -26,16 +51,19 @@ [_ #f])] [_ (equal? with (infer with Γ))])) -;; (infer Expr Context): Type -(define (infer expr [Γ #hash()]) +;; Infers a type from some expression, in a given context. +(define/contract (infer expr [Γ #hash()]) + (->* (stlc/expr?) (dict?) stlc/type?) (match expr [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] - [`(λ (,x : ,t) ,e) - `(,t → ,(infer e (dict-set Γ x t)))] + [f #:when (symbol? f) + (err (format "attempting to infer type of free variable ~a" f))] [`(,e1 ,e2) (match (infer e1 Γ) [`(,t1 → ,t2) (if (check e2 t1 Γ) t2 (err (format "inferred argument type ~a does not match arg ~a" t1 e2)))] [t (err (format "expected → type on application body, got ~a" t))])] - [e (err (format "attempting to infer an unknown expression ~a" e))])) + [`(λ (,x : ,t) ,e) + `(,t → ,(infer e (dict-set Γ x t)))])) + diff --git a/tests/stlc-imp.rkt b/tests/stlc-imp.rkt deleted file mode 100644 index 44e0c17..0000000 --- a/tests/stlc-imp.rkt +++ /dev/null @@ -1,29 +0,0 @@ -#lang racket -(require (except-in rackunit check)) -(require "../stlc-imp.rkt") - -(define-test-suite landins-knot - (check-exn - exn:fail? - (λ () (infer ' - (let (id : (Nat → 1 Nat)) (λ x x) - (let (r : (Ref (Nat → 0 Nat))) (new id) - (let (f : (Nat → 1 Nat)) (λ x ((! r) x)) - (set r f - (f 0)))))))) - - (check-eq? ; fixme: this should fail - (infer ' - (let (id : (Nat → 0 Nat)) (λ x x) - (let (r : (Ref (Nat → 0 Nat))) (new id) - (let (f : (Nat → 1 Nat)) (λ x ((! r) x)) - (f 0))))) - 'Nat) - - (check-true - (check ' - (let (id : (Nat → 0 Nat)) (λ x x) - (let (r : (Ref (Nat → 0 Nat))) (new id) - (let (f : (Nat → 1 Nat)) (λ x ((! r) x)) - (f 0)))) - 'Nat))) diff --git a/tests/stlc-pred.rkt b/tests/stlc-pred.rkt deleted file mode 100644 index f7afc43..0000000 --- a/tests/stlc-pred.rkt +++ /dev/null @@ -1,29 +0,0 @@ -#lang racket -(require (except-in rackunit check)) -(require "../stlc-pred.rkt") - -(define-test-suite landins-knot - (check-exn - exn:fail? - (λ () (infer ' - (let (id : (Nat → 0 Nat)) (λ x x) - (let (r : (Ref (Nat → 0 Nat))) (new id) - (let (f : (Nat → 1 Nat)) (λ x ((! r) x)) - (set r f - (f 0)))))))) - - (check-eq? - (infer ' - (let (id : (Nat → 0 Nat)) (λ x x) - (let (r : (Ref (Nat → 0 Nat))) (new id) - (let (f : (Nat → 1 Nat)) (λ x ((! r) x)) - (f 0))))) - 'Nat) - - (check-true - (check ' - (let (id : (Nat → 0 Nat)) (λ x x) - (let (r : (Ref (Nat → 0 Nat))) (new id) - (let (f : (Nat → 1 Nat)) (λ x ((! r) x)) - (f 0)))) - 'Nat))) diff --git a/tests/stlc.rkt b/tests/stlc.rkt index 154e77d..cfec36f 100644 --- a/tests/stlc.rkt +++ b/tests/stlc.rkt @@ -2,7 +2,7 @@ (require (except-in rackunit check)) (require "../stlc.rkt") -(check-equal? (interpret '(λ x x)) '(λ x x #hash())) -(check-equal? (interpret '((λ a a) (x y))) '(x y)) -(check-equal? (interpret '((λ a (x y)) (λ z z))) '(x y)) -(check-equal? (interpret '((λ a (a y)) x)) '(x y)) +(check-equal? (interpret '(λ (x : Foo) x)) '(λ x x #hash())) +(check-equal? (interpret '((λ (a : Bar) a) (x y))) '(x y)) +(check-equal? (interpret '((λ (a : Bat) (x y)) (λ (z : Bingus) z))) '(x y)) +(check-equal? (interpret '((λ (a : Baz) (a y)) x)) '(x y)) |