{-

This is a comment in Haskell.

1. Side-effects.

    Examples are:

    In C we can write

    x = y + 1;

    We evaluate the right-hand.
    The value obtained overwrites the current value stored in x.

    In C we can write

    x = x + 1;

    This is "odd" because we can overwrite an existing value.
    In languages like C, we can do in-place update.

-}


main = putStrLn "Hello World"

main2 = do putStr "Hello "
           putStrLn "World"


main3 = do { putStr "Hello " ;

      putStrLn "World" }

main4 = do putStr "Hello "
           if True
            then putStrLn "World"
            else do putStr "wor"
                    putStrLn "ld"

-- Haskell is statically typed.
-- The types of variables/functions can be left implicit.

{-

From the context, we can infer that variable 'name' is of type String.

"    name <- getLine"

In Haskell we use "<-" for variable assignment.

The equal symbol "=" can only be used for function definitions.

-}

main5 = do
    print "What is your name?"
    name <- getLine
    print ("Hello " ++ name ++ "!")


{-

We pattern match over the input.
 Either

    the empty list or

    the non-empty list where
     (p:xs) is a pattern where p refers to the head element and xs to the rest.

-}

quicksort [] = []
quicksort (p:xs) = (quicksort lesser) ++ [p] ++ (quicksort greater)
    where
        lesser = filter (< p) xs
        greater = filter (>= p) xs

{-

let's infer the type of quicksort

quicksort :: (t -> t -> Bool) -> [t] -> [t]

"->" stands for the function arrow, like in math.

-}

gt x y = x > y

quicksort gtThan [] = []
quicksort gtThan (p:xs) = (quicksort gtThan lesser) ++ [p] ++ (quicksort gtThan greater)
    where
        ltEqThan = \x -> \y -> not (gtThan x y)
        lesser = filter (gtThan p) xs
        greater = filter (ltEqThan p) xs

{-

Equational style of writing programs.

Program consists of a sequence of function definitions.

Functions can take parameters, the function body starts after the "=".

Our quicksort function takes two parameters.

The first parameter is a function.

The second parameter is a list.
We know that cause we seem to be using list notation.

## Let's talk about lists

[] stands for the empty list.

[p] stands for the list with a single element p.

All the elements in a list must be of the same kind.
Haskell is a statically typed language (but types can be implicit).
That means, all elements in a list must be of the same type.

Side note.
Haskell suppports type inference. Before "compilation" the type checker
goes through the Haskell program and infers/checks all the types.

Let's get back to lists.

In ghci, we can query the type of (list) expressions.
For example,

*Main> :type [True, False]

yields

[True, False] :: [Bool]

^^^^^^^^^^^^     ^^^^^^
Value            Type

The above says:

The list [True, False] is of type [Bool].

Point to note.
[...]  is used to form a list of values.

[...] is used to describe a list type.

Another example.

[[True, False], [True], []] :: [[Bool]]

[[Bool]] stands for a list of a list of Boolean values.

Yet another example.

[[1,2],[True,False]] does not work. Why?

We infer the following.

(1) [True, False] :: [Bool]

(2) [1,2] :: Num a => [a]

This looks amazing!!!!!!

In Haskell, we can overload numbers!

What's the type of constant 1?

1 is of type Int.
But also, 1 is of type Float.

What's the type of 1?

Haskell's solution is overloading.

Consider

1 :: Num p => p

The above says: 1 is a number.

  Num p     =>     p
  ^^^^^^         ^^^^
               stands for any type parameter p

where p is constrained by "Num p".
The symbol "=>" we can read as logical implication.
Implies that p is a number.

Let's consider again.

(2) [1,2] :: Num a => [a]

1 is of type Num p => p

2 is of type Num p => p

This implies that

[1,2] is of type Num p => [p]

Side note.
Renaming of type parameters.
Consider "Num p => [p]".
There is an implicit "forall".
This means we could replace
the name "p" by let's say "a".
We must replace all occurences of "p" by "a".

Recall.
[[1,2],[True,False]] does not work. Why?

Now we know that

(1) [True, False] :: [Bool]

(2) [1,2] :: Num a => [a]

All the elements in a list must be of the
same type.

This implies that "[Bool]" and "[a]" are the same!
This implies that "Bool" and "a" are the same.
This implies that we must satisfy "Num Bool".


Let's consider the empty list, written [].
What's its type?

[]    ::      [a]
^^^^^        ^^^^^
Value        Type

The type "[a]" stands for a list where the elements are of all type "a"
where "a" is not constrained in any way.

In Haskell, we say, the empty list has a "parametric type".

Consider

[[],[True,False]]

In the above context, we use the empty list "[]" in a context of type [Bool]!

### List operations.

See lecture notes.

head [1,2] yields 1, the first element.

tail [1,2,3,4] yields [2,3,4], that means, we simply drop the first element.

head and tail are "partial functions".
Not defined for all shapes of input.


-}

{-

Homework:

(1)
Consider the intermediates steps of evaluating

append [1,2] [3,4]

(2)
sum xs =
  if null xs then 0
  else head xs + sum (tail xs)

Implement the above using pattern matching,
instead of null, head and tail.

-}


-- let's start with lists
-- In Haskell we can define functions via pattern matching.
-- Our example: Pattern matching involving list values.

-- Values:
-- []          Empty list
-- 1,2,3, ...  Integer values
-- True, False Boolean values
-- [1,2,3]     A list consisting of integers.

-- Patterns:
-- The idea: Via a pattern we can describe several values.
-- The pattern dictates the shape of certain values.

-- Note: head is pre-defined, so I'm simply using myHead.
-- Types serve documentation:
-- The input is a list whose elements are of type "a".
-- We return a value in that list (it seems cause, the return value is also of type "a").
myHead :: [a] -> a
myHead (x:xs) = x

-- In the above,
--
--   (x:xs)  is a pattern, and it describes a non-empty list
-- where x refers to the head and xs refers to the tail.
--
-- Variables x and xs are pattern variables.
--
-- Why not write something like [x,...] to refer to a non-empty list
-- where x refers to the head?
-- Because we only require the ":" operator!!!

