myuon_myon https://blog.hatena.ne.jp/myuon_myon/ Just $ A sandbox https://myuon-myon.hatenablog.com/ Haskell Haskellで型レベルプログラミング(あるいはごく簡単な証明)を書くときに, DataKindsでデータ型をそのまま持ち上げると困る場面がある. {-# LANGUAGE DataKinds, GADTs, TypeOperators, TypeFamilies #-} data a :=: b where Refl :: a :=: a data Nat = Zero | Succ Nat type family (:+:) a b where Zero :+: n = n (Succ n) :+: m = Succ (n :+: m) と定義した時, 「任意の自然数nについてn+0=n」… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fmyuon-myon.hatenablog.com%2Fentry%2F2015%2F06%2F14%2F222142" title="DataKindsとGADTの使い方について - Just $ A sandbox" 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 2015-06-14 22:21:42 rich https://myuon-myon.hatenablog.com/entry/2015/06/14/222142 1.0 100%