Quotation effect verification - inferred vs declared #231

New issue

Closed

opened 2026-01-10 23:12:17 +00:00 by navicore · 2 comments

navicore commented

2026-01-10 23:12:17 +00:00

(Migrated from github.com)

Problem

Quotation types are inferred from their bodies, but there's limited verification that the inferred effect matches what's expected by the caller.

Example

// What if quotation has wrong arity?
: apply-binary ( Int Int Quot -- Int )
  call ;

: test ( -- Int )
  5 10 [ drop ] apply-binary ;  // Quot is ( Int -- ), not ( Int Int -- Int )

Current Behavior

Quotation body is type-checked, inferring its effect
Effect is stored as Type::Quotation { effect } or Type::Closure { ... }
When call is used, the quotation's effect is applied to current stack
Mismatch should be caught by unification

Questions

Is the inferred quotation effect always verified against usage context?
What happens with polymorphic quotations passed to combinators?
Are there edge cases where wrong-arity quotations slip through?

Test Cases Needed

// Wrong input arity
[ drop drop ] // ( a b -- ) passed where ( a -- ) expected

// Wrong output arity  
[ dup ] // ( a -- a a ) passed where ( a -- a ) expected

// Type mismatch in quotation
[ 1 i.+ ] // ( Int -- Int ) passed where ( String -- String ) expected

// Polymorphic confusion
[ swap ] // Generic, but used in specific context

Proposed Work

Add tests for quotation arity mismatches
Add tests for quotation type mismatches
Verify combinator words (bi, dip, keep, etc.) catch bad quotations
Improve error messages for quotation type failures

Acceptance Criteria

Tests proving wrong-arity quotations are rejected
Tests proving wrong-type quotations are rejected
Clear error messages pointing to the quotation issue
Documentation of quotation type checking guarantees

## Problem Quotation types are inferred from their bodies, but there's limited verification that the inferred effect matches what's expected by the caller. ## Example ```seq // What if quotation has wrong arity? : apply-binary ( Int Int Quot -- Int ) call ; : test ( -- Int ) 5 10 [ drop ] apply-binary ; // Quot is ( Int -- ), not ( Int Int -- Int ) ``` ## Current Behavior 1. Quotation body is type-checked, inferring its effect 2. Effect is stored as `Type::Quotation { effect }` or `Type::Closure { ... }` 3. When `call` is used, the quotation's effect is applied to current stack 4. Mismatch should be caught by unification ## Questions 1. Is the inferred quotation effect always verified against usage context? 2. What happens with polymorphic quotations passed to combinators? 3. Are there edge cases where wrong-arity quotations slip through? ## Test Cases Needed ```seq // Wrong input arity [ drop drop ] // ( a b -- ) passed where ( a -- ) expected // Wrong output arity [ dup ] // ( a -- a a ) passed where ( a -- a ) expected // Type mismatch in quotation [ 1 i.+ ] // ( Int -- Int ) passed where ( String -- String ) expected // Polymorphic confusion [ swap ] // Generic, but used in specific context ``` ## Proposed Work 1. Add tests for quotation arity mismatches 2. Add tests for quotation type mismatches 3. Verify combinator words (`bi`, `dip`, `keep`, etc.) catch bad quotations 4. Improve error messages for quotation type failures ## Acceptance Criteria - [ ] Tests proving wrong-arity quotations are rejected - [ ] Tests proving wrong-type quotations are rejected - [ ] Clear error messages pointing to the quotation issue - [ ] Documentation of quotation type checking guarantees

navicore commented

2026-01-11 00:12:57 +00:00

(Migrated from github.com)

