hpastetwo

newtype Id a = Id a

newtype Const a b = Const a

data Pair f fs a = Pair (f a) (fs a)

data Unary f fs a = Z (fs (fs a)) | S (Unary f (Pair f fs) a)

type Square = Unary Id (Const ())

zero :: Square a
zero = Z (Const ())

one :: Square Int
one = S (Z (Pair (Id (Pair (Id 1) (Const ()))) (Const ())))

two :: Square Int
two = S . S . Z $ Pair (Id $ Pair (Id 1) $ Pair (Id 2) $ Const ())
                $ Pair (Id $ Pair (Id 3) $ Pair (Id 4) $ Const ())
                $ Const ()

data Nil a = Nil

infixr 6 `Cons`
data Cons fs a = Cons a (fs a)

data Unary fs a = Z (fs (fs a)) | S (Unary (Cons fs) a)

type Square = Unary Nil

zero :: Square a
zero = Z Nil

one :: Square Int
one = S . Z $ (1 `Cons` Nil) `Cons` Nil

two :: Square Int
two = S . S . Z $      (1 `Cons` 2 `Cons` Nil)
                `Cons` (3 `Cons` 4 `Cons` Nil)
                `Cons` Nil

size' :: Unary fs a -> Int
size' (Z _) = 0
size' (S s) = 1 + size' s

size :: Square a -> Int
size = size'

instance Functor fs => Functor (Cons fs) where
  fmap f (Cons a fs) = Cons (f a) (fmap f fs)

instance Functor Nil where
  fmap _ Nil = Nil

instance Functor fs => Functor (Unary fs) where
  fmap f (Z ffs) = Z $ fmap (fmap f) ffs
  fmap f (S n)   = S (fmap f n)

instance Foldable Nil where
  foldr f z Nil = z

instance Foldable fs => Foldable (Cons fs) where
  foldr f z (Cons a fs) = a `f` foldr f z fs

instance Foldable fs => Foldable (Unary fs) where
  foldr f z (Z ffs) = foldr (flip $ foldr f) z ffs
  foldr f z (S n)   = foldr f z n

instance Traversable Nil where
  traverse _ Nil = pure Nil

instance Traversable fs => Traversable (Cons fs) where
  sequenceA (Cons ma fms) = Cons <$> ma <*> sequenceA fms

instance Traversable fs => Traversable (Unary fs) where
  sequenceA (Z ffms) = Z <$> sequenceA (fmap sequenceA ffms)
  sequenceA (S n)    = S <$> sequenceA n