data Nat = Zero | Succ Nat は自然数ではない?
@t_udaさんのつぶやきが元ネタ。
なぜNat型が自然数ではないかと言うと、次のようなNat型の値が存在するから。
x = Succ x
以下Nat型が自然数ではないことの、限りなく怪しい証明。
まずNat型が自然数だと仮定する。この時、上のようなxはZeroにSuccをk回(kは自然数)適用した値と等しくならない。もし等しくなるとすると、「Succ x = Succ y ならば x = y」というペアノの公理の一つを繰り返し適用することによって Succ x = Zero が導けるが、これはペアノの公理に反する。ここでNat型の値の集合から x = Succ x となるようなxを除いた新しい集合を考えると、この集合はペアノの公理の数学的帰納法に関する項目の要請を満たすので、全ての自然数はこの新しい集合に含まれるはずだが、これはNat型が自然数であるという仮定に反する。(以上妄想終わり)
上の話はともかくとして、x = Succ x というようなxがNat型の値として認められてしまうのはあんまり嬉しくない気がする。こんなxをShowしようとすると無限にSuccを表示しようとして死んでしまうし、他にも例えばReal World Haskell五章に以下のようなJSONデータ型が定義されていて、
data JValue = JString String | JNumber Double | JBool Bool | JNull | JObject [(String, JValue)] | JArray [JValue] deriving (Eq, Ord, Show)
これを印字するために以下のような関数が定義されているけど(一部抜粋)、
renderValue (JString s) = show s ... renderValue (JArray a) = "[" ++ values a ++ "]" where values [] = "" values vs = intercalate ", " (map renderJValue vs)
この関数に x = JArray [x] なんて投げたら無限ループに陥ってしまう。
こんなxを受け入れる利点があるのか、それともエラーにするのが難しいのか、どっちなんだろう?