Earn extra honor and gain new allies!
Honor is earned for each new codewarrior who joins.
Learn more
  • 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.

    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
    
    
  • 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:

    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
    
  • 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 very last 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 hard about 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

    powerset :: [a] -> [[a]]
    powerset = filterM $ const [False, True]
    
  • 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] = 20 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...