==============[ Readings ]==============

On Curry-Howard Isomorphism:
https://en.wikibooks.org/wiki/Haskell/The_Curry%E2%80%93Howard_isomorphism

The correspondence between logical propositions, programs, types, and
automated proofs is fascinating, and, alongside with the
Hindley-Milner type system and the unification algorithm for type
inference is one of the major achievements in our understanding of
programming languages.

I suggest reading Phillip Wadler's "Propositions as Types" for more!
http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf

You can start with watching his talk 
https://www.youtube.com/watch?v=IOiZatlZtGU

On Haskell IO:
  (a) for a set of examples without explanations of monadic
        types involved: http://learnyouahaskell.com/input-and-output
  (b) for more in-depth explanations of how IO works:
        http://book.realworldhaskell.org/read/io.html

Suggested exercise: work through (a) figuring out the types and
desugaring as explained in (b) and in
http://www.haskellforall.com/2014/10/how-to-desugar-haskell-code.html

Pay special attention to the "do" and "<-" notation, and write the
equivalent code using >>= and >> functions and lambdas. You may get a
ton of type errors at first; persevere!

==============[ Algebraic data types ]==============

In Haskell, you are free (and expected to) construct data
types---including functional data types---from the primitive
ones. Whenever you write a function or a lambda (or even
a partial application), you, in fact, construct a data type,
which is written with -> (which :t prints you for functions).

Think of this as having an additional language in which you
write (create) formulas for types, similar to how you write
formulas in algebra. Just like in algebra, you can use 
variables to signify unknowns, or parameters.

Whenever you define a function that takes some object of type A to
type B, you have constructed a type (A -> B). This serves as assurance
that if you are given an object x of A, then B will not be an empty
type, because you will use your function on x to get an object of B.

This might remind you of logic: if you have a proposition A
that you know to be true, and you know an implication A => B
(from A follows B), then you can also obtain that B is true.
The proof of B consists of showing A and A => B ; with the 
implication A => B, you know how to make a B out of A. 

These parallels between constructing function types (i.e., writing
functions, i.e., programming) and proving logical theorems lead
to the Curry-Howard Isomorphism (see readings above for more).


You can also make new types by extending the values of existing
types---like one constructs new sets from given sets (think Venn
diagrams).

For example, with "Maybe a" you can take a type and extend it with a
special value Nothing (usually meaning "an error occurred, but I'll
deal with it later; don't terminate the program via an
exception". With 'Either', you can have a type that contains values of
two different types, which a unconfusable as to which type they came
from---this is called a "direct sum" (you can do the same for two
sets, but you need to watch out for values that occur in both,
because, say, a 0 from the first set and a 0 from the second set will
be two different elements of the direct sum of these number sets).

You can also construct a "direct product" of two types---we know
these as pairs (a,b) or tuples. 

Such are "algebraic types". Like formulas in algebra, these are endless;
you can always write a longer (and valid) formula from existing ones.

---------------[ IO as a Monad ]---------------

Maybe is a very simple monad. Haskell's IO is also a monad---a lot
more complex, of course, because it interacts with the OS. This monad
serves a very important goal (among others): to separate pure
operations from those that involve the OS state, and may end up in
failure for whatever OS reasons (e.g., your terminal went away, a file
ended, or could not be read from, or didn't exist, etc.)

Haskell IO takes getting used to. Work through examples in
"Learn You a Haskell" and "Read World Haskell" is the readings
above---and make sure to keep track of the types!

Note that the "do" notation actually hides >>= (for IO, which,
of course, has a different instance definition from Maybe) and
<- in the "do" notation hides lambdas. For example,

main = do 
    chat
    putStrLn "Bye!"

chat = do
    putStrLn "What's your name?"
    name <- getLine
    putStrLn ("Hello " ++ name ++ "!")

is actually:

main = chat >> 
       putStrLn "Bye!" 

chat = putStrLn "What's your name?" >> 
    getLine >>= \ name -> putStrLn ("Hello " ++ name ++ "!")

Note that the lambda fits the >>= type signature, because using putStrLn
on a pure string brings that string into the monad IO (). Note that
getLine is IO String; but the signature of >>= is general enough to fit
both (a is String here, b is (), m is IO)

Prelude> :t getLine
getLine :: IO String

Prelude> :t putStrLn
putStrLn :: String -> IO ()

Prelude> :t (>>=)
(>>=) :: Monad m => m a -> (a -> m b) -> m b