Nested nested lists in Haskell

nested_lists.hs

{-# LANGUAGE TypeFamilies, DataKinds, GADTs #-}

-- Wrap the doll one level.
matryoshka :: a -> [a]
matryoshka x = [x]

-- The type of unary natural numbers.
-- With the help of 'DataKinds' extension, we get a corresponding
-- 'Nat' type which we can use to index the 'NestedList' type.
data Nat = Zero | Succ Nat

-- Define the types of n-nested lists via 'TypeFamilies'.
-- Type families allow to perform type-level computation,
-- the 'Nat' kind we use here is promoted from the previous type.
type family NestedList (n :: Nat) a
type instance NestedList Zero     a = a
type instance NestedList (Succ n) a = [NestedList n a]

-- Problem! We cannot write the following function:
--
-- > doll :: a -> NestedList n a
--
-- because there's no way to obtain an 'n' from the context.

-- The customary solution is to create a singleton type which allows
-- you to construct values which reflect the type we want to get.
-- This is done using a Generalized Algebraic Data Type (GADT),
-- where the index (the 'n' variable) is the type we need.
data SingNat n where
  SingZero :: SingNat Zero
  SingSucc :: SingNat n -> SingNat (Succ n)

singThree :: SingNat (Succ (Succ (Succ Zero)))
singThree = SingSucc $ SingSucc $ SingSucc $ SingZero

-- Now we can finally write the doll function!
doll :: SingNat n -> a -> NestedList n a
doll SingZero     x = x
doll (SingSucc n) x = [doll n x]

-- This is an example of the use of doll.
-- Notice that we had to give a SingNat argument to it.
doll3 :: a -> [[[a]]]
doll3 x = doll singThree x

-- Note that cannot write a function
--
-- > fromInteger :: Integer -> SingNat n
--
-- because in Haskell types cannot depend on values.
-- If you want to do so, you need dependent types, which you
-- can taste by using Agda or Idris.