fully linear sort, no with-clauses, no mutual recursion

fully_linear_sort.hs

module Main where

data Nat  = Z | S Nat deriving Eq
data Nats = N | C Nat Nats deriving Eq
data Bit  = T | F deriving Eq

-- Sort
-- ----

tmap :: (Nat -> Nat) -> (Nat -> Nat) -> (Nat, Nat) -> (Nat, Nat)
tmap f g (a, b) = (f a , f b)

order :: Nat -> Nat -> (Nat, Nat)
order Z     y     = (Z, y)
order x     Z     = (Z, x)
order (S n) (S m) = tmap S S (order n m)

insert_go :: (Nat, Nat) -> (Nat -> Nats -> Nats) -> (Nat -> Nats) -> Nats
insert_go (x, y) c f = c x (f y)

insert :: Nats -> (Nat -> Nats -> Nats) -> Nat -> Nats
insert N        c x = c x N
insert (C y ys) c x = insert_go (order x y) C (insert ys c)

sort :: Nats -> Nats
sort N        = N
sort (C x xs) = insert (sort xs) C x

-- Main
-- ----

int :: Nat -> Int
int Z     = 0
int (S n) = 1 + int n

nat :: Int -> Nat
nat n | n <= 0 = Z
nat n | n >  0 = S (nat (n - 1))

nats :: [Int] -> Nats
nats []     = N
nats (x:xs) = C (nat x) (nats xs)

ints :: Nats -> [Int]
ints N        = []
ints (C x xs) = int x : ints xs

main :: IO ()
main = print $ ints $ sort $ nats [3, 1, 4, 1, 5, 9, 2, 6]