pith. machine review for the scientific record. sign in

arxiv: 2604.23807 · v1 · submitted 2026-04-26 · 💻 cs.PL

Recognition: unknown

Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types

Takashi Suwa , Atsushi Igarashi
Authors on Pith no claims yet

Pith reviewed 2026-05-08 04:53 UTC · model grok-4.3

classification 💻 cs.PL
keywords tensor shape checkingstagingcompile-time verificationshape consistencydependent typestensor programmingassertionscode generation
0
0 comments X

The pith

Staged shape-dependent types verify tensor shape consistency through compile-time assertions instead of proofs.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that staging can extract shape consistency conditions for tensors before actual computation occurs in many cases. These conditions are then checked by assertions that run as compile-time computations, immediately flagging inconsistencies without requiring users to supply proofs of type equality or subtyping. A surface language resembling ordinary dependently-typed code is translated into a staged core language, with shape arguments inferred implicitly where possible. If the approach holds, it delivers a mathematical guarantee that any successfully generated code will always be consistent with respect to tensor shapes, reducing the practical difficulties of continuous development compared to proof-heavy methods.

Core claim

The central claim is that tensor shape checking can be formalized using staging so that consistency conditions are extracted prior to tensor computations and enforced by assertions evaluated at compile time. Successfully generated code is therefore mathematically guaranteed to be consistent with respect to tensor shapes. The system reduces annotation effort by allowing implicit shape arguments that are inferred in a best-effort manner and by providing a non-staged surface language that translates to the staged core.

What carries the argument

Staged shape-dependent types, which shift shape consistency verification from static proofs to assertions evaluated during compile-time computation.

If this is right

  • Shape inconsistencies are detected immediately as assertion failures during compilation rather than at runtime.
  • Generated code carries a static guarantee of shape consistency without additional runtime checks for those properties.
  • A variety of tensor programs, including examples from ocaml-torch, can be verified for shape safety.
  • Implicit shape arguments lessen the need for explicit annotations while still preserving the consistency guarantee.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Similar staging techniques might apply to other properties that can be decided before execution, such as array bounds in general code.
  • The best-effort inference for shapes will likely require occasional manual intervention on programs with highly dynamic shape relations.
  • Integration with existing tensor libraries could allow shape checking to occur during just-in-time code generation rather than only at static compile time.

Load-bearing premise

Shape consistency conditions can be extracted before running the actual tensor computations in many typical cases.

What would settle it

A program accepted by the system whose generated code nevertheless produces a runtime shape mismatch error would show the guarantee does not hold.

Figures

Figures reproduced from arXiv: 2604.23807 by Atsushi Igarashi, Takashi Suwa.

Figure 11
Figure 11. Figure 11: all rules for reduction relations on terms view at source ↗
read the original abstract

When writing programs involving matrices or tensors in general, it is desirable to rule out the inconsistency of tensor shapes (i.e., the generalization of matrix sizes) before actual computation. For this purpose, some languages provide dependent types such as Mat m n, and others offer refinement types to track predicates for shapes. Despite the theoretical maturity, however, such methods are often unhandy for continuous software development due to the requirement of proofs for judging type equality or subtyping; even automated proving is often unsuitable due to its unforeseeable time consumption. To remedy this, our study provides an alternative formalization by using staging. Based on the observation that conditions for the shape consistency can be extracted before running the actual tensor computations in many typical cases, we ensure such consistency by assertions evaluated as compile-time computations, not by proofs. Under this formalization, we can verify the consistency virtually statically in the sense that inconsistencies as to tensor shapes will be immediately detected as assertion failures during compile-time computation. Our work achieves a mathematical guarantee that successfully generated code is always consistent with respect to tensor shapes. Furthermore, to vastly lessen the burden of adding shape- or stage-related descriptions, we (1) allow shape-related arguments to be implicit and infer them in a best-effort manner, and (2) offer a non-staged surface language that seemingly resembles ordinary dependently-typed languages and translate its programs into the staged core language. By a prototype implementation, we confirm that our language is expressive enough to verify a number of programs, including several examples offered by ocaml-torch.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

3 major / 2 minor

Summary. The paper proposes a staging-based alternative to dependent or refinement types for tensor shape checking. It uses compile-time assertions (evaluated via staging) to enforce shape consistency in many typical programs, claims a mathematical guarantee that successfully generated code is always shape-consistent, provides best-effort implicit shape inference, and offers a non-staged surface language that translates to the staged core. A prototype implementation is evaluated on examples including those from ocaml-torch.

Significance. If the central guarantee holds and the staging approach scales, the work could offer a more practical route to static shape safety for tensor programs than full dependent types, avoiding proof obligations while still catching inconsistencies at compile time. The combination of implicit inference and surface-language translation addresses usability concerns common in dependently-typed tensor libraries.

major comments (3)
  1. [Abstract] Abstract: The central claim of a 'mathematical guarantee that successfully generated code is always consistent with respect to tensor shapes' is asserted without any theorem statement, proof sketch, or formal argument in the manuscript. The description remains informal, resting on the observation that 'conditions for the shape consistency can be extracted before running the actual tensor computations in many typical cases,' but no derivation shows why the staged assertions are sufficient and complete for the modeled operations.
  2. [Abstract and §4 (prototype evaluation)] The skeptic concern about sufficiency is load-bearing: if the surface-to-core translation or the best-effort implicit inference fails to capture data-dependent control flow or unmodeled operations, generated code could still exhibit runtime shape inconsistencies. The manuscript provides no formal preservation argument or counterexample analysis for these cases.
  3. [§3] §3 (formalization of staged core): Without explicit equations or a small-step semantics for the staging mechanism, it is unclear how assertion failures during compile-time computation are guaranteed to correspond exactly to runtime shape mismatches, especially when shapes depend on runtime values that are not statically extractable.
minor comments (2)
  1. The paper would benefit from a small worked example showing the surface language, its translation, and the resulting staged assertions for a matrix multiplication with mismatched dimensions.
  2. [Abstract] Clarify the scope of 'many typical cases' with a precise characterization of the programs for which extraction is complete versus those that fall back to runtime checks.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for the constructive comments highlighting the need for stronger formal presentation of our staging-based guarantees. We address each major comment below and commit to revisions that strengthen the manuscript without altering its core contributions.

