制約解決の部分は今までいいかげんでしたね。そもそも、連立不等式系なので、解があっても一意的に決まるわけではない。なにか「最適性」の基準を決めて、「制約（不等式の集まり）を満たしてコレコレを最大にする」ような最適解の問題にできればいいのだけ…

不等式的な型付けとは、ワイヤー（パイプ）が1本あると、その両端に型がラベルされる型付けの方法。普通の圏論だと、f:A→B, g:C→D が結合可能なのは B = C のときだけだが、Catyでは B = C は要求しない。B ⊆ C という集合の包含に関する不等式を要求する。…

お絵描き圏論とCatyScriptの変数など - 檜山正幸のキマイラ飼育記 とか 変数なしプログラミングとお絵描き圏論 - 檜山正幸のキマイラ飼育記 とかにデータフローグラフの例はある。ボックス＆ワイヤーの絵を描けばいいのだが、ワイヤリングのための特殊なノー…

次の5段階になるかな。 式（スクリプトコード）からデータフローグラフを作る。 データフローグラフをもとに、不等式版の型単一化を行い制約系（連立不等式系）を作る。 制約系（連立不等式系）は論理式なので、推論により論理式を簡約する（より短く単純な…

これから、型検査と制約解決の解説をするが、絵を使う。本質的にCatyScriptは絵図言語なので。既に絵を描いてスキャンした。が、見直したら細部（でもないか？）では絵が間違っている。直すのはめんどくさいので、絵はそのまま使う。いちおう修正は入れるが…

静的型検査のアルゴリズムは、2009年末から2010年はじめに（2010-01-05, 2010-01-11）だいたいは考えた。その手順を述べると： スクリプトコードからデータフローグラフを作る。（プログラムで実行するなら記号的な操作となる。） データフローグラフのワイ…