joins-a-fork-whose-branches-a-stay-brought-to-one-shape.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# A branch reading the ρ of a copy, the way 'as-number' of EO reads its 'data',
# comes to a dispatch the copy hangs on as its ρ, '( ρ ↦ ⟦ … ⟧ )', while the
# other branch, made of no object, carries no such tail. Both are numbers made
# of one symbol, yet the join compares the terms as written and the tail makes
# their shapes differ. A 'stay' line drops every ρ a dispatch is applied to,
# which 'stay' or 'skip' of normalization drops anyway once the dispatch comes
# to a formation, so the two have one shape and the fork answers their join.
# Each 'stay' line binds a meta of its own, which the protocol writes like a
# 'rewrite' one, commented with the meta it kept; a branch with no tail is
# bound as it was (#1902).
symbolic: |
  - λ: L_fork
    morph:
      𝑛1: $.a
      𝑛2: $.b
    stay:
      𝑛3: 𝑛1
      𝑛4: 𝑛2
    join:
      𝑛5: [𝑛3, 𝑛4]
    𝑛: 𝑛5
location: 'Q.y'
hide-rho: false
input: '⟦ number ↦ ⟦ φ ↦ ∅ ⟧, bytes ↦ ⟦ φ ↦ ∅ ⟧, y ↦ ⟦ a ↦ ⟦ φ ↦ Φ.number( φ ↦ ⟦ ρ ↦ Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ), x ↦ ∅ ⟧.ρ ) ⟧, b ↦ ⟦ φ ↦ Φ.number( φ ↦ Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ) ) ⟧, λ ⤍ L_fork ⟧.φ ⟧'
result: 'Φ.bytes( φ ↦ 𝜎3:λ ):φ'
protocol: |
  𝕄(Φ.y):
    𝔼(L_fork):
      𝑛1·1 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎1:λ, ρ ↦ ⟦ ρ ↦ Φ.bytes( φ ↦ 𝜎1:λ ), x ↦ ∅ ⟧ ) ):φ  # 𝕄(ξ.a)
      𝑛2·1 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎2:λ ) ):φ  # 𝕄(ξ.b)
      𝑛3·1 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎1:λ ) ):φ  # 𝑛1
      𝑛4·1 := 𝑛2·1  # 𝑛2
      𝔻(𝜎3:λ) ∈ { 𝔻(𝜎1:λ), 𝔻(𝜎2:λ) }
      𝑛5·1 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎3:λ ) ):φ  # [𝑛3, 𝑛4]
      𝑛·1·1 := 𝑛5·1  # 𝑛
      𝑛·1·2 := 𝑛5·1  # 𝕄(𝑛·1·1)
    𝑛·0·1 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎3:λ ) )