I think I understand how function application works when writing out the steps, but the type signature arithmetic doesn’t add up in my head. Apologies for the long prelude (no pun intended).
To bring a specific example, this one’s from Stefan Höck’s Idris2 tutorial:
plusTwo : Integer -> Integer
plusTwo = (+2)
twice : (Integer -> Integer) -> Integer -> Integer
twice f n = f (f n)
In the REPL(s):
> twice plusTwo 3
7
> (twice . twice) plusTwo 3
11
What I know
-
functions both in Haskell and Idris are curried and every function takes only one argument
-
function composition is implemented as
f . g = \x -> f (g x) -
function application is left associative
-
arrows in type signatures are right associative
Writing out (twice . twice) plusTwo 3
The expression can be explicitly parenthesized as
((twice . twice) plusTwo) 3
which can be re-written as
------f-------- -n-
(twice (twice plusTwo)) 3
|
V
------f-------- (------f-------- -n-)
(twice plusTwo) ((twice plusTwo) 3 )
\------------------/
|||
plusTwo (plusTwo 3)
|||
7
\-----------------------------------/
|||
twice plusTwo 7
Seeming type signature mismatch
The function composition operator’s type signature below shows that it takes one-argument functions,
(.) :: (b -> c) -> (a -> b) -> a -> c
f . g = \x -> f (g x)
but twice takes two arguments (i.e., (t -> t) -> t -> t), so this throws me off.
I guess the only way this works when the argument x of the returned lambda is itself a function. Could it be this simple?
twice . twice
((a -> a) -> a -> a) -> ((a -> a) -> a -> a) -> ?
(---b---- -> --c---) -> (---a---- -> --b---) -> (a -> c)
? = (a -> a) -> a -> a
or, to put it another way, twice . twice takes a function with the signature (a -> a) -> a (where a here is Integer).
If the above stuff is correct, then I can figure out function compositions where the participating functions have differing input arguments (e.g., twice . (+2)).
>Solution :
Yes, that’s really all it is. It may make it easier to think about if you write the signature of twice as
twice :: (Integer -> Integer) -> (Integer -> Integer)
As you know, this is equivalent thanks to currying. Seen this way, twice is a function of one argument, and composing it with twice again seems perfectly sensible.