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

ProjectEuler1and2.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}

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

newtype Fix a = In { out :: Fix a -> a }

-- GHC's inliner will blow up if this is allowed to inline
{-# NOINLINE diag #-}
diag = \x -> out x x

omega = diag (In diag)

fix = \f -> diag (In (\x -> f (out x x)))

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)
badd = fix (\badd x y ->
  let
    bsuc = \x -> badd x b1
    badd1 = fix (\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
    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)
bsuc = \x -> badd x b1

b2 = bsuc b1
b2e0 = b1
b2e1 = BNat (\e _ _ -> e b2e0)
b2e2 = BNat (\e _ _ -> e b2e1)
b2e3 = BNat (\e _ _ -> e b2e2)
b2e4 = BNat (\e _ _ -> e b2e3)
b2e5 = BNat (\e _ _ -> e b2e4)
b2e6 = BNat (\e _ _ -> e b2e5)
b2e7 = BNat (\e _ _ -> e b2e6)
b2e8 = BNat (\e _ _ -> e b2e7)
b2e9 = BNat (\e _ _ -> e b2e8)
b2e10 = BNat (\e _ _ -> e b2e9)
b2e11 = BNat (\e _ _ -> e b2e10)
b2e12 = BNat (\e _ _ -> e b2e11)
b2e13 = BNat (\e _ _ -> e b2e12)
b2e14 = BNat (\e _ _ -> e b2e13)
b2e15 = BNat (\e _ _ -> e b2e14)
b2e16 = BNat (\e _ _ -> e b2e15)
b2e17 = BNat (\e _ _ -> e b2e16)
b2e18 = BNat (\e _ _ -> e b2e17)
b2e19 = BNat (\e _ _ -> e b2e18)
b2e20 = BNat (\e _ _ -> e b2e19)
b2e21 = BNat (\e _ _ -> e b2e20)
b4000000 = badd b2e21 (badd b2e20 (badd b2e19 (badd b2e18 (badd b2e16 (badd b2e11 b2e8)))))
bcmp = fix (\bcmp x y lt eq gt -> unBNat x
  (\x' -> unBNat y
    (\y' -> bcmp x' y' lt eq gt)
    (\y' -> bcmp x' y' lt lt gt)
    (bcmp x' b0 lt eq gt))
  (\x' -> unBNat y
    (\y' -> bcmp x' y' lt gt gt)
    (\y' -> bcmp x' y' lt eq gt)
    gt)
  (unBNat y
    (\y' -> bcmp b0 y' lt eq gt)
    (\_ -> lt)
    eq))

pe1 =
  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))

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

pe2 = fix
  (\f s x y ->
    let
      s' = unBNat x (\_ -> badd s x) (\_ -> s) s
      r = f s' y (badd x y)
    in
      bcmp x b4000000 r r s)
  b0
  b1
  b2

-- >>> pe2
-- 4613732

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