notogawa https://blog.hatena.ne.jp/notogawa/ ぼくのぬまち 出張版 https://notogawa.hatenablog.com/ EmptyCaseが入ってきた．absurd pattern matchingがHaskellで使えるのでHaskell証明士には朗報だ．具体的にEmptyCaseの有無で世界がどう変わるかを把握してる範囲で書く．まず，矛盾(bottom)の扱いについて．矛盾は「値を構成できない型」になればよいので，通常次のいずれかになる． data Bottom data Bottom = Bottom Bottom 直観主義における「矛盾からは何でも導ける(bottom elimination)」は，型としては， bottomElimination :: Bottom -> whatever となるが，今… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fnotogawa.hatenablog.com%2Fentry%2F2014%2F04%2F24%2F001438" title="Haskell定理証明士がEmptyCase拡張によって受ける恩恵と効能 - ぼくのぬまち 出張版" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2014-04-24 00:14:38 rich https://notogawa.hatenablog.com/entry/2014/04/24/001438 1.0 100%