実世界を扱う依存型プログラミングのたぶん基本～外界から安全な世界までの道 - ぼくのぬまち 出張版

依存型ならさらに安全にプログラミングできちまうんだ！と言ったところで，「無料で遊べちまうんだ！」とか「3000円払えば無料で10連まわせる」みたいな感があり， 依存型使わない場合とどう違ってくるのか 入出力から扱い始めるとどういった形のプログラムになるのか 大概どういう流れでプログラミングすることになるのか とか，そういった話を通しではそんなに見ないかなーという気がしたので，ごく基本的なものを一通りまとめておこうと思って． まず，説明に使う問題設定について．行列演算，特に行列積を考えてみる．ただし，行列の形(行はいくつ，列はいくつ)についてはプログラムの外から入力によって決定するような状況とする．これ自体は普通の問題設定だと思われる． 依存型を使わなければ特にどうということも無い．恐らく行列の型を次のように定義し， -- 形のみ持っておき，中身の数値については簡単のため省略 data Ma

[xiangze]

[[programming][依存型]

[pandaman64]

先行研究

[nanakoso]

依存型

[ilyaletre]

singletonはagdaの世界では不要っぽい。

[jinjor]

"型合わせゲー"

[kazeula]

いわゆる動的型付け言語とは違う方法で動的型検査をやってるように見える。面白いなー。

[teracy_junk]

『依存型ならさらに安全にプログラミングできちまうんだ！と言ったところで，「無料で遊べちまうんだ！」とか「3000円払えば無料で10連まわせる」みたいな感があり』

[lotz84]

IOの例があって依存型の使い方がわかりやすい

[ruicc]

Agdaチュートリアルが始まるのかと思ったがHaskell