This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
In https://github.com/ekmett/lens/wiki/Derivation, we see some types for | |
composition of compositions: (.).(.), (.).(.).(.), and so on. Let's prove that | |
the type of (.).(.) is (a -> b) -> (c -> d -> a) -> c -> d -> b, as stated in | |
the site. We'll stick with prefix notation, meaning that we want the type of | |
(.)(.)(.). | |
Recall the type of composition. This should be intuitive: | |
(.) :: (b -> c) -> (a -> b) -> a -> c [1] |
It’s folklore that if you’re summing a list of numbers, then you should always use strict foldl
. Is that really true though? foldr
is useful for lists when the function we use is lazy in its second argument. For (+) :: Int -> Int -> Int
this is tyically not the case, but in some sense that’s because Int
is “too strict”. An alternative representation of numbers is to represent them inductively. If we do this, sumation can be lazy, and foldr
can do things that foldl
simply can’t!
First, let’s define natural numbers inductively, and say how to add them:
data Nat = Zero | OnePlus Nat deriving Show
one :: Nat