Haskell / Miranda: Find the type of the function

functional-programming, haskell, miranda, type-inference, types

Solution

You've already got the answer, I'll just write down the derivation step by step so it's easy to see all at once:

xxf xs = foldr (+) 0 . foldr ((:) . length . flip (:) []) [] $ xs
       = sum         $ foldr ((:) . length . (: []))      []   xs
       = sum         $ foldr (\x -> (:) (length [x]))     []   xs
       = sum         $ foldr (\x r ->    length [x]:r)    []   xs
       = sum         $ map   (\x   ->    length [x]  )         xs
       = sum                            [length [x]  |    x <- xs]  
       = sum                            [ 1          |    x <- xs]
--     = length xs
xxf :: (Num n) => [a] -> n

So that, in Miranda, `xxf xs = #xs`. I guess its type is `:: [*] -> num` in Miranda syntax.

Haskell's `length` is `:: [a] -> Int`, but as defined here, it is `:: (Num n) => [a] -> n` because it uses `Num`'s `(+)` and two literals, `0` and `1`.

If you're having trouble visualizing `foldr`, it is simply

foldr (+) 0 (a:(b:(c:(d:(e:(...:(z:[])...))))))
      =      a+(b+(c+(d+(e+(...+(z+ 0)...)))))
      = sum [a, b, c, d, e, ..., z]

Problem

Brief: This is a past exam question from a Miranda exam but the syntax is very similar to Haskell. Question: What is the type of the following expression and what does it do? (The definitions of the functions length and swap are given below). ``` (foldr (+) 0) . (foldr ((:) . length . (swap (:) [] )) []) length [] = 0 length (x:xs) = 1 + length xs swap f x y = f y x ``` Note: Please feel free to reply in haskell syntax - sorry about putting using the stars as polytypes but i didn't want to translate it incorrectly into haskell. Basically, if one variable has type * and the other has * it means they can be any type but they must both be the same type. If one has ** then it means that it can but does not need to have the same type as *. I think it corresponds to a,b,c etc in haskell usuage. My working so far From the definition of length you can see that it finds the length of a list of anything so this gives ``` length :: [*] -> num. ``` From the definition I think swap takes in a function and two parameters and produces the function with the two parameters swapped over, so this gives ``` swap :: (* -> ** -> ***) -> ** -> [*] -> *** ``` foldr takes a binary function (like plus) a starting value and list and folds the list from right to left using that function. This gives ``` foldr :: (* -> ** -> **) -> ** -> [*] -> **) ``` I know in function composition it is right associative so for example everything to the right of the first dot (.) needs to produce a list because it will be given as an argument to the first foldr. The foldr function outputs a single value ( the result of folding up the list) so I know that the return type is going to be some sort of polytype and not a list of polytype. My problem I'm unsure where to go from here really. I can see that swap needs to take in another argument, so does this partial application imply that the whole thing is a function? I'm quite confused!

Original source