joins-a-side-whose-operand-raises.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The right side fires 'L_wrap', whose only operand under 'dataize' is a
# copy of 'throw', whose λ function 'L_throw' the entry names under
# 'terminators'. Data that comes from something that raises is the same
# raise, so 'L_wrap' answers ⊥ and never fires 'L_throw', and the join
# takes the right side for a side that raises (#2330).
symbolic: |
  - λ: L_wrap
    terminators: [L_throw]
    dataize:
      𝛿1: $.x
    𝑛: ⟦ λ ⤍ 𝜎 ⟧
  - λ: L_pick
    terminators: [L_throw]
    dataize:
      𝛿1: $.c
    morph:
      𝑛1: $.l
      𝑛2: $.r
    join:
      on: 𝛿1
      left: 𝑛1
      right: 𝑛2
location: 'Q.y'
input: '⟦ wrap(x) ↦ ⟦ λ ⤍ L_wrap ⟧, y ↦ ⟦ λ ⤍ L_pick, c ↦ ⟦ λ ⤍ 𝜎1 ⟧, l ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧, r ↦ Φ.wrap( ⟦ λ ⤍ L_throw ⟧ ).φ ⟧.φ ⟧'
result: '𝜎4:λ'
protocol: |
  𝕄(Φ.y):
    𝔼(L_pick):
      𝔻(ξ.c):
        𝛿·1·1 := 𝔻(𝜎1:λ)
      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.c)
      𝕄(ξ.l):
        morphed 𝑛·1·1 := 𝜎2:λ:φ
      𝑛1·1 := 𝑛·1·1  # 𝕄(ξ.l)
      𝕄(ξ.r):
        remembered 𝑛·1·2 ≡ Φ.wrap  # ⟦ x ↦ ∅, λ ⤍ L_wrap ⟧
        𝑛·1·3 := Φ.wrap( x ↦ L_throw:λ )
        𝑛·1·4 := ⟦ x ↦ L_throw:λ, λ ⤍ L_wrap ⟧
        remembered 𝑛·1·4 ≡ 𝑛·1·2( x ↦ L_throw:λ )
        𝔼(L_wrap):
          𝑛·2·1 := ⊥
        morphed 𝑛·1·5 := ⊥
      𝑛2·1 := ⊥  # 𝕄(ξ.r)
      joined 𝜎4 := 𝛿1·1 ? 𝜎2 : 𝜎3  # where 𝜎3 is ⊥
      𝑛·1·6 := 𝜎4:λ:φ
    morphed 𝑛·0·1 := 𝜎4:λ