read point-by-point responses

  1. Referee: [Abstract] The central claim of a 'mathematical guarantee that successfully generated code is always consistent with respect to tensor shapes' is asserted without any theorem statement, proof sketch, or formal argument in the manuscript. The description remains informal, resting on the observation that 'conditions for the shape consistency can be extracted before running the actual tensor computations in many typical cases,' but no derivation shows why the staged assertions are sufficient and complete for the modeled operations.

    Authors: We acknowledge that the abstract presents the guarantee informally. Section 3 defines the staged core language and assertion mechanism, which establishes the guarantee by construction: shape conditions are checked via staging before code generation. In the revision we will add an explicit theorem statement to Section 3, together with a proof sketch deriving sufficiency and completeness for the modeled operations from the staging semantics. revision: yes

  2. Referee: [Abstract and §4 (prototype evaluation)] The skeptic concern about sufficiency is load-bearing: if the surface-to-core translation or the best-effort implicit shape inference fails to capture data-dependent control flow or unmodeled operations, generated code could still exhibit runtime shape inconsistencies. The manuscript provides no formal preservation argument or counterexample analysis for these cases.

    Authors: The surface-to-core translation and implicit inference are designed for programs in which shape conditions are statically extractable. We agree a formal preservation argument is missing. We will extend Section 4 (or add an appendix) with a preservation argument for the translation on extractable cases and include counterexample analysis for data-dependent control flow and unmodeled operations where the guarantee does not apply. revision: yes

  3. Referee: [§3] §3 (formalization of staged core): Without explicit equations or a small-step semantics for the staging mechanism, it is unclear how assertion failures during compile-time computation are guaranteed to correspond exactly to runtime shape mismatches, especially when shapes depend on runtime values that are not statically extractable.

    Authors: Section 3 presents the staged core and assertion rules, but we concur that more explicit semantics would improve clarity. We will revise Section 3 to include small-step operational semantics for staging, with equations showing how assertion failures at compile time correspond to runtime shape mismatches for extractable cases, and we will explicitly delimit the scope for non-extractable runtime-dependent shapes. revision: yes

Circularity Check

0 steps flagged

No circularity: staged assertions and surface-to-core translation are independent of the consistency guarantee

full rationale

The paper's central claim is a mathematical guarantee for successfully generated code, resting on an explicit design choice to evaluate shape-consistency conditions as compile-time assertions rather than proofs. This rests on the stated observation about typical programs and the formalization of staging plus implicit inference, none of which reduce to the target result by definition or by self-citation. No equations, fitted parameters, or load-bearing self-citations appear in the provided text; the derivation is self-contained against the paper's own formal model.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the domain assumption that shape-consistency conditions are extractable at staging time for typical programs; no free parameters or invented entities are introduced.

axioms (1)
  • domain assumption Shape-consistency conditions can be extracted before actual tensor computation in many typical cases
    Stated explicitly in the abstract as the basis for using compile-time assertions.

pith-pipeline@v0.9.0 · 5580 in / 1114 out tokens · 28252 ms · 2026-05-08T04:53:08.153835+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

