Solving project euler 1 in pure lambda calculus (embedded in Haskell)

ProjectEuler1.hs

newtype SNat = SNat { unSNat :: forall x. (SNat -> x) -> x -> x }
newtype CNat = CNat { unCNat :: forall x. (x -> x) -> x -> x }
newtype Quad a b c d = Quad { unQuad :: forall x. (a -> b -> c -> d -> x) -> x }
newtype BNat = BNat { unBNat :: forall x. (BNat -> x) -> (BNat -> x) -> x -> x}

test =
  let
    ssuc = \x -> SNat (\s _ -> s x)
    s0 = SNat (\_ z -> z)
    s2 = ssuc (ssuc s0)
    s4 = ssuc (ssuc s2)
    ctimes = \x y -> CNat (\s z -> unCNat x (unCNat y s) z)
    c10 = CNat (\s z -> s (s (s (s (s (s (s (s (s (s z))))))))))
    c1000 = ctimes c10 (ctimes c10 c10)
    quad = \a b c d -> Quad (\f -> f a b c d)
    b0 = BNat (\_ _ z -> z)
    b1 = BNat (\_ o _ -> o b0)
    b2n = \x -> BNat (\e _ _ -> e x)
    b2n1 = \x -> BNat (\_ o _ -> o x)
    bsuc = \x -> badd x b1
    badd = \x y -> unBNat x (\x' -> unBNat y (\y' -> b2n (badd x' y')) (\y' -> b2n1 (badd x' y')) (b2n x')) (\x' -> unBNat y (\y' -> b2n1 (badd x' y')) (\y' -> b2n (badd1 x' y')) (b2n1 x')) y
    badd1 = \x y -> unBNat x (\x' -> unBNat y (\y' -> b2n1 (badd x' y')) (\y' -> b2n (badd1 x' y')) (b2n1 x')) (\x' -> unBNat y (\y' -> b2n (badd1 x' y')) (\y' -> b2n1 (badd1 x' y')) (b2n (bsuc x'))) (bsuc y)
  in
    unCNat c1000
      (\x -> unQuad x (\i r t f ->
        let
          i' = bsuc i
          r' = badd i r
        in
          unSNat t
            (\t' -> unSNat f
              (\f' -> quad i' r t' f')
              (quad i' r' t' s4))
            (unSNat f (\f' -> quad i' r' s2 f') (quad i' r' s2 s4))))
      (quad b0 b0 (ssuc s2) (ssuc s4))

instance (Show a, Show b, Show c, Show d) => Show (Quad a b c d) where
  show q = unQuad q (\a b c d -> show (a,b,c,d))
instance Show CNat where
  show cn = show $ unCNat cn (+ 1) 0
instance Show SNat where
  show sn = show (go 0 sn) where
    go s sn = unSNat sn (go (1 + s)) s
instance Show BNat where
  show bn = show (go 0 0 bn) where
    go i s bn = unBNat bn (go (i + 1) s) (go (i + 1) (2 ^ i + s)) s

-- >>> test
-- (1000,233168,2,0)

Since writing this I've solved more problems and made a proper repo: https://github.com/noughtmare/project-euler-lambda/blob/main/Main.hs