-- In Haskell, whenever we write a list,
-- say
-- [1,2,3]
-- the above is a short-hand for
-- 1 : (2 : (3 : []))

-- The operator ":" is a pre-defined constructor to build lists.
-- The first operand is an element and
-- the second operand is a list.

-- So, in Haskell,
-- [1,2] is syntactic sugar for
-- 1 : (2 : [])

-- We can drop "(...)" because the operator/constructor ":"
-- is right-associativ!

-- Now, the constructor ":" is pronounced "cons" in Haskell.

-- Here comes the important feature.
-- We can use ":" to describe the various shapes of input.

-- Let's revisit some value.
-- (1) [1,2,3]       is syntactic sugar for    1 : (2 : (3 : []))
-- (2) [True, False] is syntactic sugar for    True : (False : [])

-- What is the common shape of the above values?
-- We're trying to generalize specific sets of values
-- and describe them via a pattern.

-- In Haskell, we have list patterns.
--
-- For example,
--
--  (x:xs)
--
-- is such a list pattern.
-- Patterns must be well-typed.
-- Hence, pattern variable x refers to an element and
-- pattern variable xs refers to a list.

-- Let's match the pattern x:xs against the above concrete values.
-- (1) What's the result when we match x:xs against 1 : (2 : (3 : []))?
-- (2) What's the result when we match x:xs against True : (False : [])?
-- The results are:
-- (1) x = 1 (means variable x is bound to the value 1)
--     xs = [2,3]
-- (2) x = True
--     xs = [False]
--
-- Let's do another example.
--  We match (y:z) against [True] : [].
-- Result: y = [True] and z = []
--
-- Recall: [True] is a short-hand for True : []
--         [[True]] is a short-hand for [True] : []


{-

Given

myHead (x:xs) = x

the expression

myHead [[True]]

evaluates to [True].

Why?

We match the function calls the sequence of available function definitions.
In our case, this boils down to matching the pattern x:xs against [[True]].
This yields x = [True] and xs = [].
The function definition tells us that the function body is simply "x".
Hence, we yields the value [True].

-}

-- In Haskell, we can have "don't care patterns",
-- in case we don't care about certain parts of the pattern.
-- "_" effectively stands for an annonymous pattern variable.

myHead2 :: [a] -> a
myHead2 (x:_) = x

myTail :: [a] -> [a]
myTail (_:xs) = xs

{-

myTail [[True]] evaluates to []

because matching (_:xs) against [[True]] which is a short-hand for [True] : []
yields the pattern binding xs = []

-}


-- Let's play around
-- We can compose patterns!

-- Input values must be non-empty lists and consist of at least two elements!
-- Consider (x:(y:xs))
-- implies that x refers to the first element, y refers to the second element and xs to the rest.
someRandomFunction :: Num a => [a] -> a
someRandomFunction (x:y:xs) = x + y

{-

someRandomFunction [1] yields an exception
because it's a partial function.

-}

-- Some idea:
-- A pattern that only applies if the first two elements are equal.
-- Something like (x:x:xs).
-- This is NOT allowed in Haskell
{-
somethingFunny (x:x:xs) = xs
-}

{-
Why?
Pattern matching becomes more complicated.
We not only need to match against values but also need to compare values.

The Haskell condition imposed on variables in patterns
demand that all pattern variables are distinct.
Somethis is also explained as saying that patterns must be "linear".
In the end, no duplicate pattern variables are allowed.

-}

somethingFunny (x:y:xs)
  | x == y    = xs
  | otherwise = error "case not dealt with"

somethingFunnya (x:y:xs) =
   if (x == y) then xs else error "case not dealt with"


-- Let's consider function calls

{-

myTail [True] : []  evaluates to [[]]

Why?

Function application in Haskell left-associative.

Let's consider the above expression in detail.

myTail    [True]       :        []
^^^^^     ^^^^^      ^^^^      ^^^^
function  value     operator   value

To make the above expression (syntactically) unambiguous.
we assume that function application has a higher preceedence than ":".
Hence, the above is interpreted as

(myTail    [True])       :        []

Hence,

myTrail [True] evaluates to []


Take note.

[] : [] evaluates to [[]]

In the above, the left operand is an element and the right operand is a list.
Consider the types.
Left operand is of type [a].
Right operand is of type [[a]].



-}


-- What about "combining" two lists, say we append one list to the other?
-- In Haskell, many function definitions combine
-- (a) pattern matching and
-- (b) recursion
append :: [a] -> [a] -> [a]
append [] ys = ys                           -- A1
append (x:xs) ys = x : (append xs ys)       -- A2

{-
 The above states:

 If the first list is empty, then simply yield the second list.
 Note. Pattern variable ys matches against any list.


-}


{-

Let's evaluate the following expression by hand.

   append [1,2] [3,4]

=>  1. We check for matching patterns.
       A1 does not apply. The empty list pattern [] does not match [1,2].
       A2 applies.
         - Pattern (x:xs) matches [1,2].
           Recall [1,2] is syntactic sugar for 1 : 2 : [].
           Recall that ":" (cons) operator is right associative.
           That means, 1 : 2 : [] equals (1 : (2 : [])).

           We match (x:xs) against (1 : (2 : [])).
           This yields pattern bindings
               x = 1 and xs = 2:[].

         - Pattern ys matches [3,4]. This yields ys = [3,4].

  This means,

  append [1,2] [3,4]

=>  1 : (append [2] [3,4])

 Next evaluation step. Again A2 applies.
 (x:xs) matches [2] and ys matches [3,4].
 This yields x = 2, xs = [], ys = [3,4].

=> 1 : 2 : (append [] [3,4])

  Finally A1 applies.

=> 1 : 2 : [3,4]

   = [1,2,3,4]

-}

-- sum is pre-defined, hence, we call this "mySum"
mySum xs =
  if null xs then 0
  else head xs + mySum (tail xs)


mySum2 [] = 0
mySum2 (y:ys) = y + mySum2 ys


