Check Typed Jerboa effect calls
ober
e0c9ce978fce6008dfc734ceeb241ee5f80f7344
--- a/docs/jerboa-to-rust.md +++ b/docs/jerboa-to-rust.md @@ -292,8 +292,10 @@ Typed Jerboa effects should influence generated Rust: - `unsafe`: requires generated unsafe block with audit marker Current landing: typed def forms can carry parsed `#:effects (...)` -annotations. The Rust backend does not use them yet; effect checking and -effect-aware lowering remain future work. +annotations. The checker validates effect names and same-module call +relationships, so pure functions cannot call effectful functions and effectful +callers must cover every callee effect. The Rust backend does not use effects +yet; effect-aware lowering remains future work. The Rust backend should avoid `panic!` for Typed Jerboa errors. Use explicit `Result` values and convert failures into Jerboa conditions at the boundary. --- a/docs/typed-jerboa.md +++ b/docs/typed-jerboa.md @@ -404,8 +404,11 @@ Pure functions should not call effectful functions. Effectful functions can call pure functions. Higher-level functions should accumulate effects from callees. Current landing: the parser preserves optional `#:effects (...)` annotations on -typed defs as `typed-def-effects`. The checker does not yet enforce pure versus -effectful call relationships; that is the next Milestone 5 step. +typed defs as `typed-def-effects`. The checker validates effect names, rejects +duplicate effects, requires `pure` to appear by itself, and enforces same-module +call relationships: a caller may only call functions whose effects are covered +by the caller's own effect list. Empty effects and `#:effects (pure)` both mean +pure. ## Memory Model @@ -883,7 +886,9 @@ Minimum excluded features: - Add effect annotations. Parsed `#:effects (...)` lists now land on typed def AST nodes as `typed-def-effects`. -- Check pure/effectful call relationships. +- Check pure/effectful call relationships. Same-module calls now require the + caller's effect list to cover the callee's effects; pure callers reject + effectful callees. - Add linear resource types. - Model FFI handles. The current generated wrapper layer models same-module record and variant handles as tagged opaque values, exposes explicit handle --- a/lib/jerboa/typed/checker.ss +++ b/lib/jerboa/typed/checker.ss @@ -19,10 +19,11 @@ (jerboa typed parser)) (defstruct typed-check-error (kind message detail)) - (defstruct typed-call-sig (param-types return-type)) + (defstruct typed-call-sig (param-types return-type effects)) (def *call-env* (make-parameter '())) (def *variant-env* (make-parameter '())) + (def *current-effects* (make-parameter '())) (def builtin-type-names '(Unit Bool Char Int Nat Fixnum Float String Bytes Symbol Keyword)) @@ -34,6 +35,9 @@ (Result . 2) (Pair . 2))) + (def allowed-effects + '(pure alloc mut io ffi throw block qt unsafe)) + (def any-value-type (gensym "typed-any")) (def (make-check-error kind message detail) @@ -65,6 +69,14 @@ "Make every branch produce the same type."] [(operand-type-mismatch) "Use operands whose types match the primitive operation."] + [(unknown-effect) + "Use one of the supported effects: pure, alloc, mut, io, ffi, throw, block, qt, or unsafe."] + [(duplicate-effect) + "List each effect at most once."] + [(bad-effect-combination) + "Use pure by itself, or omit it and list the concrete effects."] + [(effect-mismatch) + "Add the callee effects to the caller's #:effects list, or call the effectful function from an effectful boundary."] [(bad-call-arity) "Pass exactly the number of arguments required by the typed function, constructor, accessor, or predicate."] [(argument-type-mismatch) @@ -124,6 +136,64 @@ [else (loop (cdr rest) (cons (car rest) seen) dups)]))) + (def (all-symbols? xs) + (and (list? xs) + (let loop ([rest xs]) + (cond + [(null? rest) #t] + [(symbol? (car rest)) (loop (cdr rest))] + [else #f])))) + + (def (unknown-effects effects) + (let loop ([rest effects] [out '()]) + (cond + [(null? rest) (reverse out)] + [(memq (car rest) allowed-effects) + (loop (cdr rest) out)] + [else (loop (cdr rest) (cons (car rest) out))]))) + + (def (pure-combined? effects) + (and (memq 'pure effects) + (not (null? (cdr effects))))) + + (def (effect-list-valid-for-flow? effects) + (and (all-symbols? effects) + (null? (unknown-effects effects)) + (null? (duplicates effects)) + (not (pure-combined? effects)))) + + (def (normalize-effects effects) + (if (memq 'pure effects) '() effects)) + + (def (effect-subset? needed available) + (let ([available (normalize-effects available)] + [needed (normalize-effects needed)]) + (let loop ([rest needed]) + (cond + [(null? rest) #t] + [(memq (car rest) available) (loop (cdr rest))] + [else #f])))) + + (def (effect-errors effects) + (append + (if (all-symbols? effects) + (map (lambda (effect) + (make-check-error 'unknown-effect + "unknown effect" + effect)) + (unknown-effects effects)) + (list (make-check-error 'bad-effect + "effects must be symbols" + effects))) + (duplicate-errors 'duplicate-effect + "duplicate effect" + effects) + (if (pure-combined? effects) + (list (make-check-error 'bad-effect-combination + "pure cannot be combined with other effects" + effects)) + '()))) + (def (duplicate-errors kind message xs) (map (lambda (x) (make-check-error kind message x)) (duplicates xs))) @@ -199,16 +269,17 @@ (cons (typed-def-name decl) (make-typed-call-sig (map typed-param-type (typed-def-params decl)) - (typed-def-return-type decl))))) + (typed-def-return-type decl) + (typed-def-effects decl))))) (def builtin-call-signatures (list (cons 'string-length - (make-typed-call-sig (list 'String) 'Nat)) + (make-typed-call-sig (list 'String) 'Nat '())) (cons 'string-append - (make-typed-call-sig (list 'String 'String) 'String)) + (make-typed-call-sig (list 'String 'String) 'String '())) (cons 'bytevector-length - (make-typed-call-sig (list 'Bytes) 'Nat)))) + (make-typed-call-sig (list 'Bytes) 'Nat '())))) (def (field-types fields) (map typed-field-type fields)) @@ -223,13 +294,17 @@ [accessor-name (symbol-append prefix "-" field-name)] [accessor (cons accessor-name - (make-typed-call-sig (list record-name) field-type))]) + (make-typed-call-sig + (list record-name) + field-type + '()))]) (if (typed-field-mutable? field) (list accessor (cons (symbol-append accessor-name "-set!") (make-typed-call-sig (list record-name field-type) - 'Unit))) + 'Unit + '()))) (list accessor)))) (typed-record-fields record)))) @@ -239,22 +314,23 @@ (append (list (cons (symbol-append "make-" record-name) - (make-typed-call-sig (field-types fields) record-name)) + (make-typed-call-sig (field-types fields) record-name '())) (cons (symbol-append record-name "?") - (make-typed-call-sig (list any-value-type) 'Bool))) + (make-typed-call-sig (list any-value-type) 'Bool '()))) (record-field-call-signatures record)))) (def (variant-case-call-signature variant-name case) (cons (typed-variant-case-name case) (make-typed-call-sig (field-types (typed-variant-case-fields case)) - variant-name))) + variant-name + '()))) (def (variant-call-signatures variant) (let ([variant-name (typed-variant-name variant)]) (cons (cons (symbol-append variant-name "?") - (make-typed-call-sig (list any-value-type) 'Bool)) + (make-typed-call-sig (list any-value-type) 'Bool '())) (map (lambda (case) (variant-case-call-signature variant-name case)) (typed-variant-cases variant))))) @@ -354,6 +430,7 @@ (duplicate-errors 'duplicate-param "duplicate parameter name" (map typed-param-name (typed-def-params def))) + (effect-errors (typed-def-effects def)) (append-map (lambda (param) (check-type (typed-param-type param) type-names)) (typed-def-params def)) @@ -782,6 +859,17 @@ (list name (car expected) (car actual))) out))]))) + (def (call-effect-errors name callee-effects caller-effects) + (if (and (effect-list-valid-for-flow? callee-effects) + (effect-list-valid-for-flow? caller-effects) + (not (effect-subset? callee-effects caller-effects))) + (list (make-check-error 'effect-mismatch + "callee effects are not covered by caller" + (list name + (normalize-effects callee-effects) + (normalize-effects caller-effects)))) + '())) + (def (infer-function-call name args env type-names expr) (let ([sig (lookup-name name (*call-env*))]) (if (not sig) @@ -798,12 +886,19 @@ (let-values ([(actual-types arg-errors) (infer-args args env type-names)]) (let ([type-errors - (argument-type-errors name expected-types actual-types)]) + (argument-type-errors name expected-types actual-types)] + [effect-errors + (call-effect-errors + name + (typed-call-sig-effects sig) + (*current-effects*))]) (values - (if (and (null? arg-errors) (null? type-errors)) + (if (and (null? arg-errors) + (null? type-errors) + (null? effect-errors)) (typed-call-sig-return-type sig) #f) - (append arg-errors type-errors))))))))) + (append arg-errors type-errors effect-errors))))))))) (def (infer-expression expr env type-names) (cond @@ -857,10 +952,13 @@ (def (check-def-body def type-names) (let-values ([(actual-type body-errors) - (infer-body - (typed-def-body def) - (param-env (typed-def-params def)) - type-names)]) + (parameterize ([*current-effects* + (normalize-effects + (typed-def-effects def))]) + (infer-body + (typed-def-body def) + (param-env (typed-def-params def)) + type-names))]) (append body-errors (if (and actual-type --- a/tests/test-typed-checker.ss +++ b/tests/test-typed-checker.ss @@ -271,6 +271,89 @@ (g x)))) '(return-type-mismatch)) +(test "effect annotation accepted" + (error-kinds + '(typed-library (effects accepted) + (export read) + (def (read) : Nat + #:effects (io alloc) + 1))) + '()) + +(test "unknown effect rejected" + (error-kinds + '(typed-library (effects unknown) + (export read) + (def (read) : Nat + #:effects (network) + 1))) + '(unknown-effect)) + +(test "duplicate effect rejected" + (error-kinds + '(typed-library (effects duplicate) + (export read) + (def (read) : Nat + #:effects (io io) + 1))) + '(duplicate-effect)) + +(test "pure effect cannot combine" + (error-kinds + '(typed-library (effects pure-combined) + (export read) + (def (read) : Nat + #:effects (pure io) + 1))) + '(bad-effect-combination)) + +(test "pure caller rejects effectful callee" + (error-kinds + '(typed-library (effects pure-caller) + (export f read) + (def (read) : Nat + #:effects (io) + 1) + (def (f) : Nat + (read)))) + '(effect-mismatch)) + +(test "effectful caller covers callee effects" + (error-kinds + '(typed-library (effects covered) + (export f read) + (def (read) : Nat + #:effects (io) + 1) + (def (f) : Nat + #:effects (io) + (read)))) + '()) + +(test "effectful caller must cover all callee effects" + (error-kinds + '(typed-library (effects missing) + (export f read) + (def (read) : Nat + #:effects (io alloc) + 1) + (def (f) : Nat + #:effects (io) + (read)))) + '(effect-mismatch)) + +(test "pure effect annotation is pure" + (error-kinds + '(typed-library (effects explicit-pure) + (export f g) + (def (g) : Nat + #:effects (pure) + 1) + (def (f) : Nat + #:effects (pure) + (g)))) + '()) + (test "builtin string-length returns Nat" (error-kinds '(typed-library (body string-length-ok)