読者です 読者をやめる 読者になる 読者になる

夜も眠れない

「プログラミングHaskell*1を読んでいて、p.123にかっちょいいaddの定義が載っていて、ぜひmulも欲しかったので、ちょっと考えてみたが、挫折した。格好良くないのだ。

data Nat = Zero | Succ Nat
	deriving (Eq, Ord, Show, Read)

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

mul :: Nat -> Nat -> Nat
mul a b = mul b a
mul Zero n = Zero
mul (Succ Zero) n = n
mul m (Succ n) = add m (mul m n)

だと

Main> :l a.hs
[1 of 1] Compiling Main             ( a.hs, interpreted )

a.hs:9:0:
    Warning: Pattern match(es) are overlapped
             In the definition of `mul':
                 mul Zero n = ...
                 mul (Succ Zero) n = ...
                 mul m (Succ n) = ...
Ok, modules loaded: Main.
Main>

交換法則を直接書くのはこういうやり方じゃダメなのかw
というわけで、実直に書いてみた。でも、addだと片方だけでいいのはなんでかなー。評価の順序としてそうだってことだっけか。よくわかって無い俺。

data Nat = Zero | Succ Nat
	deriving (Eq, Ord, Show, Read)

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

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

すると、、

Main> mul Zero Zero
Zero
Main> mul (Succ Zero) Zero
Zero
Main> mul Zero (Succ Zero)
Zero
Main> mul (Succ Zero) (Succ Zero)
Succ Zero
Main> mul (Succ Zero) (Succ (Succ Zero))
Succ (Succ Zero)
Main> mul (Succ (Succ (Succ Zero))) (Succ (Succ Zero))
Succ (Succ (Succ (Succ (Succ (Succ Zero)))))
Main>

ということでとりあえず寝る、じゃなくて仕事再開する。

もうやらないとかいいながら

どうしても腑に落ちないので、単位元の定義をすっ飛ばしてみた

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

こうなると、変形のパターンがやっと見えてきて、もうひとつも不要だとわかった。

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

で、addを使わずにmulだけってのは、、、というかその逆はどうか、というとエフイチの世界になってしまうのか(本当ですか?)
あ、addと合わせないと格好悪い、、、

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

もー、センス無いなぁ、やんなっちゃう。
だから、結局割り算はまともにできなかった。切り上げになってしまう。

sub :: Nat -> Nat -> Nat
sub Zero n = Zero
sub n Zero = n
sub (Succ n) (Succ m) = sub n m

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

*1:[asin:4274067815:detail]