-- Let's skip every second element in a list.
skip [] = []
skip [x] = [x]                -- The pattern [x] is a short-hand for (x:[]).
skip (x:y:ys) = x : skip ys   -- The pattern (x:y:ys) is a short-hand for
                              -- (x:(y:ys)).
                              -- Why can't we write [x,y,ys]?
                              -- x, y are elements, ys is a list. Won' type check.

-- What about the order of pattern clauses?

-- The order of clauses does not matter here
-- because patterns are disjoint.
-- Disjoint means that there is no list value that is a match
-- for say the [] pattern and the [x] pattern and so on.
skip2 [x] = [x]
skip2 (x:y:ys) = x : skip2 ys
skip2 [] = []


-- Pattern clauses are tried from top to bottom (textual order).
-- For our case, this means that by the time we reach S3,
-- pattern ys can only match a singleton list.
-- Becaue S1 covers the empty list and S2 covers any list with at least two elements.
skip3 [] = []                      -- S1
skip3 (x:y:ys) = x : skip3 ys      -- S2
skip3 ys = ys                      -- S3


-- By the time we try Skip4-2 we know that
-- the pattern ys can only match either the empty list or a singleton list.

-- The type says the input is a list where all elements are of the same type 'a'.
-- The output is against such a list.
skip4 :: [a] -> [a]
skip4 (x:y:ys) = x : skip4 ys      -- Skip4-1
skip4 ys = ys                      -- Skip4-2

{-

-- functions

-- curried vs uncurried style


-}


-- "+" is overloaded, defined for all numbers.
plus :: Num a => a -> a -> a
plus x y = x + y

plus2 = \x -> (\y -> x + y)

-- In this definition of "plus",
-- we pass in all arguments at once.

-- We use here a tuple pattern of the form (x,y).
add :: Num a => (a, a) -> a
add (x,y) = x + y


-- Technically, the expression
--
--  (0) plus 1 3
--
-- is ambiguous in the syntactic sense. Why?
-- (1) (plus 1) 3
-- (2) plus (1 3)
-- Function application is left associative.
-- Hence, (0) is interpreted as (1).

plusOf1And3 = plus 1 3

-- What is the result of applying "plus 1".

inc x = 1 + x

-- Partial function application.
-- plus 1 is a function that expects another number and yields a number where we add one.
inc2 = plus 1


-- We're introducing syntax to define functions.


-- Recall calculus ("lambda" notation for functions).
inc3 =   \ x      ->                     x + 1
--      ^^^^     ^^^^                    ^^^^^^
--   Start of
--   function,
--   x is the
--   parameter
--              delimiter
--              before parameters
--              after function body
--                                       function body

inc4 = \x->x+1
inc5 = \ x -> x   +1

-- Parse error:  "->" is a keyword.
-- inc6 = \x - > x+1

-- plus2 1
-- yields
-- (\y -> 1 + y)


apply f x = f x

-- The function space operator "->" is right associative.
-- f has type  t1 -> t2
-- x has type t1
-- Higher-order function because argument f is a function.
apply2 :: (t1 -> t2) -> (t1 -> t2)
apply2 =  \f -> \x -> f x

true = \x -> \y -> x

false = \x -> y -> y

ite e1 e2 e3 = (e1 e2) e3

-- Same notation for the above.
-- ite = \e1 -> \e2 -> \e3 ->  (e1 e2) e3


{-

Desired behavior.

(1) ite true e2 e3 -> e2

(2) ite false e2 e3 -> e3


Let's consider (1).

ite (\x -> \y -> x) e2 e3

= assuming we add (..)

((ite (\x -> \y -> x)) e2) e3

->  ( (\x -> \y -> x) e2) e3

->  (\y -> e2) e3

->  e2

That's exactly what we want.

Let's consider (2).

((ite (\x -> \y -> y)) e2) e3

->  ( (\x -> \y -> y) e2) e3

=   ([ e2 / x] (\y -> y)) e3

=  (\y -> y) e3

-> e3

Magic! That's exactly what we want.


-}

-- Doing the same thing differently.

-- Check if there are any duplicate elements in a list.
-- We report True if there are no duplicates.
-- Algorithm:
-- Iterate through the list,
-- for each element x check if x appears in the remaining list of elements.
duplicates [] = False
duplicates [x] = False
duplicates (x:xs)
  | elem x xs = True
  | otherwise = duplicates xs


duplicates2 xs =
    not $ null $
    filter (\zs -> length zs /= 1)
    $ map (\x -> filter (\y -> x == y) xs) xs


duplicates3 xs =
  (not.null)
  [ zs | zs <- [  [ y | y <- xs, x == y ] | x <- xs ], length zs /= 1 ]

{-

Question:

Could you demonstrate the reduction of the exercise out of the last test?
(\x -> \y -> x (x y)) (\z -> z)

1. All lambda binders introduce distinct names.
Hence, no alpha-renaming is necessary.

2. Let's add some (..) to make highlight what is the lambda body connected to (\x -> ...)

(\x -> (\y -> x (x y))) (\z -> z)

Let's start apply the beta-reduction rule.

    (\x -> (\y -> x (x y))) (\z -> z)
     ^^    ^^^^^^^^^^^^^^^  ^^^^^^^^^
                t1            t2

--> [(\z -> z) / x] (\y -> x (x y))

  = \y -> (\z -> z) ((\z -> z) y)


Observation, under CBN and CBV we will stop evaluating!

Observation, if the lambda term is "terminating" then
innermost and outermost reduction will yield the same value.

(a)

   =alpha  \y -> (\z1 -> z1) ((\z2 -> z2) y)
                         ^^  ^^^^^^^^^^^^^^^
                         t1       t2
-->outermost

      \y ->  [((\z2 -> z2) y) / z1] z1

    = \y ->  ((\z2 -> z2) y)

-->   \y -> y


Let's consider applying innermost first.

(b)     \y -> (\z1 -> z1) ((\z2 -> z2) y)
                                   ^^  ^^
                                   t1  t2

-->innermost

       \y -> (\z1 -> z1) ([y / z2] z2)

    = \y -> (\z1 -> z1) y

-->  \y -> y

-}

