No, it is not abuse of logic: fix (S . (* Z)) should have 1 === S Z as fixpoint, because S . (* Z) $ S Z = S Z (1 + 1 * 0 = 1); and your definition successfully yields it for fix (S . (Z *)) = S Z.

There is indeed no nice definition that makes it work with both left and right multiplication. An explicit case would work i think, but that's ugly.

I guess there is no nice solution, because it is abuse of the logic anyway. Having 0 times infinity be 0 is wrong in most of mathematics. But ultimately, this logic does not have room for infinity in the first place.

module Counting.Preloaded where
import Control.Arrow ((***))
data Nat = Z | S Nat deriving (Show, Eq, Ord)
nat :: a -> (Nat -> a) -> Nat -> a
nat a _ Z = a
nat _ aa (S n) = aa n
iterNat :: (a -> a) -> Nat -> (a -> a)
iterNat _ Z = id
iterNat aa (S n) = aa . iterNat aa n
natUnderflow :: String
natUnderflow = "Nat is non-negative"
instance Num Nat where
(+) = iterNat S
a * b = iterNat (b+) a Z
a - Z = a
Z - b = error natUnderflow
S a - S b = a - b
abs = id
signum Z = Z
signum (S _) = S Z
fromInteger x
| x < 0 = error natUnderflow
| x == 0 = Z
| otherwise = S $ fromInteger $ x - 1
instance Enum Nat where
toEnum x
| x < 0 = error natUnderflow
| x == 0 = Z
| otherwise = S $ toEnum $ x - 1
fromEnum x = iterNat (+1) x 0
instance Real Nat where toRational = toRational . fromEnum
instance Integral Nat where
quotRem a Z = error "divide by zero"
quotRem a b = until ((< b) . snd) (S *** subtract b) (Z, a)
divMod = quotRem
toInteger n = iterNat (+1) n 0

I have updated description ("Order of inhabitants in infinite lists won't be tested."), hope it clarifies it. It was complementary task, so I think strictness is unnecessary.

module Counting.Preloaded where
import Control.Arrow ((***))
data Nat = Z | S Nat deriving (Show, Eq, Ord)
nat :: a -> (Nat -> a) -> Nat -> a
nat a _ Z = a
nat _ aa (S n) = aa n
iterNat :: (a -> a) -> a -> Nat -> a
iterNat _ a Z = a
iterNat aa a (S n) = iterNat aa (aa a) n
natUnderflow :: String
natUnderflow = "Nat is non-negative"
instance Num Nat where
(+) = iterNat S
a * b = iterNat (+a) Z b
a - Z = a
Z - b = error natUnderflow
S a - S b = a - b
abs = id
signum Z = Z
signum (S _) = S Z
fromInteger x
| x < 0 = error natUnderflow
| x == 0 = Z
| otherwise = S $ fromInteger $ x - 1
instance Enum Nat where
toEnum x
| x < 0 = error natUnderflow
| x == 0 = Z
| otherwise = S $ toEnum $ x - 1
fromEnum = iterNat (+1) 0
instance Real Nat where toRational = toRational . fromEnum
instance Integral Nat where
quotRem a Z = error "divide by zero"
quotRem a b = until ((< b) . snd) (S *** subtract b) (Z, a)
divMod = quotRem
toInteger = iterNat (+1) 0

This took me quite a few days to figure out and I had to read half a book on category theory, but once I had my "Eureka!" moment, everything became very simple and straightforward. To those stuck on the counting challenges, here is a hint (hopefully not too much of a spoiler) - think long and hard about what isomorphism really means and what it entails ... ;)

No, it is not abuse of logic:

`fix (S . (* Z))`

should have 1 ===`S Z`

as fixpoint, because`S . (* Z) $ S Z = S Z`

(1 + 1 * 0 = 1); and your definition successfully yields it for`fix (S . (Z *)) = S Z`

.Thanks for the update.

There is indeed no nice definition that makes it work with both left and right multiplication. An explicit case would work i think, but that's ugly.

I guess there is no nice solution, because it is abuse of the logic anyway. Having 0 times infinity be 0 is wrong in most of mathematics. But ultimately, this logic does not have room for infinity in the first place.

Just in case: it has changed slightly.

This comment is hidden because it contains spoiler information about the solution

This comment is hidden because it contains spoiler information about the solution

I have updated description ("Order of inhabitants in infinite lists won't be tested."), hope it clarifies it. It was complementary task, so I think strictness is unnecessary.

Thanks a lot!

Here:

Can you publish the Counting.Preloaded for local testing?

nice kata

— andrei-bolkonsky

This comment is hidden because it contains spoiler information about the solution

Damn - that

verylast part on generating a list of all possible functions`a -> b`

was tricky - I got tripped up on it for quite a while ;)This took me quite a few days to figure out and I had to read half a book on category theory, but once I had my "Eureka!" moment, everything became very simple and straightforward. To those stuck on the counting challenges, here is a hint (hopefully not too much of a spoiler) - think

long and hardabout what isomorphism really means and what it entails ... ;)In addition, according to the approach, mentioned in that paper, you could implement set of all subsets in haskell as

Good question)

Yes, when

`count @t`

is infinity we could not conclude, that`t`

is countable (in mathematical sense).So ℵ

_{0}=`count @Nat < count @[Nat]`

= 2^{ℵ0}in terms of cardinal numbers,and type/set

`t`

is countable iff`count @t == count @Nat`

.We can not express such things in haskell, so when infinity, we just write all formally.

Also if

`count @x >= 2`

then type`Nat -> x`

is not countable.## Loading more items...