====================[ Hindley-Milner types and type inference ]=====================

Read Chapter 6 of the textbook. Focus on Section 6.3, "Type Inference".

Depending on your learning style, you may find the following sources helpful
to understand the Hindley-Milner-Damas type inference algorithm:

https://bernsteinbear.com/blog/type-inference/ -- explanations of inference algorithms
     with Python implementations

https://slightknack.dev/passerine/type-inference/ -- Cornell lecture notes, gives
     examples of type reference in OCaml. OCaml's syntax is slightly different,
     "let g = fun x -> ((+) 5) x" would be "let g = \ x  -> ((+) 5) x" in Haskell
     and type variables are written 'a, 'b, etc. OCaml has more "fun" :) 

------------------[ Let's see type inference in Haskell, in action ]-----------------

-- Our first steps in Haskell. Our emphasis was on Haskell's types, which were
--   _always_ inferred by Haskell's version of Hindley-Milner type inference (an
--   extension of the famous Algorithm W) and the elements of Haskell's syntax
--   inspired  by lambda calculus (such as left associativity of functions by default).

-- I used GHCI on my M1 Mac. "brew install ghc" or "port install ghc" will get it for
--   you on MacOS. GHC is the compiler, GHCI is the interactive REPL.

-- GHCI's commands :t and :i will show the expression's type and show you information
--  about where a function is defined. Use these often.

user@snowball hs % ghci 
GHCi, version 9.14.1: https://www.haskell.org/ghc/  :? for help

-- "\" stands for lambda. Imagine a short front leg jutting left from the middle of "\"

ghci> let id = \ x -> x   

ghci> :t id      --  :t is a part of GHCI interactive REPL, not Haskell itself    
id :: p -> p     --   this is the type. For any type, 'id' returns the same type (and the same value) 

ghci> id 1
1

ghci> :t "foo"
"foo" :: String

ghci> id "foo"
"foo"

ghci> 1+2   -- Haskell favors infix syntax
3

-- However, every infix operator is a function that has a Lisp-y prefix form in ()s and you
--   can look up their types and syntax info for that form.

ghci> (+) 1 2
3

ghci> :t (+)
(+) :: Num a => a -> a -> a

ghci> :i (+)
type Num :: * -> Constraint
class Num a where
  (+) :: a -> a -> a
  ...
  	-- Defined in ‘GHC.Internal.Num’
infixl 6 +        -- infix, associating to the left, with the precedence of 6 (not too high,
                  --   function application is higher)

-- Association to the left means that we can write  1+2+3+4  without explicit parentheses,
--  and we will be getting exactly (((1+2)+3)+4) when we do so. 


-- +1 and 1+ are both functions, same as \x -> x+1  and \x -> 1+x . What can be more natural? :) 

ghci> :t (+) 1
(+) 1 :: Num a => a -> a     -- partial application of a -> a -> a produces a -> a 

ghci> :t (+ 1)
(+ 1) :: Num c => c -> c

ghci> :t (1 +)
(1 +) :: Num a => a -> a

ghci> (1+) 2
3

ghci> (+1) 2
3

ghci> :i (>)
type Ord :: * -> Constraint
class Eq a => Ord a where
  ...
  (>) :: a -> a -> Bool
  ...
  	-- Defined in ‘GHC.Internal.Classes’
infix 4 >       -- NOTE that this is infix but _not_ associative

ghci> 4 > 5
False

ghci> :t (4 > 5)
(4 > 5) :: Bool

-- Not set up for associativity, for two reasons: none defined AND 4>5 is Bool, not a number
--   that can be compared with another number.

ghci> 4 > 5 > 3
<interactive>:12:1: error: [GHC-88747]
    Precedence parsing error
        cannot mix ‘>’ [infix 4] and ‘>’ [infix 4] in the same infix expression

-- this is a parsing error, parens are needed

ghci> :t 1+
<interactive>:1:3: error: [GHC-58481]
    parse error (possibly incorrect indentation or mismatched brackets)


ghci> :t 1 +
<interactive>:1:4: error: [GHC-58481]
    parse error (possibly incorrect indentation or mismatched brackets)


ghci> :t \ x -> 1 + x 
\ x -> 1 + x :: Num a => a -> a

ghci> :t (>2) 
(>2) :: (Num b, Ord b) => b -> Bool

ghci> (>2) 5
True

ghci> (>2) 1
False

-- A parsing error, no associativity defined.

ghci> 2>3>5
<interactive>:22:1: error: [GHC-88747]
    Precedence parsing error
        cannot mix ‘>’ [infix 4] and ‘>’ [infix 4] in the same infix expression

-- Even if we put parens in, we'll get a type error. Remember, (2>3) is False.

ghci> (2>3) > 5
<interactive>:24:9: error: [GHC-39999]
    • No instance for ‘Num Bool’ arising from the literal ‘5’
    • In the second argument of ‘(>)’, namely ‘5’
      In the expression: (2 > 3) > 5
      In an equation for ‘it’: it = (2 > 3) > 5