-- Let's look at the Church encoding

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE IncoherentInstances #-}   -- required due to instances I1 and I2

-- Church encoding of Booleans.

true = \x -> \y -> x
false = \x -> \y -> y
ifThenElse :: (t1 -> (t2 -> t3)) -> t1 -> t2 -> t3
ifThenElse x y z = (x y) z
-- Recall: Function application is left-associative.
--  1. x has type (t1 -> t2 -> t3). Isn't this ambiguous?
-- Why ambiguous? Compare  t1->(t2->t3) versus (t1->t2)->t3!
-- But, function arrow is right-associative.
-- 2. y has type t1.
-- 3. z has type t2.
-- Point to note.
-- (x y) has type t2 -> t3 because
--    x has type t1 -> (t2 -> t3)    and y has type t1
-- Therefore, (x y) z has type t3.
--
-- We apply here the following general rule.
--  if f is of type t1->t2 and e is of type t1
--  then (f e) is of type t2.


-- Is there a difference if I write the following?
-- It's the same thing!
ifThenElse2 x y = \ z -> (x y) z

ifThenElse3 = \x -> \y -> \ z -> (x y) z


{-

     ifThenElse false false true

-->  true

     true is a function defined as \x -> \y -> x

 How can "show" the true value on the console?
 Think of printf!?
 We need to convert the machine representation of a value into a string (for display on the console).
 Typical examples are Integer, Floatingpoint, ... values.

 C++ supports overloaded output stream operators!
 That is, for your own types you can specify the desired output.

*Main> ifThenElse false false true
TRUE

What's happening here?

    Haskell will evaluate

 ifThenElse false false true -->* true
 where true is defined as the function  \x -> \y -> x


-}


notC x = ifThenElse x false true
andC x y = ifThenElse x y false
orC x y = ifThenElse x true y


-- We use here higher-order abstract syntax (HOAS).
-- How to display/show the syntax such as Haskell functions?
-- We can play a trick by overloading the show function.



instance Show (t->t1->t) where                                   -- I1
   show _ = "TRUE"

instance Show (t->t1->t1) where                                  -- I2
   show _ = "FALSE"



-- Examples
ex = ifThenElse true true false
ex2 = ifThenElse ex (andC false ex) false
ex2a = ifThenElse false true false


-- Church encoding of pairs.

mkPair x y = \b -> b x y
fstP p = p true
sndP p = p false


ex3 = fstP (mkPair ex ex2)

-- Church encoding of lists.
nullL = mkPair true true                        -- first element
                                               -- indicates list is empty
isNull = fstP
consL = \h -> \t -> mkPair false (mkPair h t)  -- non-empty list
                                               -- as a pair of (head,tail)
headL = \z -> fstP (sndP z)                    -- head = first element of
                                               --        the second pair
tailL = \z -> sndP (sndP z)                    -- tail = second element of
                                               --        the second pair

ex4 = consL true (consL false nullL)

ex5 = headL ex4

-- Church encoding of natural numbers.
-- n represented as n compositions of function f.

zeroN = \f -> \x -> x
succN = \n -> \f -> \x -> f (n f x)

plusN = \m -> \n -> \f -> \x -> m f (n f x)

isZeroN = \n -> n (\x -> false) true

