joins-a-side-that-raises-through-a-terminator.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The right side is a copy of 'throw', whose λ function 'L_throw' the entry
# names under 'terminators', the way EO raises its 'T' with a message. The
# side goes through the 'evaluate', 'stay', 'symbolize' and 'defer' lines
# untouched, so 'L_throw' is never fired and its message is never turned
# into a symbol. The join takes it for a side that raises, the way it takes
# ⊥: it keeps the left side, mints 𝜎3 to stand for the raise and names the
# copy of 'throw' in the comment of the 'joined' line (#2263).
symbolic: |
  - λ: L_fork
    terminators: [L_throw]
    dataize:
      𝛿1: $.on🌵
    morph:
      𝑛1: $.left🌵
      𝑛2: $.right🌵
    evaluate:
      𝑛3: 𝑛1
      𝑛4: 𝑛2
    stay:
      𝑛5: 𝑛3
      𝑛6: 𝑛4
    symbolize:
      𝑛7: 𝑛5
      𝑛8: 𝑛6
    defer:
      𝑛9: 𝑛7
      𝑛10: 𝑛8
    join:
      on: 𝛿1
      left: 𝑛9
      right: 𝑛10
      otherwise: L_fork
location: 'Q.x'
input: '⟦ throw(message) ↦ ⟦ λ ⤍ L_throw ⟧, x ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎1 ⟧, left🌵 ↦ ⟦ k ↦ ⟦⟧, φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧, right🌵 ↦ Φ.throw( "bad" ) ⟧.φ ⟧'
result: '𝜎4:λ'
protocol: |
  𝕄(Φ.x):
    𝔼(L_fork):
      𝔻(ξ.on🌵):
        𝛿·1·1 := 𝔻(𝜎1:λ)
      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.on🌵)
      𝕄(ξ.left🌵):
        morphed 𝑛·1·1 := ⟦ k ↦ ⟦⟧, φ ↦ 𝜎2:λ ⟧
      𝑛1·1 := 𝑛·1·1  # 𝕄(ξ.left🌵)
      𝕄(ξ.right🌵):
        𝑛·1·2 := Φ.throw( message ↦ "bad" )
        𝑛·1·3 := ⟦ message ↦ "bad", λ ⤍ L_throw ⟧
        morphed 𝑛·1·4 := 𝑛·1·3
      𝑛2·1 := 𝑛·1·3  # 𝕄(ξ.right🌵)
      joined 𝜎4 := 𝛿1·1 ? 𝜎2 : 𝜎3  # where 𝜎3 is ⊥ raised by 𝑛·1·3
      𝑛·1·5 := ⟦ k ↦ ⟦⟧, φ ↦ 𝜎4:λ ⟧
    morphed 𝑛·0·1 := 𝜎4:λ