Remix.run Logo
Remix clone Hacker News
new | show | ask | jobsGithub
▲ solomonb a day ago

Given an algebraic data type such as:

    data List a = Nil | Cons a (List a)
You can define its recursion principle by building a higher-order function that receives an element of your type and, for each constructor, receives a function that takes all the parameters of that constructor (with any recursive parameters replaced by `r`) and returns `r`.

For `List` this becomes:

   foldr :: (() -> r) -> (a -> r -> r) -> List a -> r
The eliminator for `Nil` can be simplified to `r` as `() -> r` is isomorphic to `r`:

   foldr :: r -> (a -> r -> r) -> List a -> r
   foldr z f Nil = z
   foldr z f (List a xs) = f a (foldr f z xs)
For `Bool`:

    data Bool = True | False
We get:

    bool :: a -> a -> Bool -> a
    bool p q True = q
    bool p q False = p
Which is precisely an If statement as a function!

:D