{-# LANGUAGE FlexibleInstances #-}

-- instance Show (List Int) demands "flexible" instances.
-- Reason: By default, Haskell imposes very strict conditions on type classes and their instances.
-- If we don't impose such strict conditions, we can write programs at the level of types.
-- In fact, we can encode the lambda calculus, Turing machines, ... at the level of types.

data List a = Null | Cons a (List a) deriving (Show, Eq)

-- The following instances can be derived automatically.
{-
instance Show (List Int) where
   show Null = "Null"
   show (Cons x xs) = "Cons " ++ show x ++ "(" ++ show xs ++ ")"
                            --   Show Int

instance Show (List Bool) where
   show Null = "Null"
   show (Cons x xs) = "Cons " ++ show x ++ "(" ++ show xs ++ ")"
                              -- Show Bool
-}

-- Parametric instances. Subsumes the above two instances!
-- We can define show for values of type "List a",
-- if we can provide show for values of type "a".
-- Via "deriving Show" we can automatically obtain the following instance.
{-
instance Show a => Show (List a) where
   show Null = "Null"
   show (Cons x xs) = "Cons " ++ show x ++ "(" ++ show xs ++ ")"
                             --  Show a
-}

mfilter p Null = Null
mfilter p (Cons x xs)
   | p x       = Cons x (mfilter p xs)
   | otherwise = mfilter p xs


-- some list examples

-- [1,2,3]
list1 :: List Int
list1 = Cons 1 (Cons 2 (Cons 3 Null))


{-

Cons 1 (2 : [])

yields a type error cause the types

 List Int

and

 [Int]

are different.
-}

-- [True,False]
list2 :: List Bool
list2 = Cons True (Cons False Null)

coerce :: List a -> [a]
coerce Null = []
coerce (Cons x xs) = (:) x (coerce xs)

coerceF :: [a] -> List a
coerceF [] = Null
coerceF (x:xs) = Cons x (coerceF xs)

{-

The following type checks.

Cons 1 (coerceF (2 : []))

-}

{-

Requires an instance of equality, indicated as "Eq t",
because we compare list values, see "x == y".

-}
member :: Eq t => t -> List t -> Bool
member x Null = False
member x (Cons y ys)
    | x == y    = True
    | otherwise = member x ys

{-

Haskell data types and type classes: Regular expression example.

-}


import Test.QuickCheck



{-

EBNF Syntax of regular expressions and words

 R ::= 'x' | 'y' | ...              alphabet symbols
     | epsilon                      represents the empty string
     | R + R                        alternatives
     | R . R                        concatenation
     | R*                           Kleene star
     | (R)                          Grouping via parentheses


 W ::= epsilon | 'x' | 'y' | ...
   | W W

-}

-- Data type to represent regular expressions.
data R = Epsilon
       | Sym Char
       | Alt R R
       | Conc R R
       | Star R deriving Eq  -- automatically derive equality among regular expressions

{-
-- The following instance can be derived automatically.
instance Eq R where
   (==) Epsilon Epsilon = True
   (==) (Sym x) (Sym y) = x == y
   (==) (Alt r1 r2) (Alt s1 s2) = r1 == s1 && r2 == s2
   (==) (Conc r1 r2) (Conc s1 s2) = r1 == s1 && r2 == s2
   (==) (Star r) (Star s) = r == s
-}

-- Show instance for regular expressions
instance Show R where
  show Epsilon = ""
  show (Sym x) = [x]
  show (Alt r s) = "(" ++ show r ++  "+" ++ show s ++ ")"
  show (Conc r s) = "(" ++ show r ++  "." ++ show s ++ ")"
  show (Star s) = "(" ++ show s ++ ")" ++ "*"


-- some regular expressions plus short-hands
x = Sym 'x'
y = Sym 'y'

r1 = Star x
r2 = Star $ Alt x y
r3 = Conc y r2
r4 = Alt (Conc Epsilon r1) r1


-----------------------------------------------------------------------
-- Writing functions that operate on data types via pattern matching.


-- Yield True if epsilon is part of the language, otherwise, we find False.
nullable :: R -> Bool
nullable Epsilon = True
nullable Sym{} = False
nullable (Alt r s) = nullable r || nullable s
nullable (Conc r s) = nullable r && nullable s
nullable Star{} = True

-- Splitting a word into two subwords where we consider all combinations.
split :: [Char] -> [([Char],[Char])]
split [] = []
split [x] = [([],[x]), ([x],[])]
split (x:xs) = [(x:ys,zs) | (ys,zs) <- split xs] ++ [([],x:xs)]


-- Property:
-- If we split a list xs into a pair (ys,zs), the concatenated pair, ys++zs,
-- must be equal to xs.
propSplit :: [Char] -> Bool
propSplit xs = and $ map (\(ys,zs) -> xs == ys++zs) $ split xs


-- Variant of split where we use fold and map.
split2 :: [Char] -> [([Char],[Char])]
split2 xs =
  foldr (\x -> \yzs -> map (\(ys,zs) -> (x:ys,zs)) yzs
                       ++ (case yzs of
                             [] -> [([],[x]), ([x],[])]
                             ((ys,zs):_) -> [([],x:(ys++zs))]))
        [] xs


-- match xs r, check if regular expression r matches the word xs.
-- We apply a naive approach where we check for all possible combinations.
-- For example, consider the case for concantenation.
--
-- Consider the expression R . S and the word W.
-- R . S matches W if
-- for any words W1, W2 where W = W1 W2 we find that
--    R matches W1 and
--    S matches W2.
match :: [Char] -> R -> Bool
match [] r = nullable r
match [x] (Sym y) = x == y
match xs (Alt r s) = match xs r || match xs s
match xs (Conc r s) = any (\(ys,zs) -> match ys r && match zs s) $ split xs
match xs (Star r) = any (\(ys,zs) -> match ys r && match zs (Star r)) $ split xs
match _ _ = False


-- Simplifying expressions:
-- epsilon . R = R
-- R + R = R
--
-- We build a "fixpont"!
-- We apply helper simp2 until no further simplifications can be applied.
-- Why is this necessary? Hint. Consider example r4.
simp :: R -> R
simp r = let s = simp2 r
         in if s == r then r
            else simp s
     where
        simp2 (Conc Epsilon r) = simp2 r
        simp2 (Conc r s) = Conc (simp2 r) (simp2 s)
        simp2 (Alt r s)
           | r == s    = simp2 r
           | otherwise = Alt (simp2 r) (simp2 s)
        simp2 (Star r) = Star $ simp2 r
        simp2 r = r



-- Parametric data types.
-- The alphabet sigma is now a parameter.
data RE a = EpsRE
       | SymRE a
       | AltRE (RE a) (RE a)
       | ConcRE (RE a) (RE a)
       | StarRE (RE a)  deriving Show


sym_x = SymRE 'x'
sym_y = SymRE 'y'

reg_r1 = StarRE sym_x
reg_r2 = StarRE $ AltRE sym_x sym_y
reg_r3 = ConcRE sym_y reg_r2
reg_r4 = AltRE (ConcRE EpsRE reg_r1) reg_r1


instance Eq a => Eq (RE a) where
   (==) EpsRE EpsRE = True
   (==) (SymRE x) (SymRE y) = x == y
   (==) (AltRE r1 r2) (AltRE s1 s2) = r1 == s1 && r2 == s2
   (==) (ConcRE r1 r2) (ConcRE s1 s2) = r1 == s1 && r2 == s2
   (==) (StarRE r) (StarRE s) = r == s


nullableRE :: RE a -> Bool
nullableRE EpsRE = True
nullableRE SymRE{} = False
nullableRE (AltRE r s) = nullableRE r || nullableRE s
nullableRE (ConcRE r s) = nullableRE r && nullableRE s
nullableRE StarRE{} = True


splitWord :: [a] -> [([a],[a])]
splitWord xs =
  foldr (\x -> \yzs -> map (\(ys,zs) -> (x:ys,zs)) yzs
                       ++ (case yzs of
                             [] -> [([],[x]), ([x],[])]
                             ((ys,zs):_) -> [([],x:(ys++zs))]))
        [] xs

matchRE :: Eq a => [a] -> RE a -> Bool
matchRE [] r = nullableRE r
matchRE [x] (SymRE y) = x == y
matchRE xs (AltRE r s) = matchRE xs r || matchRE xs s
matchRE xs (ConcRE r s) = any (\(ys,zs) -> matchRE ys r && matchRE zs s) $ splitWord xs
matchRE xs (StarRE r) = any (\(ys,zs) -> matchRE ys r && matchRE zs (StarRE r)) $ splitWord xs
matchRE _ _ = False

{-# LANGUAGE GADTs #-}

----------------------------------
-- Existential data types

-- A thing is a value of some type 'a'
-- where for 'a' we have an instance of the Show type class
data Thing = forall a. Show a => MkThing a


instance Show Thing where
    show (MkThing x) = show x
-- We don't know much about "thing".
-- Could be an integer, ...
-- All we know is that each "thing" is showable.

thing1 = MkThing [True]


data List a = Nil | Cons a (List a)

-- Can't build 'Thing' cause no instance of Show for 'List Bool'.
-- thing2 = MkThing (Cons True Nil)


----------------------------------
-- Arithmetic expressions (GADTs)

-- AST for arithmetic expressions
data E = One | Zero | ETrue | EFalse
       | Plus E E | Mult E E
       | Or E E

-- Arithmetic expressions are well-formed by construction.
ex1 = Mult One (Plus One Zero)


-- The following ill-formed expression will not be accepted.
-- ex2 = Mult One Plus


-- Well-formed but ill-typed.
-- Hence,
-- (A) evaluator needs to perform (dynamic) type checks, or
-- (B) first type check expression (see "typecheck")
ex3 = Plus One ETrue


-- Case (A)
eval_RunTimeTypeCheck :: E -> Maybe (Either Int Bool)
eval_RunTimeTypeCheck One = Just (Left 1)
eval_RunTimeTypeCheck EFalse = Just (Right True)
eval_RunTimeTypeCheck (Plus e1 e2) =
     let r1 = eval_RunTimeTypeCheck e1
         r2 = eval_RunTimeTypeCheck e2
     in case (r1, r2) of
         (Just (Left i1), Just (Left i2)) -> Just (Left (i1 * i2))
         -- Run-time type check!
         -- Pattern Just (Left i1) expresses that evalution yields some integer value.
         (_,_)  -> Nothing
eval_RunTimeTypeCheck _ = error "add missing cases"


-- Case (B)
eval_AssumesStaticTypeCheck :: E -> Either Int Bool
eval_AssumesStaticTypeCheck (Plus e1 e2) =
    case (eval_AssumesStaticTypeCheck e1, eval_AssumesStaticTypeCheck e2) of
       (Left i1, Left i2) -> Left (i1 + i2)
       -- Non-exhaustive, we don't cover all cases!
       -- What about (Right _, Right _)?
       -- Under the assumption that we apply "typecheck" first,
       -- only case (Left _, Left _) is possible.


-- GADT to guarantee by construction that expressions are well-formed and well-typed!
data Exp a where
   One_Exp :: Exp Int
   ETrue_Exp :: Exp Bool
   Plus_Exp :: Exp Int -> Exp Int -> Exp Int


-- Well-formed but ill-typed.
-- ex4 = Plus_Exp One_Exp ETrue_Exp

-- Evaluation of well-typed expressions.
-- No need for "Either" cause each expression
-- is represented as a value of type 'Exp a'
-- where 'a' is the type of the expression.
evalExp :: Exp a -> a
evalExp One_Exp = 1
evalExp ETrue_Exp = True
evalExp (Plus_Exp e1 e2) = evalExp e1 + evalExp e2

{-# LANGUAGE BangPatterns #-}

-- Haskell supports lazy evaluation.
-- Lots of cool applications but can also bite us!

---------------------------------------------------------------------------------------------
-- Stream, infinite sequence of data (numbers, temperature reading, internet traffic, ...)

-- Simplified stream example.
data Stream a = Cons a (Stream a) deriving Show
-- Compare this to lists.
data List a = ConsL a (List a) | Null
-- Observation:
-- Every value of type List a is finite!
-- How to emulate the stream data type say in a Java like language?
data JavaStr a = ConsS a (() -> JavaStr a)
--                       ^^^^^^^^^^^^^
--                  suspended computation
--                  () -> Str a   refers to a parameter-less function that yields a stream
--                  thus we can suspend the computation (and emulate lazy evaluation in a strict language)

headS :: Stream a -> a
headS (Cons x _) = x

headStr :: JavaStr a -> a
headStr (ConsS x _) = x

tailS :: Stream a -> Stream a
tailS (Cons x xs) = xs

tailStr :: JavaStr a -> JavaStr a
tailStr (ConsS _ f) = f ()   -- force the computation, i.e. take one step

succN :: Integer -> Stream Integer
succN n = Cons n (succN (n+1))

-- Natural numbers: 0, 1, ...
nats :: Stream Integer
nats = succN 0

mapS :: (a -> b) -> Stream a -> Stream b
mapS f (Cons x xs) = Cons (f x) (mapS f xs)

-- Negative numbers: -1, -2, ...
negs :: Stream Integer
negs = mapS (\x -> -x) (tailS nats)

-- interleaveS applied to
--     ... x0, x1, ...
--     ... y0, y1, ...
-- yields
--     ... x0,y0,x1,y1, ...
interleaveS :: Stream a -> Stream a -> Stream a
interleaveS (Cons x xs) ys = Cons x (interleaveS ys xs)

-- All positive, negative numbers.
ints :: Stream Integer
ints = interleaveS nats negs

firstN :: Int -> Stream Integer -> [Integer]
firstN n (Cons x xs)
 | n < 0     = error "must be positive"
 | n == 0    = []
 | otherwise = x : firstN (n-1) xs


-------------------------------------------------------------------------------------------
-- The bad and the ugly. Space leaks!
msum [] = 0
msum (x:xs) = x + msum xs

test_msum = do
 print (msum [1..1000000000]) -- warning, leads to stack overflow


{-
 In an imperative language, we'd use a for loop.
 acc := 0
 for each element x in xs
   acc = acc + x

-}
msum2 acc [] = acc
msum2 acc (x:xs) = msum2 (acc+x) xs

-- Issue: Lazy evaluation is the problem.
-- We won't evaluate acc+x unless needed.
-- That means, for a list say [x1, ..., xn]
--  we build up the huge expression
--  x1 + ... + xn.
-- This is really bad here!

test_msum2 = do
 print (msum2 0 [1..1000000000]) -- warning, leads to stack overflow

-- In this case, we would like to strictly evaluate
-- the accumlated numbers.
-- In Haskell, we can use bang patterns (!)
-- to tell the compiler that the argument shall be
-- evaluated strictly.

msum3 !acc [] = acc
msum3 !acc (x:xs) = msum3 (acc+x) xs


test_msum3 = do
 print (msum3 0 [1..1000000000])



main = test_msum
-- main = test_msum2
-- main = test_msum3

{-


AOR, NOR, CBN, CBV

Recall the example from the lecture notes "lambda calculus"

// Haskell version
inc :: Int -> Int
inc x = x + 1

f :: Int -> Int
f x = inc(1+1) + x

main = f (1+2)

The above is not quite a "pure" lambda term.
We give lambdas a name and we assume arithmetic.

Recall

inc :: Int -> Int
inc x = x + 1

is a short-hand for

inc :: Int -> Int
inc = \x -> x + 1

Let's consider the main expression.

f (1+2)

Let's inline all the function definitions.

1. Inline f

(\x -> inc(1+1) + x) (1 + 2)

2. Inline inc


(\x -> ((\x -> x + 1) (1+1)) + x) (1 + 2)

Recall

AOR = Look for a redex innermost, leftmost

For our example, we find the following

(\x -> ((\x -> x + 1) (1+1)) + x) (1 + 2)
                      ^^^^^
                  innermost, leftmost redex


Recall

CBV = AOR but "don't evaluate under a lambda"

That is, the above redex "1+1" won't be choosen under CBV,
because the redex appears under a lambda.

What are the choices we have that satisfy the criteria:
   Innermost, leftmost and not under a lambda?


(\x -> ((\x -> x + 1) (1+1)) + x) (1 + 2)
                                  ^^^^^^^
                  the innermost, leftmost redex that doesn't appear under a lambda


(\x -> ((\x -> x + 1) (1+1)) + x) (1 + 2)

-->CBV

(\x -> ((\x -> x + 1) (1+1)) + x) 3
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
the innermost, leftmost redex that doesn't appear under a lambda

-->CBV

[3 / x]  ((\x -> x + 1) (1+1)) + x)

            Be careful. There's the potential for a name clash here because
            there's some inner lambda term that also refers to x.

=  ((\x -> x + 1) (1+1)) + 3
                  ^^^^^

-->CBV

((\x -> x + 1) 2) + 3
^^^^^^^^^^^^^^^^^

-->CBV

(2 + 1) + 3
^^^^^^

-->CBV

3 + 3

-->CBV

6

In contrast, evaluation under AOR proceeds as follows.


(\x -> ((\x -> x + 1) (1+1)) + x) (1 + 2)
                      ^^^^^
                  innermost, leftmost redex

-->AOR

(\x -> ((\x -> x + 1) 2) + x) (1 + 2)
        ^^^^^^^^^^^^^^^
         innermost, leftmost redex

-->AOR

(\x -> (2 + 1) + x) (1 + 2)
       ^^^^^^
       innermost, leftmost redex

-->AOR

(\x -> 3 + x) (1 + 2)
              ^^^^^^^

-->AOR

(\x -> 3 + x) 3


-->AOR

3 + 3

-->AOR

6


Side note:

There are two possible subterms on which we can apply a reduction.

(\x -> (2 + 1) + x) (1 + 2)
       ^^^^^^                             Choice 1
                    ^^^^^^^               Choice 2

^^^^^^^^^^^^^^^^^^^^^^^^^^^^              Choice 3
      means that we take "1 + 2" as argument and apply it to (\x -> (2+1) + x)


Choice 1 is the innermost leftmost redex

Choice 2 is the innermost leftmost redex not under a lambda

Choice 3 is the outermost leftmost redex


Why leftmost?
Well, there can be several innermost reductions.
Consider the following example

 (1 + 2) * (3 * 4)
 ^^^^^^
           ^^^^^^^

Both underlined redexes are innermost.
Leftmost is simple a strategy to pick a specific redex unambiguously.



CBN vs lazy evaluation

Consider

(\(x,y) -> x + y) (1+2, 1+2)

Point to note, in (1+2, 1+2) we find two identical subterms!

Under CBN evaluation proceeds as follows.


(\(x,y) -> x + y) (1+2, 1+2)

-->CBN (1+2) + (1+2)

-->CBN 3 + (1+2)

-->CBN 3 + 3

-->CBN 6

Lazy evaluation is a form of optimization of CBN.
If we need to evaluation the same (identical) subterms,
we immediately reuse the result.


(\(x,y) -> x + y) (1+2, 1+2)

-->Lazy (1+2) + (1+2)

-->Lazy 3 + 3       -- We evaluation 1+2 to 3 and realize
                    -- there's another occurence of 1+2 and
                    -- immediately use the result 3
-}




-- DATA TYPES

-- predefined
-- data Maybe a = Just a | Nothing

-- Parametric, recursive algebraic data type to describe lists
data List a = Null | Cons a (List a) deriving Show


{-

On the left-hand side we introde a new type data "List a".

The right-hand side describes the possible set of list values.
Lists are always of a finite size.

There can be the empty list represented by Null.

There can be lists consisting of a single element.
For example,

 Cons 1 Null

describes a list consisting of the integer 1.

 Cons 1 (Cons 2 Null)

describes a list consisting of the integer 1 followed by the integer 2.


 Cons (Cons 1 Null) Null

describes a list consisting of a single element where the element is itself a list.


We can definie functions that operate on the "List a" data type using pattern matching syntax.


-}


headL :: List a -> a
headL (Cons x _) = x



-- FUNCTIONS: Application is left-associative, functions types are right-associative.


-- functions
f :: Int -> Int -> Int
f x y = x + y


{-

function application is left-associative (our definition).

That means,

f 1 2

shall be interpreted as

(f 1) 2
^^^^^
yields a function that expects an integer,
we assume that the final result is an integer as well.

This implies that f is a function of the followoing type


f :: Int -> (Int -> Int)

To reduce noise in our program, we wish to remove (..) while
making sure that the syntax of programs remains unambigous.

Our only choice then is to assume that function types are right-associative.

That means,

the following two type annotations are equivalent.


f :: Int -> (Int -> Int)

f :: Int -> Int -> Int




-}

-- MOTVATION: Imperative programming and monads.

import Data.IORef

{-

Haskell is a pure language.
A pure function will always compute the same result for the same set of inputs (no side effects).

We can't reassign let/where defined variable.

-}

inc :: Int -> Int
inc x = let y = x + 1
        in y


-- The following will not work!
-- x will be evaluated lazily and based on the equation "x = x + 1",
-- the computation will never terminate.
inc2 :: Int -> Int
inc2 x = let x = x + 1
         in x

{-
-- Compiler complains: Conflicting definitions for ‘y’
inc3 :: Int -> Int
inc3 x = let y = 1
             y = x + y
         in y
-}


{-

-- C program where we perform in-place update and output a string to the console.
-- In-place updates and side-effects such as sending some output to the console is easy.

int x;

int inc_x() {
 printf("%d", x);
 x = x + 1;
 // The above means the following:
 // Right-hand side expression: x + 1
 // 1. Read the value storted in x.
 // 2. Add this value to 1.
 // Assignment: x = x + 1
 // Overwrite the value stored in x, by the value we just computed.
 return x;
}


-}

-- In Haskell, we can do the same, but it's more verbose.

-- In C, the Haskell type "IORef Int" corresponds to "int*" (pointer type).

incRef2 :: IORef Int -> IO Int
incRef2 x = do
  v <- readIORef x      -- Dereferencing, in C this would be "*x"
  writeIORef x (v+1)    -- Overwrite, in C this would be "*x = v + 1"
  return (v+1)


-- incRef3 :: IORef Int -> IO (IORef Int)    -- this would be a more specific type.
incRef3 :: Num a => IORef a -> IO (IORef a)
incRef3 x = do
  v <- readIORef x      -- Dereferencing, in C this would be "*x"
  writeIORef x (v+1)    -- Overwrite, in C this would be "*x = v + 1"
  return x



-- How to output a string to the console, do in-place update in Haskell!?


-- In an impure world, we must explictly keep track of any impure effects.
-- Do deal with in-place update, keep track of the state of variables.

type State = [(String, Int)]   -- represent, name of a variable and its current value.

readS :: String -> State -> (State,Int)
readS x w = case lookup x w of
                    Just v -> (w,v)

-- Overwrite by a a new value.
writeS :: (String, Int) -> State -> State
writeS (x,v) w =  (x,v) : [ (y,u) | (y,u) <- w, y /= x ]

inc_x :: State -> (State, Int)
inc_x st = let (st2,v) = readS "x" st
               st3 = writeS ("x", v+1) st2
               (st4, u) = readS "x" st3
           in (st4, u)


test_inc = let (st,v) = inc_x [("x",0)]
           in v


-- What out printing a string to the console?
-- In addition to the state of variables, must keep track of the state of the console.

type Console = [String]
type World = (State, Console)

readW :: String -> World -> (World, Int)
readW x (st,c) = case lookup x st of
                    Just v -> ((st,c),v)

printW :: String -> World -> World
printW out (st,c) = (st,c ++ [out])


-- and so on ...


-- SHORT SUMMARY:
-- "Simple" things like I/O, in-place updates seem really (really) difficult in Haskell.

-- SOLUTION:
-- In Haskell we capture side-effects via monads.
--
--  What is a monad?
--
--  Short and complicated answer.
--  A monad is a mathematical strucure known from category theory. See Kleisli triple, ...

--  Short and simple answer.
--  Monads allow for the systematic control of side effects where
--  (1) Computations and their results are described via types, and
--  (2) side-effecting computations are build via functional composition of primitive monad functions.
--  Thus, we can hide details such as (hidden) state etc.



-- "IO" is a monad, referred to as the "I/O" monad.
-- "IO Int" effectively represents "World -> (World, Int)"
incIO :: Int -> IO Int
incIO x = do print x
             return (x+1)


-- Alternative notation for the above.
incIO2 :: Int -> IO Int
incIO2 x = do { print x; return (x+1) }


-- In-place update of a variable implies that the variable is stored somewhere in memory.
-- In the C programming language, we can represent the memory location of an int variable via "int *".
-- In Haskell, write "IORef Int".

-- Side-effects that involve in-place updates are part of the IO monad.
incRef :: IORef Int -> IO Int
incRef x = do
  v <- readIORef x
  writeIORef x (v+1)
  return (v+1)

import Control.Monad
import Control.Monad.STM
import Control.Concurrent.STM.TVar

--------------------------
-- Maybe is a monad

-- data Maybe a = Just a | Nothing

divSafe :: Int -> Int -> Maybe Int
divSafe x y = if y == 0
          then fail "division by zero"
          else return (x `div` y)

-- The above is monadic sugar for the following

divSafe2 :: Int -> Int -> Maybe Int
divSafe2 x y = if y == 0
          then Nothing
          else Just (x `div` y)

divTwice x y = do  z <- divSafe x y
                   z2 <- divSafe z y
                   return z2

-- Above effectively corresponds to the following.
divTwice2 x y = case (divSafe x y) of
                   Just z ->  divSafe z y
                   Nothing -> Nothing


--------------------------
-- List ("[]") is a monad


incL xs = do x <- xs
             return (x+1)

sumL xs ys = do x <- xs
                y <- ys
                return (x+y)

-- Above effectively corresponds to the following.
sumL2 xs ys = [ x + y | x <- xs, y <- ys ]


----------------------------------------------------
-- Software Transactional Memory (STM) is a monad

swap :: TVar a -> TVar a -> STM ()
swap x y = do
   vx <- readTVar x
   vy <- readTVar y
   writeTVar x vy
   writeTVar y vx

testSwap :: IO ()
testSwap = do
   x1 <- newTVarIO (3::Int)
   x2 <- newTVarIO (5::Int)
   atomically (swap x1 x2)



-- STM effects (reads/writes) are executed atomically (all or nothing semantics).

{-

-- We can't mix STM and IO effects.
-- Hence, the below yields a type error.
-- Rightly so! How would we undo the effect of "print"?
swap2 :: TVar a -> TVar a -> STM ()
swap2 x y = do
   vx <- readTVar x
   vy <- readTVar y
   print vx
   print vy
   writeTVar x vy
   writeTVar y vx

-}