How to “iterate” over a function whose type change

Question

I have just started learning Haskell and I come across the following problem. I try to "iterate" the function \x->[x]. I expect to get the result [[8]] by

foldr1 (.) (replicate 2 (\x->[x])) $ (8 :: Int)

This does not work, and gives the following error message:

Occurs check: cannot construct the infinite type: a ~ [a]

Expected type: [a -> a]

Actual type: [a -> [a]]

I can understand why it doesn't work. It is because that foldr1 has type signature foldr1 :: Foldable t => (a -> a -> a) -> a -> t a -> a, and takes a -> a -> a as the type signature of its first parameter, not a -> a -> b

Neither does this, for the same reason:

((!! 2) $ iterate (\x->[x]) .) id) (8 :: Int)

However, this works:

(\x->[x]) $ (\x->[x]) $ (8 :: Int)

and I understand that the first (\x->[x]) and the second one are of different type (namely [Int]->[[Int]] and Int->[Int]), although formally they look the same.

Now say that I need to change the 2 to a large number, say 100.

My question is, is there a way to construct such a list? Do I have to resort to meta-programming techniques such as Template Haskell? If I have to resort to meta-programming, how can I do it?

As a side node, I have also tried to construct the string representation of such a list and read it. Although the string is much easier to construct, I don't know how to read such a string. For example,

read "[[[[[8]]]]]" :: ??

I don't know how to construct the ?? part when the number of nested layers is not known a priori. The only way I can think of is resorting to meta-programming.

The question above may not seem interesting enough, and I have a "real-life" case. Consider the following function:

natSucc x = [Left x,Right [x]]

This is the succ function used in the formal definition of natural numbers. Again, I cannot simply foldr1-replicate or !!-iterate it.

Any help will be appreciated. Suggestions on code styles are also welcome.

Edit: After viewing the 3 answers given so far (again, thank you all very much for your time and efforts) I realized this is a more general problem that is not limited to lists. A similar type of problem can be composed for each valid type of functor (what if I want to get Just Just Just 8, although that may not make much sense on its own?).

Answer 1

I'd like to propose a very simple alternative which doesn't require any extensions or trickery: don't use different types.

Here is a type which can hold lists with any number of nestings, provided you say how many up front:

data NestList a = Zero a | Succ (NestList [a]) deriving Show
instance Functor NestList where
    fmap f (Zero a) = Zero (f a)
    fmap f (Succ as) = Succ (fmap (map f) as)

A value of this type is a church numeral indicating how many layers of nesting there are, followed by a value with that many layers of nesting; for example,

Succ (Succ (Zero [['a']])) :: NestList Char

It's now easy-cheesy to write your \x -> [x] iteration; since we want one more layer of nesting, we add one Succ.

> iterate (\x -> Succ (fmap (:[]) x)) (Zero 8) !! 5
Succ (Succ (Succ (Succ (Succ (Zero [[[[[8]]]]])))))

Your proposal for how to implement natural numbers can be modified similarly to use a simple recursive type. But the standard way is even cleaner: just take the above NestList and drop all the arguments.

data Nat = Zero | Succ Nat

Answer 2

You'll certainly agree that 2 :: Int and 4 :: Int have the same type. Because Haskell is not dependently typed^†, that means foldr1 (.) (replicate 2 (\x->[x])) (8 :: Int) and foldr1 (.) (replicate 4 (\x->[x])) (8 :: Int) must have the same type, in contradiction with your idea that the former should give [[8]] :: [[Int]] and the latter [[[[8]]]] :: [[[[Int]]]]. In particular, it should be possible to put both of these expressions in a single list (Haskell lists need to have the same type for all their elements). But this just doesn't work.

The point is that you don't really want a Haskell list type: you want to be able to have different-depth branches in a single structure. Well, you can have that, and it doesn't require any clever type system hacks – we just need to be clear that this is not a list, but a tree. Something like this:

data Tree a = Leaf a | Rose [Tree a]

Then you can do

Prelude> foldr1 (.) (replicate 2 (\x->Rose [x])) $ Leaf (8 :: Int)
Rose [Rose [Leaf 8]]
Prelude> foldr1 (.) (replicate 4 (\x->Rose [x])) $ Leaf (8 :: Int)
Rose [Rose [Rose [Rose [Leaf 8]]]]

---

^†_{Actually, modern GHC Haskell has quite a bunch of dependently-typed features (see DaniDiaz' answer), but these are still quite clearly separated from the value-level language.}

Answer 3

This problem indeed requires somewhat advanced type-level programming.

I followed @chi's suggestion in the comments, and searched for a library that provided inductive type-level naturals with their corresponding singletons. I found the fin library, which is used in the answer.

The usual extensions for type-level trickery:

{-# language DataKinds, PolyKinds, KindSignatures, ScopedTypeVariables, TypeFamilies #-}

Here's a type family that maps a type-level natural and an element type to the type of the corresponding nested list:

import Data.Type.Nat

type family Nested (n::Nat) a where
    Nested Z a = [a]
    Nested (S n) a = [Nested n a]

For example, we can test from ghci that

*Main> :kind! Nested Nat3 Int
Nested Nat3 Int :: *
= [[[[Int]]]]

(Nat3 is a convenient alias defined in Data.Type.Nat.)

And here's a newtype that wraps the function we want to construct. It uses the type family to express the level of nesting

newtype Iterate (n::Nat) a = Iterate { runIterate :: (a -> [a]) -> a -> Nested n a }

The fin library provides a really nifty induction1 function that lets us compute a result by induction on Nat. We can use it to compute the Iterate that corresponds to every Nat. The Nat is passed implicitly, as a constraint:

iterate' :: forall n a. SNatI n => Iterate (n::Nat) a
iterate' =
    let step :: forall m. SNatI m => Iterate m a -> Iterate (S m) a
        step (Iterate recN) = Iterate (\f a -> [recN f a])
    in  induction1 (Iterate id) step

Testing the function in ghci (using -XTypeApplications to supply the Nat):

*Main> runIterate (iterate' @Nat3) pure True
[[[[True]]]]