Test Results: Quotation Effect Verification (#231)

Added 10 tests for combinator quotation verification.

✅ Working Correctly (8 tests)

Test	What it verifies
`test_times_rejects_quotation_that_pushes`	`times` rejects `[1]` (pushes value)
`test_times_rejects_quotation_that_consumes`	`times` rejects `[drop]` (consumes value)
`test_while_cond_must_return_bool`	`while` cond must return Bool
`test_until_body_must_be_stack_neutral`	`until` body must be stack-neutral
`test_valid_while_loop`	Valid while loop works
`test_valid_until_loop`	Valid until loop works
`test_quotation_in_times_loop`	Valid times loop works

❌ GAPS FOUND (2 tests document known issues)

Test	Gap
`test_while_body_stack_neutral_gap`	`while` body `[1]` should be rejected but passes
`test_until_cond_return_type_gap`	`until` cond `[1]` (returns Int) should be rejected but passes

Root Cause Analysis

The gaps occur because of how row variable unification works with quotation types in combinator signatures:

// while signature
( ..a Quot[..a -- ..a Bool] Quot[..a -- ..a] -- ..a )

When [1] with effect (-- Int) is matched against Quot[..a -- ..a]:

The row variable ..a unifies with empty
Expected: Quot[empty -- empty]
Actual: Quot[empty -- Int]
Should fail but the unification is too permissive

The issue is that quotation type matching doesn't properly verify that:

The output stack shape matches exactly (not just unifies loosely)
Concrete types like Bool are checked, not absorbed into row variables

Recommendation

Create a new issue for fixing quotation type matching in combinator unification. This requires:

Stricter unification when matching Quot[effect] types
Ensuring shared row variables in signatures constrain properly
Concrete types (Bool, Int) should not unify with row variables

Summary

times combinator: Fully working ✅
while combinator: Partial - cond check works, body check has gap
until combinator: Partial - body check works, cond check has gap

## Test Results: Quotation Effect Verification (#231) Added 10 tests for combinator quotation verification. ### ✅ Working Correctly (8 tests) | Test | What it verifies | |------|------------------| | `test_times_rejects_quotation_that_pushes` | `times` rejects `[1]` (pushes value) | | `test_times_rejects_quotation_that_consumes` | `times` rejects `[drop]` (consumes value) | | `test_while_cond_must_return_bool` | `while` cond must return Bool | | `test_until_body_must_be_stack_neutral` | `until` body must be stack-neutral | | `test_valid_while_loop` | Valid while loop works | | `test_valid_until_loop` | Valid until loop works | | `test_quotation_in_times_loop` | Valid times loop works | ### ❌ GAPS FOUND (2 tests document known issues) | Test | Gap | |------|-----| | `test_while_body_stack_neutral_gap` | `while` body `[1]` should be rejected but passes | | `test_until_cond_return_type_gap` | `until` cond `[1]` (returns Int) should be rejected but passes | ### Root Cause Analysis The gaps occur because of how row variable unification works with quotation types in combinator signatures: ```rust // while signature ( ..a Quot[..a -- ..a Bool] Quot[..a -- ..a] -- ..a ) ``` When `[1]` with effect `(-- Int)` is matched against `Quot[..a -- ..a]`: 1. The row variable `..a` unifies with `empty` 2. Expected: `Quot[empty -- empty]` 3. Actual: `Quot[empty -- Int]` 4. **Should fail** but the unification is too permissive The issue is that quotation type matching doesn't properly verify that: 1. The output stack shape matches exactly (not just unifies loosely) 2. Concrete types like Bool are checked, not absorbed into row variables ### Recommendation Create a new issue for fixing quotation type matching in combinator unification. This requires: 1. Stricter unification when matching `Quot[effect]` types 2. Ensuring shared row variables in signatures constrain properly 3. Concrete types (Bool, Int) should not unify with row variables ### Summary - `times` combinator: **Fully working** ✅ - `while` combinator: **Partial** - cond check works, body check has gap - `until` combinator: **Partial** - body check works, cond check has gap

navicore commented

2026-01-11 00:20:43 +00:00

(Migrated from github.com)

https://github.com/navicore/patch-seq/pull/235