Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

How to "iterate" over a function whose type changes among iteration but the formal definition is the same

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?).

like image 554
Weijun Zhou Avatar asked Dec 08 '22 16:12

Weijun Zhou


2 Answers

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.

like image 169
leftaroundabout Avatar answered Jan 13 '23 00:01

leftaroundabout


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
like image 37
Daniel Wagner Avatar answered Jan 12 '23 23:01

Daniel Wagner