Seriously, Haskell can be annoying. It makes you think in twists and turns. What I wanted was a control flow around some input, but Haskell does not do loops, and call depth might be an issue when asking for input recursively. So what we need is an elegant way to fail when the input is incorrect.

We're working with a command-line application, so we just need to input and output string values. Our core execution type is naively (in lambda calculus, not strict Haskell):

solve : String -> String

So what we can do is on bad input also return a string, but then one with the explanation in it.

To write the checks in an elegant way, we need to think about the types more deeply. A check usually results in a Bool. We do not know what we are checking so we might need a generic function to Bool. Let's take:

when : (a -> Bool)

We will also need a message to display when the check fails, we need to input that as well.

when : (a -> Bool) -> String

The function I called when, because when everything checks out, it should run a function. Which function that is? The actual run function:

run : String -> String

But we can keep it generic because what we check is the input. So if we use a again, we can use the input that we checked. So our when execution function is:

when : (a -> Bool) -> String -> (a -> a)

We will also need to denote the input that we are checking and passing through. That is of course also of type a. And for convenience our output will also be of type a.

when : (a -> Bool) -> String -> (a -> a) -> a -> a

Notice in the screenshot I changed the String to an a. Technically that is correct, since whatever output our function to run (a -> a) has (which is a), should also be the alternative output in error.

Using this when function we can get an idea of how Haskell (or rather, Lambda calculus) can use function reduction as a strength

Given

d : String -> Bool
d' : String
run : String -> String

when : (a -> Bool) -> a -> (a -> a) -> a -> a
when d : String -> (String -> String) -> String -> String
when d d' : (String -> String) -> String -> String
when d d' run : String -> String

Note that as soon as we provide a reduction that makes supertype a explicit, the remainder of the function has a realized as type String. Also notice that our final reduction does not yield an answer of type String, but a function of type (String -> String)

And so we come to our wonderful reduction:

l : String -> Bool
l' : String

when : (a -> Bool) -> a -> (a -> a) -> a -> a
when l : String -> (String -> String) -> String -> String
when l l' : (String -> String) -> String -> String
when l l' (when d d' run) : String -> String

which is equivalent to:
when l l' $ when d d' run : String -> String

The $ simply enforces right-hand first execution without using parenthesis.

This chain can be built as long as you want, you can even construct a massive check chain from a list of type [((String -> Bool), String)]. Not that it is needed, but Haskell makes me feel like I want to show off :P

Note also the function composition going on to create l and d.
(==) : a -> a -> Bool
4 : Int
(==) 4 : Int -> Bool
length : Foldable t => t a -> Int

(==) 4 . length : Foldable t => t a -> Bool

The difference with $ being that $ enforces righthand execution, while . composes two functions without needing the execution to take place at that moment.

Note that String is the same as [Char] and that any [a] is foldable. That is why that function is allowed in context.

For d there is a similar reduction but I am getting tired typing it out. As you can see I also have not mastered a very consistent code style, some things look slightly different than others. But all in all, I am proud of this part of the code!