-- Lists are built and processed recursively and are defined inductively.
--  There is an empty list constructor [] (think of it as NIL) and a constructor
--   that builds something like a CONS cell. ':' is its infix form:

ghci> :i (:)
type List :: * -> *
data List a = [] | a : [a]
  	-- Defined in ‘GHC.Internal.Types’
infixr 5 :

-- Note that : associates to the right:  1 : 2 : 3 : []  is   1 : (2 : (3 : []))

ghci> 1 : 2 : 3 : [] 
[1,2,3]

-- Remember, [1,2,3] is just a nice syntax for the actual  1:(2:(3:[]))  . There is
--  no way to construct a list or operate on a list than with [] and : !

-- An aside: Haskell allows endless lists like [1..]. This is possible due to lazy evaluation,
--   which we'll discuss later. Unlike Lisp and Scheme, Haskell's evaluation will hold off
--   on evaluating a function's arguments for as long as possible, and will do as little of
--   it as possible. This is a common Haskell idiom if you need a sequence of integers
--    (and Haskell tutorials love to show it off).

ghci> take 10 [1..]
[1,2,3,4,5,6,7,8,9,10]

-- See the types of the partial evaluations of take:

ghci> :t take
take :: Int -> [a] -> [a]

ghci> :t take 10 
take 10 :: [a] -> [a]

ghci> :i (..)
<interactive>:1:2: error: [GHC-58481]
    parse error on input ‘..’

-- (:) is a CONS:

ghci> :t (:)
(:) :: a -> [a] -> [a]

ghci> (:) 1 []
[1]

ghci> :t 1 : 
<interactive>:1:4: error: [GHC-58481]
    parse error (possibly incorrect indentation or mismatched brackets)


ghci> :t (1 : )
(1 : ) :: Num a => [a] -> [a]

-- Figure out why this doesn't type-check:

ghci> (1 : ) 2 
<interactive>:36:1: error: [GHC-39999]
    • No instance for ‘Num [Integer]’ arising from a use of ‘it’
    • In the first argument of ‘print’, namely ‘it’
      In a stmt of an interactive GHCi command: print it

-- Let's see and write some recursive list functions: 

ghci> let sq = \ x -> x*x

ghci> :t sq
sq :: Num a => a -> a

ghci> map
map      mapM     mapM_    mappend

ghci> :t map sq 
map sq :: Num b => [b] -> [b]

ghci> let ll = 1 : 2 : 3 : []

ghci> ll
[1,2,3]

ghci> map sq ll
[1,4,9]

-- Note the type of MAP: its first argument is a function that takes something of type A
--  to something of a type B, its second is a list of As, its result is a list of Bs.

ghci> :t map 
map :: (a -> b) -> [a] -> [b]

-- Let's write our own length matching the list type definition 

ghci> :{
ghci| mlen [] = 0
ghci| :}

-- Incomplete but already gives us an inferred type for mlen:

ghci> :t mlen 
mlen :: Num a1 => [a2] -> a1

ghci> mlen []
0

-- Its incompleteness is caught as seen as the (:) constructor is unmatched:

ghci> mlen [1]
*** Exception: <interactive>:45:1-11: Non-exhaustive patterns in function mlen


HasCallStack backtrace:
  collectExceptionAnnotation, called at libraries/ghc-internal/src/GHC/Internal/Exception.hs:170:37 in ghc-internal:GHC.Internal.Exception
  toExceptionWithBacktrace, called at libraries/ghc-internal/src/GHC/Internal/Exception.hs:90:42 in ghc-internal:GHC.Internal.Exception
  throw, called at libraries/ghc-internal/src/GHC/Internal/Control/Exception/Base.hs:434:30 in ghc-internal:GHC.Internal.Control.Exception.Base

-- To get to the case of the CONS cell, we must match the constructor (:)  

ghci> mlen x:xs = 1 + mlen xs
<interactive>:50:1: error: [GHC-07626]
    Parse error in pattern: mlen

-- Because functions associate to the left,  mlen x:xs  actually means (mlen x):xs, not what we meant.

ghci> mlen (x:xs) = 1 + mlen xs

-- This syntax-checks, but we need to re-add the base case of  []

ghci> mlen [1]
*** Exception: <interactive>:51:1-25: Non-exhaustive patterns in function mlen


HasCallStack backtrace:
  collectExceptionAnnotation, called at libraries/ghc-internal/src/GHC/Internal/Exception.hs:170:37 in ghc-internal:GHC.Internal.Exception
  toExceptionWithBacktrace, called at libraries/ghc-internal/src/GHC/Internal/Exception.hs:90:42 in ghc-internal:GHC.Internal.Exception
  throw, called at libraries/ghc-internal/src/GHC/Internal/Control/Exception/Base.hs:434:30 in ghc-internal:GHC.Internal.Control.Exception.Base

-- So this works. Note that it has the same shape as a Lisp or Scheme function, and this
--  shape is similarly driven by _the only way we are allowed to construct a list_, i.e., with
--  constructors for the empty list and for a single step of the list's construction, a single cell.
--  Once you match these two, your recursive function is ready!

