![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Yes, I have been reading Okasaki ...
What do you mean, it's computationally foolish to define arithmetic using the Peano axioms?
>pinc [] = [1]
>pinc [1] = [0,1]
>pinc (0:u:xs) =
> if (head (pinc xs) == 0) then (u+head (pinc xs) : drop 1 (pinc xs))
> else (u : pinc xs)
>pinc (1:t:xs) = 0:t+1:xs
>pinc (u:xs) = 0:1:u-1:xs
>pnums = iterate pinc []
>pinc [] = [1]
>pinc [1] = [0,1]
>pinc (0:u:xs) =
> if (head (pinc xs) == 0) then (u+head (pinc xs) : drop 1 (pinc xs))
> else (u : pinc xs)
>pinc (1:t:xs) = 0:t+1:xs
>pinc (u:xs) = 0:1:u-1:xs
>pnums = iterate pinc []
no subject
Efficiency, not that you care:
Don't repeat calls to the same thing, there's no guarantee you'll get CSE.
More idiom: it's often nicer to use pattern matching than head/tail everywhere.
Algebra: if head (pinc xs) == 0 then u + head (pinc xs) == u
So...
pinc (0:u:xs) = case pinc xs of
(0:as) -> u:as
as@(_:_) -> u:as