Search code examples
haskelltypesghciunification

Deriving type of foldr (!!)

foldr :: (a->b->b)->b->[a]->b
(!!)::[c]->Int->c

From that we get a->b->b=[c]->Int->c or a=[c],b=Int,b=c.
We conclude that type of foldr (!!) is Int->[[Int]]->Int.
Is it correct?
WinGHCi tells me something different:

Prelude> :t foldr (!!)
foldr (!!) :: Foldable t => Int -> t [Int] -> Int
Solution

  • The foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b indeed in the early days had the signature (a -> b -> b) -> b -> [a] -> b, but they have generalized the function, such that it not only works with lists (where t ~ []), but with other Foldable types (like Maybe, Sum, etc. as well). But for the list case, nothing changes, the function is simply applicable to more Foldable types.

    Deriving the type for the "old" foldr

    In that case we take as ingredients:

    foldr :: (a -> b -> b) -> b -> [a] -> b
(!!) :: [c] -> Int -> c

    or more verbose:

    foldr :: (a -> (b -> b)) -> (b -> ([a] -> b))
(!!) :: [c] -> (Int -> c)

    Since (!!) is the parameter of the call with foldr as function, we know that the type of the (!!) :: [c] -> (Int -> c) function should match with the type of the parameter of foldr, so (a -> b -> b). So that means:

      a -> (b -> b)
~ [c] -> (Int -> c)
--------------------
a ~ [c], b ~ c ~ Int

    So we know that a is the same type as [c], and that both b and c are actually Int. Therefore we know that a ~ [Int].

    So now the type of foldr (!!) is the output type of foldr, but specialized with what we derived, so:

    b -> ([a] -> b)

    which is equal to:

    Int -> ([[Int]] -> Int)

    or less verbose:

    Int -> [[Int]] -> Int

    Deriving the type of the "new" folr

    In that case we take as ingredients:

    foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b
(!!) :: [c] -> Int -> c

    and we follow the same reasoning for the first parameter of foldr:

      a -> (b -> b)
~ [c] -> (Int -> c)
--------------------
a ~ [c], b ~ c ~ Int

    So the output type of foldr is:

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

    or specified with what we know:

    Foldable t => Int -> t [Int] -> Int

    Which is what ghci derived.

    The semantics of the function

    As for the semantics, the function:

    f = foldr (!!)

    takes as input an Int (an index), and a Foldable of lists of Ints. In case of a list, it will - right-to-left - obtain the element with that index, of the most right list, and use that element as an index for the one last but one list. We keep doing that until the first list, and return the element.

    For example:

    foldr (!!) 1 [] -> 1
foldr (!!) 1 [[2, 0]] -> 0
foldr (!!) 1 [[3, 5], [2, 0]] -> 3

    For the t ~ Maybe case, we will thus return the original index in case of a Nothing, or we will return the element at that index in case it is a Just [1, 4, 2, 5] (a Just that carries a [Int] object). For example:

    foldr (!!) 1 Nothing -> 1
foldr (!!) 3 Nothing -> 3
foldr (!!) 1 (Just [1, 4, 2, 5])-> 4
foldr (!!) 3 (Just [1, 4, 2, 5])-> 5