ghci> :{
ghci| mlen [] = 0
ghci| mlen (x:xs) = 1 + mlen xs
ghci| :}

ghci> mlen [1]
1

ghci> mlen [1,2]
2

ghci> mlen (take 10 [1..])
10

ghci> mlen (take 1000 [1..])
1000

-- Note the type. It's fully inferred from the function's code. The type inference
--  algorithm notes that the returned type participates in an addition, and that the
--  argument is pattern-matched as a list, hence the type is   Num t => [a] -> t
--  Nothing can be inferred about the type of the list's elements, so we just keep an 'a'.

ghci> :t mlen
mlen :: Num t => [a] -> t

-- Now let's do out own MAP:

ghci> :t mmap
<interactive>:1:1: error: [GHC-88464]
    Variable not in scope: mmap
    Suggested fix:
      Perhaps use one of these:
        ‘map’ (imported from Prelude), ‘fmap’ (imported from Prelude)


ghci> :{
ghci| mmap f [] = []
ghci| mmap f (x:xs) = (f x) : mmap f xs 
ghci| :}

ghci> mmap sq []
[]

ghci> mmap sq [1,2,3,4]
[1,4,9,16]

ghci> mmap sq (take 10 [10..])
[100,121,144,169,196,225,256,289,324,361]

-- Now is the type of our MMAP inferred? How is it inferred that the first argument we called 'f' 
--   is a function? It was inferred from the application (f x) !

ghci> :t mmap
mmap :: (t -> a) -> [t] -> [a]

-- Suppose we make a partial application 'mmap sq'. Its type is inferred as '[a] -> [a]',
--  taking a list of some numeric 'a' to another list of the same 'a'. The Num a constraint
--  comes from looking into SQ and seeing its argument participate in a multiplication.

ghci> :t mmap sq
mmap sq :: Num a => [a] -> [a]

-- A syntactic aside: in fact, we don't need parens around f x . Application has the highest
--   precedence, and : is merely at precedence 5, lower that + and other arithmetic, which are at 6. 

ghci> :{ 
ghci| mmap f [] = []
ghci| mmap f (x:xs) = f x : mmap f xs 
ghci| :}

ghci> mmap sq (take 10 [10..])
[100,121,144,169,196,225,256,289,324,361]

-- There is a standard library's MAP:

ghci> :t map
map :: (a -> b) -> [a] -> [b]

ghci> :i map
map :: (a -> b) -> [a] -> [b] 	-- Defined in ‘GHC.Internal.Base’

ghci> :i mmap
mmap :: (t -> a) -> [t] -> [a] 	-- Defined at <interactive>:73:1

ghci> :t mmap
mmap :: (t -> a) -> [t] -> [a]

-- We can do the folds now, guided by their type.  

ghci> :t foldl  
foldl :: Foldable t => (b -> a -> b) -> b -> t a -> b

ghci> foldl (\ x y -> 1+x ) 0 [] 
0

ghci> foldl (\ x y -> 1+x ) 0 [1,2,3] 
3

-- Notice that we didn't need to do anything in our lambda for the case of the empty list [],
--   because the FOLDL function itself returns the initial value for it, 0 in this case.

ghci> :t ( foldl (\ x y -> 1+x ) 0  )
( foldl (\ x y -> 1+x ) 0  ) :: (Foldable t, Num b) => t a -> b

-- So we can define a fold-based length. Note that we should actually be using FOLDL',
--  the non-lazy variant of FOLDL in any real scenario. It's part of a subtle
--  and beautiful design explained here:  https://blog.haskell.org/foldl-and-foldr/

ghci> let flen = foldl (\ x y -> 1+x ) 0  

ghci> flen []
0

ghci> flen (take 10 [1..])
10

--- Note that functions associate to the _left_, just like in Lambda calculus.
--    So  f f x  is ((f f) x)  and you _need_ explicit parens if you mean f (f x)

-- Let's see a somewhat mind-bending exercise on this:

ghci> let dup = \ f x -> f ( f x ) 

ghci> :t dup
dup :: (t -> t) -> t -> t

ghci> :t dup sq 
dup sq :: Num t => t -> t

ghci> :t dup dup sq 
dup dup sq :: Num t => t -> t

ghci> :t dup dup sq 2
dup dup sq 2 :: Num t => t

ghci>  dup dup sq 2
65536

ghci> dup sq 2
16

ghci> (sq (sq 2))
16

ghci> sq sq 2                           -- predictably, a type error:
<interactive>:96:1: error: [GHC-39999]
    • No instance for ‘Num (Integer -> Integer)’
        arising from a use of ‘it’
      (maybe you haven't applied a function to enough arguments?)
    • In the first argument of ‘print’, namely ‘it’
      In a stmt of an interactive GHCi command: print it


ghci> dup sq 2              
16                        -- apply square twice, get a 4th power: 2^4 = 16

ghci> dup dup sq 2        -- remember, this is (dup dup) applied to sq. 
65536

-- Figuring out (dup dup) is pure lambda calculus! Do it.

ghci>