60 extracted references · 2 canonical work pages

  1. [1]

    13 Koen Claessen and John Hughes

    Association for Computing Machinery.doi:10.1145/1926354.1926358. 13 Koen Claessen and John Hughes. QuickCheck: a lightweight tool for random testing of Haskell programs. InProceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, ICFP ’00, page 268–279, New York, NY, USA, 2000. Association for Computing Machinery.doi:10.1145...

    work page doi:10.1145/1926354.1926358 2000

  2. [2]

    skeletons

    URL: https://www.sciencedirect.com/science/article/pii/S0890540185710577, doi:10.1006/inco.1995.1057. 71 GHC Team. Glasgow Haskell Compiler.https://www.haskell.org/ghc/. Accessed: 2025-03- 22. T. Suwa and A. Igarashi 31 72 Takeshi Tsukada and Atsushi Igarashi. A logical foundation for environment classifiers. In Pierre-Louis Curien, editor,Typed Lambda Ca...

    work page doi:10.1006/inco.1995.1057 1995

  3. [3]

    For eachc, its typeτ(1) :=B%(c)is a first-order type, i.e., there existτ′(1)and a sequence(τ (1) i )m i=1, wherem:= ar(c), such that: τ(1) =τ (1) 1 →···→τ (1) m →τ′(1), ⊢1 oz τ (1) i for eachi∈{1,...,m}, and ⊢1 oz τ′(1)

  4. [4]

    For a functionc of arity m := ar(c)≥1and a sequence( ci)m i=1 such thatB%(ci) = τ (1) i for eachi∈{1,...,m}whereB%(c) =: τ (1) 1 →···→τ (1) m →τ′(1), there existsc′such that δ(c,(ci)m i=1) =c′andB %(c′) =τ′(1). 4.Ifδ(c,(c i)k i=1) =q, then: k= ar(c), qis of the formc′, and there exist a sequence(τ (1) i )k i=1 andτ′(1)such that: B%(c) =τ (1) 1 →···→τ (1) ...

  5. [5]

    For eachp, its typeT (0) :=B0(p)is a well-formed first-order function type, i.e., we have•⊢0 T (0), and there existT′(0)and a sequence(T (0) i )m i=1, wherem:= ar(p), such that: T (0) = (x 1 :T (0) 1 )→···→(xm :T (0) m )→T′(0), ⊢0 dom T (0) i for eachi∈{1,...,m}, and ⊢0 cod T′(0)

  6. [6]

    8.Ifδ(p,(c i)k i=1) =q, then: k= ar(p), and there exist a sequence(T (0) i )k i=1 andT ′(0)such that: B0(p) = (x 1 :T (0) 1 )→···→(xk :T (0) k )→T′(0), and T

    For a functionp of aritym := ar(p)≥1and a sequence(ci)m i=1 such thatci ⊨ [ci−1/xi−1]···[c1/x1]T (0) i for eachi∈{1,...,m}whereB0(p) =: (x1 :T (0) 1 )→···→(xm :T (0) m )→T′(0), there existsq such thatδ(p,(ci)m i=1) =qandq⊨[c m/xm]···[c1/x1]T′(0). 8.Ifδ(p,(c i)k i=1) =q, then: k= ar(p), and there exist a sequence(T (0) i )k i=1 andT ′(0)such that: B0(p) = ...

  7. [7]

    If x′∈domΓ′: We can assume x′̸= x by the Barendregt convention, and we have (Γ,[N ′(0)/x]Γ′)(x′) = ([N′(0)/x]T (0))0

    Case ⊢Γ,x: (T′(0))0,Γ′ (Γ,x: (T ′(0))0,Γ′)(x′) = (T (0))0 Γ,x: (T ′(0))0,Γ′⊢0 x′:T (0) T0-V ar: By IH, from⊢Γ,x : (T′(0))0,Γ′, we have⊢Γ,[N′(0)/x]Γ′. If x′∈domΓ′: We can assume x′̸= x by the Barendregt convention, and we have (Γ,[N ′(0)/x]Γ′)(x′) = ([N′(0)/x]T (0))0. This enables us to derive ⊢Γ,[N′(0)/x]Γ′ (Γ,[N ′(0)/x]Γ′)(x′) = ([N′(0)/x]T (0))0 Γ,[N ′(...

  8. [8]

    CaseT1-Abs: Done in a way similar toT0-Abs

    CaseT1-V ar: Immediate since substitution never happens. CaseT1-Abs: Done in a way similar toT0-Abs. The other cases are straightforward

  9. [9]

    Thus, we can derive Γ,Γ ′⊢0 [N′(0)/x]T (0) 1 Γ,Γ ′,x′: (T (0) 1 )0⊢0 [N′(0)/x]T (0) 2 Γ,Γ ′⊢0 (x′: [N′(0)/x]T (0) 1 )→[N′(0)/x]T (0) 2 Wf0-Arr The other cases are straightforward

    Case Γ,x: (T ′(0))0,Γ′⊢0 T (0) 1 Γ,x: (T ′(0))0,Γ′,x′: (T (0) 1 )0⊢0 T (0) 2 Γ,x: (T ′(0))0,Γ′⊢0 (x′:T (0) 1 )→T (0) 2 Wf0-Arr: By IH, from Γ,x : (T′(0))0, Γ′⊢0 T (0) 1 andΓ ,x : (T′(0))0, Γ′,x′: (T (0) 1 )0⊢0 T (0) 2 , we respectively have Γ,Γ ′⊢0 [N′(0)/x]T (0) 1 andΓ,Γ ′,x′: (T (0) 1 )0⊢0 [N′(0)/x]T (0) 2 . Thus, we can derive Γ,Γ ′⊢0 [N′(0)/x]T (0) 1 ...

  10. [10]

    This enables us to derive Γ,[N ′(0)/x]Γ′⊢0 [N′(0)/x]N (0) :{ν:NatList|true} Γ,[N ′(0)/x]Γ′⊢1 Tensor%([N ′(0)/x]N (0)) WfT1-Tensor

    Case Γ,x: (T ′(0))0,Γ′⊢0 N (0) :{ν:NatList|true} Γ,x: (T ′(0))0,Γ′⊢1 Tensor%N (0) WfT1-Tensor: ByIH,fromΓ ,x : (T′(0))0, Γ′⊢0 N (0) :{ν:NatList|true}, we haveΓ, [N′(0)/x]Γ′⊢0 [N′(0)/x]N (0) : [N′(0)/x]{ν:NatList| true}. This enables us to derive Γ,[N ′(0)/x]Γ′⊢0 [N′(0)/x]N (0) :{ν:NatList|true} Γ,[N ′(0)/x]Γ′⊢1 Tensor%([N ′(0)/x]N (0)) WfT1-Tensor. The ot...

  11. [11]

    By IH, from ⊢Γ,x : ( T′(0))0, Γ′′andΓ ,x : (T′(0))0, Γ′′⊢0 T (0), we respectively have⊢Γ, [N′(0)/x]Γ′′andΓ , [N′(0)/x]Γ′′⊢0 [N′(0)/x]T (0)

    Case⊢Γ,x: (T′(0))0,Γ′′Γ,x: (T ′(0))0,Γ′′⊢0 T (0) ⊢Γ,x: (T′(0))0,Γ′′,x′: (T (0))0 WfEnv-Cons0: W.l.o.g., we can assume x′̸= x by the Barendregt convention. By IH, from ⊢Γ,x : ( T′(0))0, Γ′′andΓ ,x : (T′(0))0, Γ′′⊢0 T (0), we respectively have⊢Γ, [N′(0)/x]Γ′′andΓ , [N′(0)/x]Γ′′⊢0 [N′(0)/x]T (0). Thus, we can derive ⊢Γ,[N′(0)/x]Γ′′Γ,[N ′(0)/x]Γ′′⊢0 [N′(0)/x]...

  12. [12]

    CaseT0-Cst0: Straightforward from Assumption 8. Case Γ⊢0 N (0) 1 : (x:T (0) 11 )→T (0) 12 Γ⊢0 N (0) 2 :T (0) 11 Γ⊢0 N (0) 1 N (0) 2 : [N (0) 2 /x]T (0) 12 T0-App: By IH, we haveΓ ⊢0 (x: T (0) 11 )→T (0) 12 and therebyΓ ,x : (T (0) 11 )0⊢0 T (0) 12 . Thus, by Lemma 10 andΓ⊢0 N (0) 2 :T (0) 11 , we haveΓ⊢0 [N (0) 2 /x]T (0) 12 . The other cases are straightforward

  13. [13]

    N (1) 2 ) :T (1) 1 →T (1) 2 T1-Abs: By IH, we haveΓ,x : (T (1) 1 )1⊢1 T (1) 2

    Case Γ⊢1 T (1) 1 Γ,x: (T (1) 1 )1⊢1 N (1) 2 :T (1) 2 x̸∈fv(T (1) 2 ) Γ⊢1 (λx:T (1) 1 . N (1) 2 ) :T (1) 1 →T (1) 2 T1-Abs: By IH, we haveΓ,x : (T (1) 1 )1⊢1 T (1) 2 . Since x̸∈fv(T (1) 2 )holds, we haveΓ ⊢1 T (1) 2 by evident contraction. This enables us to deriveΓ⊢1 T (1) 1 Γ⊢1 T (1) 2 Γ⊢1 T (1) 1 →T (1) 2 Wf1-Arr. The other cases are all straightforward...

  14. [14]

    By Lemma 11, we also haveΓ ⊢0 (x:T (0) 11 )→T (0) 12 (and therebyΓ ⊢0 T (0) 11 ) andΓ ⊢0 T (0) 2

    Case Γ⊢0 M (0) 1 : (x:T (0) 11 )→T (0) 12 ⇝N (0) 1 Γ⊢0 M (0) 2 :T (0) 2 ⇝N (0) 2 Γ⊢ℓT (0) 2 ◁T (0) 11 ⇝N (0) 0 Γ⊢0 (M (0) 1 M (0) 2 )ℓ: [N (0) 0 N (0) 2 /x]T (0) 12 ⇝N (0) 1 (N (0) 0 N (0) 2 ) S0-App: First, by IH, we have Γ ⊢0 N (0) 1 : (x:T (0) 11 )→T (0) 12 andΓ ⊢0 N (0) 2 : T (0) 2 . By Lemma 11, we also haveΓ ⊢0 (x:T (0) 11 )→T (0) 12 (and therebyΓ ⊢...

  15. [15]

    Case Γ⊢1 M (1) 1 :T (1) 11 →T (1) 12 ⇝N (1) 1 Γ⊢1 M (1) 2 :T (1) 2 ⇝N (1) 2 T (1) 2 ||1 T (1) 11 Γ⊢1 (M (1) 1 M (1) 2 )ℓ:T (1) 12 ⇝N (1) 1 ∼((|⟨T (1) 2 ⟩◁⟨T (1) 11⟩|)ℓ⟨N (1) 2 ⟩) S1-App: First, by IH, we haveΓ⊢1 N (1) 1 :T (1) 11 →T (1) 12 andΓ⊢1 N (1) 2 :T (1) 2 . Thus, we can derive: Γ⊢1 T (1) 2 Γ⊢1 T (1) 11 T (1) 2 ||1 T (1) 11 x̸∈dom(Γ) Γ⊢0 (|⟨T (1) 2...

  16. [16]

    Then, by IH, we haveΓ,ν: ({ν1 :B|true})0⊢0 N (0) : {ν2 :Bool|N′(0)}

    Case Γ,ν: ({ν1 :B|true})0⊢0 M (0) :{ν2 :Bool|N′(0)}⇝N(0) Γ⊢0{ν:B|M(0)}⇝{ν:B|N(0)} ST0-Base: First, we can eas- ily derive⊢Γ,ν: ({ν1 :B|true})0. Then, by IH, we haveΓ,ν: ({ν1 :B|true})0⊢0 N (0) : {ν2 :Bool|N′(0)}. This enables us to derive Γ,ν: ({ν1 :B|true})0⊢0 N (0) :{ν2 :Bool|N′(0)} Γ⊢0{ν:B|N(0)} WfT0-Rfn. The other cases are straightforward

  17. [17]

    Thus, we can derive Γ⊢0 N (0) :{ν:NatList|N′(0)} Γ⊢1 Tensor%N (0) WfT1-Tensor

    Case Γ⊢0 M (0) :{ν:NatList|N′(0)}⇝N(0) Γ⊢1 Tensor%M (0) ⇝Tensor%N (0) ST1-Tensor: By IH, we haveΓ⊢0 N (0) :{ν: NatList|N′(0)}. Thus, we can derive Γ⊢0 N (0) :{ν:NatList|N′(0)} Γ⊢1 Tensor%N (0) WfT1-Tensor. The other cases are also straightforward. ◀ D.2 Preservation and Progress ▶Lemma 12(Reduction conforms to CSR equivalence).T (1)−→1 T′(1)impliesT (1)≡1...

  18. [18]

    CaseCqT0-Reflis also immediate

    CaseCqT0-Rfnis immediate. CaseCqT0-Reflis also immediate. CaseCqT0-Symis straightforward by IH. Case {ν:B|N (0) 1 }≡0 T′(0) T′(0)≡0 T (0) {ν:B|N (0) 1 }≡0 T (0) CqT0-Trans: By IH, from{ν:B|N (0) 1 }≡0 T′(0), T′(0)is of the form{ν:B|N′(0)}. Then, again by IH, fromT′(0)≡0 T (0), T (0) is of the form{ν:B|N (0) 2 }. The other cases contradict the assumption. ...

  19. [19]

    CaseCqT0-Symis straightforward by IH

    CaseCqT0-Reflis immediate. CaseCqT0-Symis straightforward by IH. T. Suwa and A. Igarashi 49 Case Tensors≡0 T′(0) T′(0)≡0 T (0) Tensors≡0 T (0) CqT0-Trans: By IH, fromTensors≡0 T′(0), we have T′(0)=Tensors. Then, again by IH, fromT′(0)≡0 T (0), we haveT (0) =Tensors. The other cases contradict the assumption. 2.Can be proved in the same manner as (1). ◀ ▶L...

  20. [20]

    CaseCqT0-Reflis also immediate

    CaseCqT0-Arris immediate. CaseCqT0-Reflis also immediate. CaseCqT0-Symis straightforward by IH. Case (x:T (0) 11 )→T (0) 12 ≡0 T′(0) T′(0)≡0 T (0) (x:T (0) 11 )→T (0) 12 ≡0 T (0) CqT0-Trans: ByIH,from (x:T (0) 11 )→T (0) 12 ≡0 T′(0), T′(0)is of the form(x:T ′(0) 1 )→T′(0) 2 . Then, by IH again, from(x:T ′(0) 1 )→T′(0) 2 ≡0 T (0),T (0) is of the form(x:T ′...

  21. [21]

    CaseCqT0-Reflis also immediate

    CaseCqT0-Codeis immediate. CaseCqT0-Reflis also immediate. CaseCqT0-Symis straightforward by IH. Case⟨T (1) 1 ⟩≡0 T′(0) T′(0)≡0 T (0) ⟨T (1) 1 ⟩≡0 T (0) CqT0-Trans: By IH, from⟨T (1) 1 ⟩≡0 T′(0), T′(0)is of the form⟨T′(1)⟩. Then, again by IH, from⟨T′(1)⟩≡0 T (0),T (0) is of the form⟨T (1) 2 ⟩. The other cases contradict the assumption. 2.Can be proved in ...

  22. [22]

    N (0) 2 ), orN (0) = (|◁{ν:B| N (0) 1 }|)L is immediate

    Case where we haveN (0) = p, N (0) = c, N (0) = (λx′:T (0) 1 . N (0) 2 ), orN (0) = (|◁{ν:B| N (0) 1 }|)L is immediate. CaseN (0) =x contradicts the assumption because we have[N (0) 0 /x]N (0) =N (0) 0 , the left-hand side (resp. the right-hand side) of which is a value (resp. is not a value). Case N (0) =x′such thatx′̸=x also contradicts the assumption s...

  23. [23]

    N (1) 2 ): We have[N (0) 0 /x]N (1) = (λx:[N (0) 0 /x]T (1) 1

    CaseN (1) = (λx:T (1) 1 . N (1) 2 ): We have[N (0) 0 /x]N (1) = (λx:[N (0) 0 /x]T (1) 1 . [N (0) 0 /x]N (1) 2 ). By the definition of stage-1values,[N (0) 0 /x]T (1) 1 =:τ (1) 1 and[N (0) 0 /x]N (1) 2 are a stage-1type value and a stage-1value, respectively. Then, by IH, we haveT (1) 1 =τ (1) 1 , andN (1) 2 is also a stage-1 value. Therefore,N (1) = (λx:τ...

  24. [24]

    Then, by Lemma 34, we haveN (0) 1 =s

    Case T (1) = Tensor%N (0) 1 : Sinceτ(1) = [N (0) 0 /x](Tensor%N (0) 1 ) = Tensor%( [N (0) 0 /x]N (0) 1 ) holds, by the definition of stage-1type values,[ N (0) 0 /x]N (0) 1 is of the forms. Then, by Lemma 34, we haveN (0) 1 =s. Thus, we haveT (1) =Tensor%s=τ (1). CaseT (1) =B: This is immediate. 54 Compile-Time Tensor Shape Checking via Staged Shape-Depen...

  25. [25]

    Left-hand side: If[N (0) 0 /x](N (0) 1 N (0) 2 )−→0 N′(0), then there existsˆN (0) such that[N′(0) 0 /x](N (0) 1 N (0) 2 )−→0 [N′(0) 0 /x] ˆN (0) andN ′(0)= [N (0) 0 /x] ˆN (0). T. Suwa and A. Igarashi 55

  26. [26]

    Right-hand side: If[N′(0) 0 /x](N (0) 1 N (0) 2 )−→0 N′(0), then there existsˆN (0) such that[N (0) 0 /x](N (0) 1 N (0) 2 )−→0 [N (0) 0 /x] ˆN (0) andN ′(0)= [N′(0) 0 /x] ˆN (0). Proof. Since[ N (0) 0 /x]N (0) 1 is a value whileN (0) 0 is not (byN (0) 0 −→0 N′(0) 0 ), N (0) 1 is also a value by Lemma 35. Therefore, we can prove (1) and (2) as follows: 1.W...

  27. [27]

    If[ N (0) 0 /x]N (0)−→0 N′(0), then there exists ˆN (0) such that[N′(0) 0 /x]N (0)−→0∗[N′(0) 0 /x] ˆN (0) andN ′(0)= [N (0) 0 /x] ˆN (0)

  28. [28]

    If[ N (0) 0 /x]N (1)−→1 N′(1), then there exists ˆN (1) such that[N′(0) 0 /x]N (1)−→1∗[N′(0) 0 /x] ˆN (1) andN ′(1)= [N (0) 0 /x] ˆN (1)

  29. [29]

    Proof.By mutual induction on the structure ofN(0),N (1), andT (1)

    If[ N (0) 0 /x]T (1)−→1 T′(1), then there existsˆT (1) such that[N′(0) 0 /x]T (1)−→1∗[N′(0) 0 /x] ˆT (1) and T′(1)= [N (0) 0 /x] ˆT (1). Proof.By mutual induction on the structure ofN(0),N (1), andT (1)

  30. [30]

    Thus, ˆN (0) :=N′(0) 0 satisfies the desired properties sinceN′(0) 0 is a closed term (byN (0) 0 −→0 N′(0) 0 ) and thereby we have[N′(0) 0 /x]N′(0) 0 = [N (0) 0 /x]N′(0) 0 =N′(0) 0

    Case N (0) = x: Since[ N (0) 0 /x]N (0) = N (0) 0 , we haveN′(0)= N′(0) 0 by Lemma 33. Thus, ˆN (0) :=N′(0) 0 satisfies the desired properties sinceN′(0) 0 is a closed term (byN (0) 0 −→0 N′(0) 0 ) and thereby we have[N′(0) 0 /x]N′(0) 0 = [N (0) 0 /x]N′(0) 0 =N′(0) 0 . Case N (0) = x′such that x′̸= x: Since[ N (0) 0 /x]N (0) = x′, this case contradicts th...

  31. [31]

    We can easily show thatˆN (1) :=∼ˆN (0) satisfies the desired properties

    CaseN (1) =∼N(0): Wehaveoneofthefollowingtwocaseswiththederivationof[ N (0) 0 /x]N (1)−→1 N′(1): Case [N (0) 0 /x]N (0)−→0 N′(0) ∼([N (0) 0 /x]N (0))−→1∼N′(0)E1-Esc: ByIH,thereexists ˆN (0) suchthat[ N′(0) 0 /x]N (0)−→0∗ [N′(0) 0 /x] ˆN (0) and N′(0)= [N (0) 0 /x] ˆN (0). We can easily show thatˆN (1) :=∼ˆN (0) satisfies the desired properties. Case ∼⟨v (...

  32. [32]

    By IH, there existsˆN (0) 1 such that[N′(0) 0 /x]N (0) 1 −→0∗[N′(0) 0 /x] ˆN (0) 1 andN′(0) 1 = [N (0) 0 /x] ˆN (0) 1

    CaseT (1) =Tensor%N (0) 1 : Tracing back the derivation of[N (0) 0 /x]T (1)−→1 T′(1), we have [N (0) 0 /x]N (0) 1 −→0 N′(0) 1 Tensor%([N (0) 0 /x]N (0) 1 )−→1 Tensor%N ′(0) 1 ET1-Tensor. By IH, there existsˆN (0) 1 such that[N′(0) 0 /x]N (0) 1 −→0∗[N′(0) 0 /x] ˆN (0) 1 andN′(0) 1 = [N (0) 0 /x] ˆN (0) 1 . We can easily show thatˆT (1) :=Tensor% ˆN (0) 1 s...

  33. [33]

    First, since N′(0) 0 is a closed term byN (0) 0 −→0 N′(0) 0 , we have[N (0) 0 /x]N′(0)= N′(0) 0

    Case N (0) = x: We will show thatN′(0):=N ′(0) 0 satisfies the desired properties. First, since N′(0) 0 is a closed term byN (0) 0 −→0 N′(0) 0 , we have[N (0) 0 /x]N′(0)= N′(0) 0 . Therefore, we have (A) by[N (0) 0 /x]N (0) = N (0) 0 and N (0) 0 −→0 N′(0) 0 . Also, (B) immediately holds by the assumption that[N′(0) 0 /x]N (0) = N′(0) 0 is a stage-0value. ...

  34. [34]

    Case whereN (1) = (λx′:T (1) 1

    Case whereN (1) =corN (1) =x′:N ′(1):=N′(1)clearly satisfies (A), (B), and (C). Case whereN (1) = (λx′:T (1) 1 . N (1) 2 ): Since[N′(0) 0 /x]N (1) is a stage-1value,[N′(0) 0 /x]T (1) 1 =: τ (1) 1 and[ N′(0) 0 /x]N (1) 2 are also a type value and a stage-1value, respectively. Then, by IH, there existsN′(1) 2 such that (1X)[N (0) 0 /x]T (1) 1 −→1∗τ (1) 1 , ...

  35. [35]

    Case T (1) = Tensor%N (0): Since[N′(0) 0 /x]T (1) =:τ(1) is a type value,[N′(0) 0 /x]N (0) must be of the forms

    CaseT (1) =B: Sinceτ(1) =B, we clearly have (X). Case T (1) = Tensor%N (0): Since[N′(0) 0 /x]T (1) =:τ(1) is a type value,[N′(0) 0 /x]N (0) must be of the forms. Then, by the definition of substitution, we have the following two cases: Case whereN (0) =x andN′(0) 0 =s: By the assumptionN (0) 0 −→0 N′(0) 0 =s, we can derive (X)[N (0) 0 /x](Tensor%x)−→1∗τ(1...

  36. [36]

    If[ N′(0) 0 /x]N (0)−→0 N′(0), then there exists ˆN (0) such that[N (0) 0 /x]N (0)−→0∗[N (0) 0 /x] ˆN (0) andN ′(0)= [N′(0) 0 /x] ˆN (0)

  37. [37]

    If[ N′(0) 0 /x]N (1)−→1 N′(1), then there exists ˆN (1) such that[N (0) 0 /x]N (1)−→1∗[N (0) 0 /x] ˆN (1) andN ′(1)= [N′(0) 0 /x] ˆN (1)

  38. [38]

    If[ N′(0) 0 /x]T (1)−→1 T′(1), then there existsˆT (1) such that[N (0) 0 /x]T (1)−→1∗[N (0) 0 /x] ˆT (1) and T′(1)= [N′(0) 0 /x] ˆT (1). Proof. By mutual induction on the structure ofN (0),N (1), andT (1) similar to the one for Lemma 38 (i.e. the left-hand side version)

  39. [39]

    First, since N′(0)is a closed term (byN (0) 0 −→0 N′(0) 0 ), we have[N′(0) 0 /x] ˆN (0) = [N′(0) 0 /x]N′(0)= N′(0)

    Case N (0) = x: We will show that ˆN (0) :=N ′(0)satisfies the desired properties. First, since N′(0)is a closed term (byN (0) 0 −→0 N′(0) 0 ), we have[N′(0) 0 /x] ˆN (0) = [N′(0) 0 /x]N′(0)= N′(0). Also, since[ N′(0) 0 /x]N (0) = N′(0) 0 holds, we haveN′(0) 0 −→0 N′(0). Therefore, by [N (0) 0 /x]N (0) = N (0) 0 ,[ N (0) 0 /x] ˆN (0) = N′(0), and the assu...

  40. [40]

    CaseN (1) = (λx′:T (1) 1

    Case whereN (1) =c or N (1) =x′: This contradicts the assumption[N′(0) 0 /x]N (1)−→1 N′(1). CaseN (1) = (λx′:T (1) 1 . N (1) 2 ): We have one of the following cases: Case where[N′(0) 0 /x]T (1) 1 is not a type value: We can uniquely trace back the derivation of [N′(0) 0 /x]N (1)−→1 N′(1)as follows: [N′(0) 0 /x]T (1) 1 −→1 T′(1) 1 λx′: [N′(0) 0 /x]T (1) 1 ...

  41. [41]

    CaseT (1) =B: This contradicts the assumption[N′(0) 0 /x]T (1)−→1 T′(1). Case T (1) = Tensor%N (0): We can trace back the derivation of[N′(0) 0 /x]T (1)−→1 T′(1)as follows: [N′(0) 0 /x]N (0) 1 −→0 N′(0) 1 Tensor%([N ′(0) 0 /x]N (0) 1 )−→1 Tensor%N ′(0) 1 ET1-Tensor. By IH, there existsˆN (0) 1 such that[N (0) 0 /x]N (0) 1 −→0∗[N (0) 0 /x] ˆN (0) 1 andN′(0...

  42. [42]

    CaseCqT0-Symis straightforward by IH

    CaseCqT0-Reflis immediate. CaseCqT0-Symis straightforward by IH. Case{ν:B|N (0) 1 }≡0 T′(0) T′(0)≡0{ν:B|N (0) 2 } {ν:B|N (0) 1 }≡0{ν:B|N (0) 2 } CqT0-Trans: By Lemma 18,T′(0)is of the form{ν:B|N′(0)}. Then, by IH on{ν:B|N (0) 1 }≡0 T′(0), we have[c/ν]N′(0)−→0∗ true. Thus, again by IH onT′(0)≡0{ν:B|N (0) 2 }, we have[c/ν]N (0) 2 −→0∗true. Case σ1−→σ2 {ν:B|...

  43. [43]

    Case Γ⊢0 N (0) 1 : (x:T (0) 11 )→T (0) 12 Γ⊢0 N (0) 2 :T (0) 11 Γ⊢0 N (0) 1 N (0) 2 : [N (0) 2 /x]T (0) 12 T0-App: By case analysis on the deriva- tion ofN (0)−→0 N′(0)

    Case Γ⊢0 N (0) :T ′(0) T′(0)≡0 T (0) Γ⊢0 T (0) Γ⊢0 N (0) :T (0) T0-TyEquiv: Straightforward by IH. Case Γ⊢0 N (0) 1 : (x:T (0) 11 )→T (0) 12 Γ⊢0 N (0) 2 :T (0) 11 Γ⊢0 N (0) 1 N (0) 2 : [N (0) 2 /x]T (0) 12 T0-App: By case analysis on the deriva- tion ofN (0)−→0 N′(0). CaseE0-App1: Straightforward by IH. Case N (0) 2 −→0 N′(0) 2 N (0) 1 N (0) 2 −→0 N (0) 1...

  44. [44]

    Case Γ⊢0 N (0) :⟨T(1)⟩ Γ⊢1∼N(0) :T (1) T1-Esc: By case analysis of the last rule used for deriving the reduction

    Case Γ⊢1 N (1) :T ′(1) T′(1)≡1 T (1) Γ⊢1 T (1) Γ⊢1 N (1) :T (1) T1-TyEquiv: Straightforward by IH. Case Γ⊢0 N (0) :⟨T(1)⟩ Γ⊢1∼N(0) :T (1) T1-Esc: By case analysis of the last rule used for deriving the reduction. Case N (0)−→0 N′(0) ∼N(0)−→1∼N′(0)E1-Esc: Straightforward by IH. Case∼⟨N′(1)⟩−→1 N′(1)E1-Cancel: By Lemma 17, fromΓ⊢0⟨N′(1)⟩:⟨T(1)⟩, there exist...

  45. [45]

    CaseT0-Absis immediate

    CaseT0-V arcontradicts the assumption⊢1 Γ. CaseT0-Absis immediate. Case Γ⊢0 N (0) 1 : (x:T (0) 11 )→T (0) 12 Γ⊢0 N (0) 2 :T (0) 11 Γ⊢0 N (0) 1 N (0) 2 : [N (0) 2 /x]T (0) 12 T0-App: By IH onΓ ⊢0 N (0) 1 : (x: T (0) 11 )→T (0) 12 , we have one of the following cases: CaseN (0) 1 −→0⇑L: We have N (0) 1 −→0⇑L N (0) 1 N (0) 2 −→0⇑L E0-App1F. Case where N (0) ...

  46. [46]

    Case Γ⊢0 N (0) :⟨T(1)⟩ Γ⊢1∼N(0) :T (1) T1-Esc: By IH, fromΓ⊢0 N (0) :⟨T(1)⟩, we have one of the following cases: CaseN (0)−→0⇑L: We have N (0)−→0⇑L ∼N(0)−→1⇑L E1-EscF

    CaseT1-V aris immediate sincexis a stage-1 value. Case Γ⊢0 N (0) :⟨T(1)⟩ Γ⊢1∼N(0) :T (1) T1-Esc: By IH, fromΓ⊢0 N (0) :⟨T(1)⟩, we have one of the following cases: CaseN (0)−→0⇑L: We have N (0)−→0⇑L ∼N(0)−→1⇑L E1-EscF. Case whereN (0)−→0 N′(0)for someN′(0): We have N (0)−→0 N′(0) ∼N(0)−→1∼N′(0)E1-Esc Case whereN (0) =v(0) is a stage-0 value: By Lemma 53, f...

  47. [47]

    Case where N (0) −→0 N′(0)for some N′(0): Similarly to the previous case, we have N (0)−→0 N′(0) Tensor%N (0)−→1 Tensor%N ′(0)ET1-Tensor

    Case Γ⊢0 N (0) :{ν:NatList|true} Γ⊢1 Tensor%N (0) WfT1-Tensor: By IH, fromΓ ⊢0 N (0) :{ν:NatList| true}, we have one of the following cases: CaseN (0)−→0⇑L: We have N (0)−→0⇑L Tensor%N (0)−→1⇑L ET1-TensorF. Case where N (0) −→0 N′(0)for some N′(0): Similarly to the previous case, we have N (0)−→0 N′(0) Tensor%N (0)−→1 Tensor%N ′(0)ET1-Tensor. Case whereN ...

  48. [48]

    Thus, by Lemma 57, we haveσ(x)∼=0 σ′(x)

    CaseN (0) =x: If x∈domσ= domσ′: By the definition ofσ−→σ′, we haveσ(x)−→0∗σ′(x). Thus, by Lemma 57, we haveσ(x)∼=0 σ′(x). If x̸∈domσ= domσ′: SinceσN(0) =σ′N (0) =x, we can immediately finish the proof by x∼=0 x Bq0-Refl. Case N (0) = (λx:T (0) 1 . N (0) 2 ): By the Barendregt convention, we can safely assume x̸∈domσ= domσ′, and thereby haveσN(0) = (λx:σT ...

  49. [49]

    CaseT (0) ={ν:B|N(0)}: This is also straightforward by the Barendregt convention and IH

    CaseT (0) = (x:T (0) 1 )→T (0) 2 : Straightforward by IH since we can safely assumex̸∈domσ= domσ′by the Barendregt convention. CaseT (0) ={ν:B|N(0)}: This is also straightforward by the Barendregt convention and IH. The other cases are all straightforward. T. Suwa and A. Igarashi 73 N (0) 1 ∼=0 N (0) 2 N (1) 1 ∼=1 N (1) 2 ⟨N (1) 1 ⟩∼=0⟨N (1) 2 ⟩ Bq0-Brkt ...

  50. [50]

    N (1) 12 ∼=1 λx:T (1)

  51. [51]

    N(0) =⇒0 λx:T′(0)

    N (1) 22 Bq1-Abs Figure 24β-equivalence relations on terms 74 Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types N (0) =⇒0 N′(0) p=⇒0 p P0-Cst0 c=⇒0 c P0-CstP x=⇒0 x P0-V ar T (0) =⇒0 T′(0) N (0) =⇒0 N′(0) λx:T(0). N(0) =⇒0 λx:T′(0). N′(0)P0-Abs N (0) 1 =⇒0 N′(0) 1 N (0) 2 =⇒0 N′(0) 2 N (0) 1 N (0) 2 =⇒0 N′(0) 1 N′(0) 2 P0-App N (0) 1 =⇒0...

  52. [52]

    The other cases are also straightforward

    CaseT (1) =Tensor%N (0): By IH, we haveσN(0)∼=0 σ′N (0), and thereby we can derive σN(0)∼=0 σ′N (0) Tensor%(σN(0))∼=1 Tensor%(σ′N (0)) BqT1-Tensor. The other cases are also straightforward. ◀ ▶Lemma 59(Stage-1 CSR equivalence impliesβ-equivalence).T (1)≡1 T′(1)impliesT (1)∼=1 T′(1). Proof.By induction on the derivation ofT (1)≡1 T′(1). Case σ−→σ′ Tensor%(...

  53. [53]

    CaseBq0-SymandBq0-Transare straightforward by IH

    CaseBq0-Reflis immediate. CaseBq0-SymandBq0-Transare straightforward by IH. Case (|⟨τ(1)⟩◁⟨τ(1)⟩|)L∼=0 λx:⟨τ(1)⟩. x Bq0-AssPass: Immediate byP0-AssPass. Case (λx:T(0). N (0) 1 )N (0) 2 ∼=0 [N (0) 2 /x]N (0) 1 Bq0-Beta: Since N (0) 1 =⇒0 N (0) 1 and N (0) 2 =⇒0 N (0) 2 hold by Lemma 61, we can derive N (0) 1 =⇒0 N (0) 1 N (0) 2 =⇒0 N (0) 2 (λx:T(0). N (0) ...

  54. [54]

    CasesBq1-SymandBq1-Transare straightforward by IH

    CaseBq1-Reflis immediate. CasesBq1-SymandBq1-Transare straightforward by IH. Case∼⟨N(1)⟩∼=1 N (1) Bq1-Cancel: SinceN (1) =⇒1 N (1) holds by Lemma 61, we can derive N (1) =⇒1 N (1) ∼⟨N(1)⟩=⇒1 N (1) P1-Cancel. Case N (0) 1 ∼=0 N (0) 2 ∼N (0) 1 ∼=1∼N (0) 2 Bq1-Esc: Immediate by IH and Lemma 64 (11). Case N (1) 11 ∼=1 N (1) 21 N (1) 12 ∼=1 N (1) 22 N (1) 11 N...

  55. [55]

    CasesBqT0-SymandBqT0-Transare straightforward by IH

    CaseBqT0-Reflis immediate. CasesBqT0-SymandBqT0-Transare straightforward by IH. Case T (1) 1 ∼=1 T (1) 2 ⟨T (1) 1 ⟩∼=0⟨T (1) 2 ⟩ BqT0-Code: ByIH,wehave T (1) 1 ⇐⇒1∗T (1) 2 . Therefore, byLemma63(1), we have⟨T (1) 1 ⟩⇐⇒0∗⟨T (1) 2 ⟩. 78 Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types (B)∗:=B(Tensor%N (0) )∗:=Tensor%(N (0) )∗ (T (1) 1 →T ...

  56. [56]

    CasesBqT1-SymandBqT1-Transare straightforward by IH

    CaseBqT1-Reflis immediate. CasesBqT1-SymandBqT1-Transare straightforward by IH. Case T (1) 11 ∼=1 T (1) 21 T (1) 12 ∼=1 T (1) 22 T (1) 11 →T (1) 12 ∼=1 T (1) 21 →T (1) 22 BqT1-Arr: By IH and Lemmata 61 and 63 (5)–(6). Case N (0) 1 ∼=0 N (0) 2 Tensor%N (0) 1 ∼=1 Tensor%N (0) 2 BqT1-Tensor: Immediate by IH and Lemma 63 (7). ◀ ▶Corollary 66.T (1) 1 ∼=1 T (1)...

  57. [57]

    Case x′=⇒0 x′P0-V ar: We further do the following case analysis: Casex′̸=x: This is immediate since we have[N (0) 0 /x]N (0) = [N′(0) 0 /x]N′(0)=x′

    CasesP0-Cst0,P0-CstP,P0-Delta,P0-AssPass, andP0-RfnPassare trivial. Case x′=⇒0 x′P0-V ar: We further do the following case analysis: Casex′̸=x: This is immediate since we have[N (0) 0 /x]N (0) = [N′(0) 0 /x]N′(0)=x′. Casex′=x: Since[N (0) 0 /x]N (0) =N (0) 0 and[N′(0) 0 /x]N′(0)=N′(0) 0 , we can finish the proof by the assumptionN (0) 0 =⇒0 N′(0) 0 . Case...

  58. [58]

    CasePT0-Code: Straightforward by IH

    CasePT0-Tensor: Trivial. CasePT0-Code: Straightforward by IH. CasesPT0-RfnandPT0-Arr: Straightforward by IH, using the Barendregt convention. 4.All the cases (includingPT1-Tensor) are immediate or straightforward by IH. ◀ 80 Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types Following the approach taken by Takahashi [70], we use conversio...

  59. [59]

    CaseN (0) = (|⟨T (1) 1 ⟩◁⟨T (1) 2 ⟩|)L where eitherT (1) 1 orT (1) 2 is not a type value: By the definition of =⇒0,N′(0)is of the form(|⟨T′(1) 1 ⟩◁⟨T′(1) 2 ⟩|)L, and we haveT (1) 1 =⇒1 T′(1) 1 andT (1) 2 =⇒1 T′(1) 2 . Then, by IH, we haveT′(1) 1 =⇒1 (T (1) 1 )∗andT ′(1) 2 =⇒1 (T (1) 2 )∗, and we can thus derive T′(1) 1 =⇒1 (T (1) 1 )∗ T′(1) 2 =⇒1 (T (1) 2...

  60. [60]

    strictly shorter

    CaseN (1) =∼N(0): We do a further case analysis onN(0): Case N (0) =⟨N (1) 0 ⟩: We first have(N (1))∗= (∼⟨N (1) 0 ⟩)∗= (N (1) 0 )∗. Considering the derivation ofN (1) =⇒1 N′(1), we have the following two cases: 82 Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types ∗ Case ⟨N (1) 0 ⟩=⇒0 N′(0) ∼⟨N (1) 0 ⟩=⇒1∼N′(0)P1-Esc: Wecanfurthertracebac...