DROPS

Document

DOI: 10.4230/LIPIcs.ECOOP.2026.28

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

Authors: Takashi Suwa and Atsushi Igarashi

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

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 will be immediately detected as 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.

Cite as

Takashi Suwa and Atsushi Igarashi. Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 28:1-28:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{suwa_et_al:LIPIcs.ECOOP.2026.28,
  author =	{Suwa, Takashi and Igarashi, Atsushi},
  title =	{{Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types}},
  booktitle =	{40th European Conference on Object-Oriented Programming (ECOOP 2026)},
  pages =	{28:1--28:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-423-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{372},
  editor =	{Krebbers, Robbert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.28},
  URN =		{urn:nbn:de:0030-drops-261247},
  doi =		{10.4230/LIPIcs.ECOOP.2026.28},
  annote =	{Keywords: Metaprogramming, Staged computation, Dependent types, Refinement types, Tensor shape checking}
}

Document

Artifact

DOI: 10.4230/DARTS.12.1.14

Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types (Artifact)

Authors: Takashi Suwa

Published in: DARTS, Volume 12, Issue 1, Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract

Based on the method proposed in the corresponding paper, we implemented a prototype type-checker (and a simple interpreter) for compile-time tensor shape checking. we ported a number of DNN-related example programs offered by ocaml-torch to our language and checked them by using the prototype implementation. The results indicated that our method can be considered effective enough to accommodate realistic tensor-handling programs.

Cite as

Takashi Suwa. Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 14:1-14:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{suwa:DARTS.12.1.14,
  author =	{Suwa, Takashi},
  title =	{{Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types (Artifact)}},
  pages =	{14:1--14:5},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2026},
  volume =	{12},
  number =	{1},
  editor =	{Suwa, Takashi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.14},
  URN =		{urn:nbn:de:0030-drops-261517},
  doi =		{10.4230/DARTS.12.1.14},
  annote =	{Keywords: Metaprogramming, Staged computation, Dependent types, Refinement types, Tensor shape checking}
}

Search Results

Documents authored by Suwa, Takashi

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

Abstract

Cite as

Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types (Artifact)

Abstract

Cite as

Thanks for your feedback!

Could not send message