data-kinds

14熱

1答えて

GADTとデータ型を組み合わせるのが本当に好きです。以前よりも型の安全性が向上しています（ほとんどの場合、AgqなどのCoqとほとんど同じです）。悲しいことに、最も単純な例ではパターンマッチングは失敗し、型クラス以外の関数を書く方法はないと思います。は、ここに私の悲しみを説明するための例です： data Nat = Z | S Nat deriving Eq data Le :: Nat -