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

While looking for a function in haskell that flattens arbitrarily deeply nested lists, i.e. a function that applies concat recursively and stops at the last iteration (with a non-nested list), I noted that this would require to have a more flexible type system because with varying list depth, the input type varies as well. Indeed, there are several stackoverflow question - such as this one - in which the responses state that "there cannot exist a function that will 'look' at different nested lists at different depths".

EDIT: Some answers provide workarounds in haskell, either for custom data types or with the help of TypeFamilies or MultiParamTypeClasses (as in the answer by Noughtmare below or the answer by 'Landei' in the post above or the answer by 'John L' in this post). However, those Families and Classes also seem to have been introduced for the lack of / to substitute dependent types in haskell (for example, the haskell wiki states "Type families are [...] much like dependent types".

My question now is if it is true that haskell was indeed originially not made for defining such functions (that e.g. flatten lists of different depths) and, furthermore, if such problems would vanish once one moved to a language that implements dependent types? (For example Idris, Agda, Coq, ...) I do not have experience with those languages which is why I am asking.

For example, on the Idris website, it is said that "types can be passed as arguments to functions" and thus, I thought, in the case of the list flattening, one could maybe simply pass the type of the list as argument and implement the desired function in a straightforward way. Is this possible?

A follow-up question would also be: Do those Families and Classes that work around this issue in haskell provide a full implementation of dependent type theory in haskell or if not, what are important differences?

CodePudding user response：

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.

CodePudding user response：

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.

CodePudding user response：

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]

CodePudding user response：

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.