Is flattening a list easier in dependently typed functional programming languages?

You can make a function like that in Haskell where you don't need to specify the output type:

{-# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts #-}

type family FlatT a where
  FlatT [[a]] = FlatT [a]
  FlatT a = a

class Flat a where
  flat :: a -> FlatT a

instance Flat [a] => Flat [[a]] where
  flat xs = flat $ concat xs

instance {-# OVERLAPPABLE #-} FlatT a ~ a => Flat a where
  flat x = x

main = print $ flat [["Hello"," "],["World", "!"]]

One problem that still occurs is the fact that you might have a polymorphic type contained in your lists which itself might be a list. For example you can write a list of integers:

main = print $ flat [[1,2],[3,4,5]]

Which will give many errors about ambiguous variables. A simple fix is to add a type signature to one of the integers: [[1,2],[3,4,5 :: Int]]. That will fix all errors. And in some sense this error feels to me like it is unavoidable, because you can write an instance like this:

instance Num [Int] where
  fromInteger n = replicate (fromInteger n) (fromInteger n)

And then you can use it like this:

main = print $ [[1,2],[3,4,5 :: [Int]]]

Which will return:

[1,2,2,3,3,3,4,4,4,4,5,5,5,5,5]

As you can see, this unwraps one layer extra. So the number of layers that are unwrapped depends on the type you give in the signature. To me that sounds like it is not possible to avoid the type signature, even in more powerful languages.

A common way in Haskell to mimic “arbitrarily deeply nested lists” is to use free monads.

Free monads are included in the language library, as package Control.Monad.Free.

so we can attempt to implement “multi-level lists” as the MLL type transformer:

import  Control.Monad
import  Control.Monad.Free

-- Multi-Level List:
type MLL = Free []

mllJoin :: [MLL a] -> MLL a
mllJoin = Free

mllWrap  :: a -> MLL a
mllWrap = return

Now the question is: how could we flatten such an object ? Well, a possible remark is that, if the functor argument ft of the Free type constructor is an instance of the Foldable class, then so is Free ft.

Hence, as [] is foldable, so is our MLL type transformer.

The type of foldr, for example:

foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b

can be specialized like this:

foldr :: (a -> acct -> acct) -> acct -> MLL a -> acct

with acct as the accumulator type.

This gives the idea to pick acct as [a], and to have cons as the functional argument of foldr. Like this:

mllFlatten :: MLL a -> MLL a
mllFlatten xs  =  let  fl1 = foldr (:) [] xs
                  in   mllJoin (fmap mllWrap fl1)

Test program:

main :: IO ()
main = do
    -- try build a small multilevel structure as zs:
    let  xs = (mllJoin [ mllWrap 41, mllWrap 42 ]) :: (MLL Integer)
         ys =  mllJoin [ xs, mllWrap 43 ]
         zs =  mllJoin [ mllWrap 40, ys, mllWrap 44 ]
    putStrLn $ "zs = " ++ (show zs)
    
    -- display structure of zs:
    let  zsImage = filter  (\ch -> not (elem ch "Pure Free"))  (show zs)
    putStrLn $ "zsImage = " ++ zsImage

    -- flattening zs:
    let  fzs = mllFlatten zs
    putStrLn $ "Flattened zs = " ++ (show fzs)

    -- display structure of flattened zs:
    let  fzsImage = filter  (\ch -> not (elem ch "Pure Free"))  (show fzs)
    putStrLn $ "fzsImage = " ++ fzsImage

Test program output:

zs = Free [Pure 40,Free [Free [Pure 41,Pure 42],Pure 43],Pure 44]
zsImage = [40,[[41,42],43],44]
Flattened zs = Free [Pure 40,Pure 41,Pure 42,Pure 43,Pure 44]
fzsImage = [40,41,42,43,44]

Hence, it seems that fold'ing the structure does flatten it.

Generics is a good tool for tasks like this. If your type is an instance of Data you can write

import Data.Generics
import Control.Monad
gFind :: (MonadPlus m, Data a, Typeable b) => a -> m b
gFind = msum . map return . listify (const True)

So,

λ> gFind [[1,2],[3,4,5]] :: [Integer]
[1,2,3,4,5]
λ> gFind ((1,"b"),(2,"d","e")) :: [Integer]
[1,2]

Since you want to see how it can be done in Coq, I propose here a simple solution.

From Coq Require Import Utf8 List.
Import ListNotations.

Fixpoint flatten {A} (l : list (list A)) : list A :=
  match l with
  | x :: l => x ++ flatten l
  | [] => []
  end.

(* Nested list type *)
Fixpoint nlist (n : nat) (A : Type) : Type :=
  match n with
  | 0 => A
  | S n => list (nlist n A)
  end.

Fixpoint nflatten {n A} (l : nlist n A) : list A :=
  match n as m
  return nlist m A → list A
  with
  | 0 => λ x, [ x ]
  | S n => λ l, flatten (map nflatten l)
  end l.

Eval compute in
nflatten (n := 2) [
  [ 1 ; 2 ; 3 ] ;
  [ 4 ; 5 ] ;
  [] ;
  [ 6 ]
].
(* = [1; 2; 3; 4; 5; 6]
     : list nat *)

Eval compute in
nflatten (n := 3) [
  [ [1] ; [2 ; 3] ] ;
  [ [4 ; 5] ] ;
  [] ;
  [ [6] ]
].
(* = [1; 2; 3; 4; 5; 6]
     : list nat *)

I first redefine flatten in a naive way and then I define a type of nested lists nlist that comes with a natural number corresponding to the depth. I assume that you want a constant depth in all your lists, otherwise the solution would be slightly more complicated.

Then nflatten will simply do a case analysis on the natural number to do the flattening.