----------------------[ Experimenting with bottoms ]----------------------

-- Typing a "bottom" (the type for an infinitely looping recursive evaluation).
--   Remember, Haskell's let is a "LETREC".

-- It type-checks:

Prelude> :t let x = x in x
let x = x in x :: t

-- ...and would run endlessly. This gets detected:

Prelude> let x = x in x
*** Exception: <<loop>>

-- undefined is a similar type. It matches any type variable; 
--   it's defined later in Preamble, otherwise it'd be used instead of the above.

Prelude> :t undefined
undefined :: a

Prelude> :i undefined
undefined :: a  -- Defined in ‘GHC.Err’

Prelude> let f x y = x + y

Prelude> :t f
f :: Num a => a -> a -> a

-- Partial application to an (error ..) expression (of type bottom)
--   is just fine, makes a legit lambda:

Prelude> let g = f (error "Boom")

Prelude> :t  g
g :: Num a => a -> a

-- Both g and f error out when evaluated, of course.
--   But: it's important to notice they type-check! They wouldn't run without type-checking first.

Prelude> g 5
*** Exception: Boom

Prelude> f (error "Boo!") 1
*** Exception: Boo!

-- But if the argument is of the wrong type, f doesn't even typecheck!
--   And so it doesn't even get to run:

Prelude> f (error "Boo!") "foo"

<interactive>:13:1:
    No instance for (Num [Char]) arising from a use of ‘f’
    In the expression: f (error "Boo!") "foo"
    In an equation for ‘it’: it = f (error "Boo!") "foo"

-- Note that partial application to a bottom doesn't affect type signature:

Prelude> let g = f (error "Boo!") 

Prelude> :t g
g :: Num a => a -> a

-- Trying to create a partial application with a wrong type fails to typecheck:

Prelude> f "bar"

<interactive>:16:1:
    No instance for (Num [Char]) arising from a use of ‘f’
    In the expression: f "bar"
    In an equation for ‘it’: it = f "bar"

-- Trying to apply g gives the same typecheck error (and no run):

Prelude> g "bar"

<interactive>:20:1:
    No instance for (Num [Char]) arising from a use of ‘g’
    In the expression: g "bar"
    In an equation for ‘it’: it = g "bar"

Prelude> g 5
*** Exception: Boo!

-- Let's use other bottoms. Same deal, they matche any type variable:

Prelude> let g = f (let x = x in x) 

Prelude> :t g
g :: Num a => a -> a

Prelude> g 5
*** Exception: <<loop>>

Prelude> let g = f undefined 

Prelude> :t g
g :: Num a => a -> a

Prelude> g 5
*** Exception: Prelude.undefined

---- Another operation, another type constraint inferred, same behavior on bottoms:

Prelude> let f x y = x ++ y

Prelude> :t f 
f :: [a] -> [a] -> [a]

Prelude> f 1 "foo"

<interactive>:3:3:
    No instance for (Num [Char]) arising from the literal ‘1’
    In the first argument of ‘f’, namely ‘1’
    In the expression: f 1 "foo"
    In an equation for ‘it’: it = f 1 "foo"

Prelude> f (error "Boom!") "foo"
"*** Exception: Boom!

Prelude> :t f (error "Boom!") "foo"
f (error "Boom!") "foo" :: [Char]

Prelude>  f (error "Boom!") 1

<interactive>:7:2:
    No instance for (Num [a0]) arising from a use of ‘it’
    In a stmt of an interactive GHCi command: print it
Prelude> 

-- This can't be the right type. Num [a] is probably not one ever wants.
--  Notice how 1, a Num instance, plays into type inference (done
--    via unification, hence 1 adds the Num constraint to the context,
--    which was not there before!

Prelude> :t f (error "Boom!") 1
f (error "Boom!") 1 :: Num [a] => [a]

-- See also the middle of Ch 5 for more discussion of undefined.