テンソル形状のコンパイル時検査＋実行時アサーション化を今のHaskellで書いてみる - Qiita

はじめに Edward Z. Yang 氏の記事 A compile-time debugger that helps you write tensor shape checks は、テンソルの形状の検査を依存型でコンパイル時に対話的にやりつつ、静的に決まらない部分や静的な検証が難しい部分はアサーションとして実行時検査に遅延するという仕組みの提案。 対話的なアサーションの挿入部分とかはともかく、型付けとアサーションの部分は今のHaskellでも大体出来るなぁと思ったので試しに書いてみた。 (元記事自体Haskellっぽい構文で書かれているし、 Edward Z. Yang 氏自身、ここまでは出来るのは当然知って書いているのだと思うけれど) 結果 元記事での、アサーションを挿入した最終的なプログラムは以下: main() { x = load("tensor1.t") y = load("t