Nested dip fails type-check; row-poly constraints don't propagate into quotation bodies #471

New issue

Closed

opened 2026-05-11 00:47:03 +00:00 by navicore · 1 comment

navicore commented

2026-05-11 00:47:03 +00:00

Owner

Summary

Nested dip (the classic Forth/Factor idiom for reaching deeper than one stack item) fails the type checker in v7.0, even when the runtime semantics are sound and the user is being careful.

: t ( -- )
    100 5 3
    [ [ 50 i.+ ] dip ] dip
    drop drop drop
;

error [type-error]: at line 1: dip: stack underflow
  - expected a value below the quotation

The "sequential double dip" form fails for the same reason:

: t ( -- )
    100 5 3
    [ 50 i.+ ] dip [ ] dip
    drop drop drop
;

(That second form lints clean but doesn't actually dip past two items — it modifies the wrong slot. So neither shape of nested dip behaves the way Forth/Factor users expect.)

Root cause

dip's effect is ( ..a x [..a -- ..b] -- ..b x ). When the typechecker walks the body of the outer quotation [ [ 50 i.+ ] dip ], the surrounding stack is row-polymorphic — the row variable ..a is unconstrained. The inner dip requires "a value below the quotation", but with ..a unconstrained the checker can't prove there is one, so it conservatively rejects.

The semantics are fine — at runtime the outer dip would supply the value below — but the row-variable inference doesn't propagate that constraint into the quotation body.

What works today

The user can hide one value with dip and rearrange inside the quotation:

100 5 3
[ swap 50 i.+ swap ] dip   # → 150 5 3

This lints clean and behaves correctly. It's the workaround currently used in seqlings (chapter 37 exercise 04).

Why fix it

dip dip is a foundational combinator pattern. It's how 2dip, 3dip, and friends are typically built in Forth and Factor. Without it:

Chapter 37 in seqlings can teach dip but can't teach "reach deeper with nested dip" — the most natural follow-up exercise.
Anyone porting Factor / Joy / Forth code hits a wall where they expect a standard idiom to work and it doesn't.
Composing combinators (e.g., 2dip = swap dip swap or [ q ] 2dip = [ [ q ] dip ] dip) ends up requiring ad-hoc workarounds.

Suggested implementation paths

A few approaches, ranked by ambition:

Add 2dip (and maybe 3dip) as builtins with concrete row-poly signatures. The typechecker only has to handle the builtin's published effect, not infer through nested quotation bodies. Cheapest fix; covers the common cases without changing inference. (Factor and Joy ship these.)
Improve row-variable inference inside quotation bodies. When a quotation body refers to a row variable from its enclosing scope, propagate constraints introduced by builtins (e.g., "this body uses dip, which requires ..a to have at least one element"). Larger change; benefits every combinator, not just dip.
Document the limitation. Add a section to docs/language-guide.md explaining that nested dip doesn't type-check and showing the swap-inside-dip workaround. Cheapest; concedes the rough edge instead of fixing it.

(1) is probably the right pragmatic step. (2) is the principled fix.

Cross-reference

seqlings chapter 37 exercise 04 (04-dip-deeper) was rewritten away from [ [ q ] dip ] dip to [ swap q swap ] dip because the nested form doesn't compile. If 2dip is added, that exercise can be restored to its natural shape.

## Summary Nested `dip` (the classic Forth/Factor idiom for reaching deeper than one stack item) fails the type checker in v7.0, even when the runtime semantics are sound and the user is being careful. ``` : t ( -- ) 100 5 3 [ [ 50 i.+ ] dip ] dip drop drop drop ; ``` ``` error [type-error]: at line 1: dip: stack underflow - expected a value below the quotation ``` The "sequential double dip" form fails for the same reason: ``` : t ( -- ) 100 5 3 [ 50 i.+ ] dip [ ] dip drop drop drop ; ``` (That second form lints clean but doesn't actually dip past two items — it modifies the wrong slot. So neither shape of nested dip behaves the way Forth/Factor users expect.) ## Root cause `dip`'s effect is `( ..a x [..a -- ..b] -- ..b x )`. When the typechecker walks the body of the *outer* quotation `[ [ 50 i.+ ] dip ]`, the surrounding stack is row-polymorphic — the row variable `..a` is unconstrained. The inner `dip` requires "a value below the quotation", but with `..a` unconstrained the checker can't prove there is one, so it conservatively rejects. The semantics are fine — at runtime the outer dip would supply the value below — but the row-variable inference doesn't propagate that constraint into the quotation body. ## What works today The user can hide one value with `dip` and rearrange inside the quotation: ``` 100 5 3 [ swap 50 i.+ swap ] dip # → 150 5 3 ``` This lints clean and behaves correctly. It's the workaround currently used in seqlings (chapter 37 exercise 04). ## Why fix it `dip dip` is a foundational combinator pattern. It's how `2dip`, `3dip`, and friends are typically built in Forth and Factor. Without it: - Chapter 37 in seqlings can teach `dip` but can't teach "reach deeper with nested dip" — the most natural follow-up exercise. - Anyone porting Factor / Joy / Forth code hits a wall where they expect a standard idiom to work and it doesn't. - Composing combinators (e.g., `2dip = swap dip swap` or `[ q ] 2dip = [ [ q ] dip ] dip`) ends up requiring ad-hoc workarounds. ## Suggested implementation paths A few approaches, ranked by ambition: 1. **Add `2dip` (and maybe `3dip`) as builtins** with concrete row-poly signatures. The typechecker only has to handle the builtin's published effect, not infer through nested quotation bodies. Cheapest fix; covers the common cases without changing inference. (Factor and Joy ship these.) 2. **Improve row-variable inference inside quotation bodies.** When a quotation body refers to a row variable from its enclosing scope, propagate constraints introduced by builtins (e.g., "this body uses `dip`, which requires `..a` to have at least one element"). Larger change; benefits every combinator, not just `dip`. 3. **Document the limitation.** Add a section to docs/language-guide.md explaining that nested dip doesn't type-check and showing the swap-inside-dip workaround. Cheapest; concedes the rough edge instead of fixing it. (1) is probably the right pragmatic step. (2) is the principled fix. ## Cross-reference - seqlings chapter 37 exercise 04 (`04-dip-deeper`) was rewritten away from `[ [ q ] dip ] dip` to `[ swap q swap ] dip` because the nested form doesn't compile. If `2dip` is added, that exercise can be restored to its natural shape.

navicore referenced this issue from a commit

2026-05-11 04:00:28 +00:00

nested dip

navicore referenced this issue

2026-05-11 04:01:18 +00:00

nested dip #472

navicore commented

2026-05-11 04:11:12 +00:00

Author

Owner

#472

https://git.navicore.tech/navicore/patch-seq/pulls/472