ナチュラルナンバー算術をゼロから実装する際のトラブル

Question

私はLYAHを経てきましたが、ハスケルの紹介はあまり良くありません。リチャード・バードの「Haskellを使った関数型プログラミング入門」を勧めた「Haskellへの優しい導入」に出くわしました。それは私が今読んでいる本です。第3章ではNat型のデータ型を作成し、基本的な算術演算を実装しています。

これは私が今まで書かれているコードです：

module Main where 
import Prelude hiding ((^^)) 

data Nat = Zero | Succ Nat 
     deriving (Eq, Ord, Show) 
xx :: Nat -> Nat -> Nat 
m `xx` Zero = Zero 
m `xx` Succ n = (m `xx` n) `add` m 

(^^) :: Nat -> Nat -> Nat 
m ^^ Zero = Succ Zero 
m ^^ Succ n = (m ^^ n) `xx` m 

add :: Nat -> Nat -> Nat 
m `add` Zero = m 
m `add` Succ n = Succ(m `add` n) 

factsu :: Nat -> Nat 
factsu Zero  = Succ Zero 
factsu (Succ n) = Succ n `xx` factsu n 

--Zero = 0 

showNat :: Nat -> String 
showNat Zero = "Zero" 
showNat (Succ Zero) = "Succ Zero" 
showNat (Succ (Succ n)) = "Succ (" ++ showNat (Succ n) ++ ")" 

main :: IO() 
main = return() 

これは何が起こるかです：

factsu Zero 
Succ Zero 
it :: Nat 

私は成功回数とゼロを定義するにはどうすればよいですか？

Answer 1

は、しかし、私は「私が等しい0からZeroをしたい」ゼロは根本的な問題は、あなたが何を意味です0

等しくなるようにしたいです。それを読むのが「私はZero == (0 :: Integer)がほしい」かもしれませんが、それは不可能です。Zeroと0 :: Integerのタイプが異なります。Zeroは実際には独自のものです。あなただけのGHCiのは...「0」として

GHCi> Zero 
0 

をZeroを印刷したい場合は、一方

natToInteger :: Nat -> Integer 
integerToNat :: Integer -> Maybe Nat 

：何ももちろん、それらの間の相互変換機能を定義するから、あなたを停止しません。 ..あなたが必要とするのは、Showというカスタムのインスタンスです.karakfaとleftaroundaboutはin the commentsを提案しています。しかし、実際にはZeroの内容は変更されません。あなたはそれが表示される方法を変えるだけです。

最後に、第三の可能性はあなたのNat秒間数値リテラル構文を使用したいということです：

あなたが Nat Numインスタンスを与えれば、実際に可能である

GHCi> 0 + 2 :: Nat 
2 
it :: Nat 

。しかし、(-)は部分的であり、negateの妥当な実装はありません（ちなみに、Maybeを上記のintegerToNatの署名に入れている理由もあります）。また、Showの場合と同様に、Numインスタンスを追加しても、実質的にはNatの内容は変更されません。特に、数字のリテラル構文は構文だけです。

^{（あなたは物事はあなたが彼らと何ができるかによって特徴づけられるという観点を取る場合は、「本質的」で私が何を意味するか疑問かもしれません。。しかし、我々はあまりにも横道にそれる前に、私はここで停止します）}