diff --git a/MD_metadata.md b/MD_metadata.md new file mode 100644 index 0000000..3f83e22 --- /dev/null +++ b/MD_metadata.md @@ -0,0 +1,19 @@ +--- +title: Curious OCaml +author: Lukasz Stafiniak +header-includes: + - + - + - +--- diff --git a/README.md b/README.md index 3ea3004..d51bb3d 100644 --- a/README.md +++ b/README.md @@ -1,3 +1,22 @@ +--- +title: Curious OCaml +author: Lukasz Stafiniak +header-includes: + - + - + - +--- # Curious OCaml # From logic rules to programming constructs diff --git a/dune b/dune index 22250c9..dc5f86f 100644 --- a/dune +++ b/dune @@ -2,6 +2,7 @@ (target README.md) (mode promote) (deps + MD_metadata.md chapter1/README.md chapter2/README.md chapter3/README.md @@ -17,6 +18,7 @@ (with-stdout-to README.md (progn + (cat MD_metadata.md) (echo "\n") (echo "# Curious OCaml\n") @@ -66,6 +68,7 @@ (with-stdout-to old_lectures_as_book.md (progn + (cat MD_metadata.md) (echo "\n") (echo "# Curious OCaml\n") diff --git a/old_lectures_as_book.md b/old_lectures_as_book.md index fd06c2d..b41b949 100644 --- a/old_lectures_as_book.md +++ b/old_lectures_as_book.md @@ -1,3 +1,22 @@ +--- +title: Curious OCaml +author: Lukasz Stafiniak +header-includes: + - + - + - +--- # Curious OCaml # Chapter 1 diff --git a/pdfs/dune b/pdfs/dune index aa5d0af..60c258a 100644 --- a/pdfs/dune +++ b/pdfs/dune @@ -25,7 +25,7 @@ (target new_book.pdf) (deps README.md) (action - (system "pandoc -s %{deps} -o %{target} --metadata title='Curious OCaml'"))) + (system "pandoc -s %{deps} -o %{target}"))) (rule (alias old_lectures_as_book) @@ -33,4 +33,4 @@ (target old_lectures_as_book.pdf) (deps old_lectures_as_book.md) (action - (system "pandoc -s %{deps} -o %{target} --metadata title='Functional Programming Course'"))) + (system "pandoc -s %{deps} -o %{target}"))) diff --git a/pdfs/new_book.pdf b/pdfs/new_book.pdf index e7f7724..0e46452 100644 Binary files a/pdfs/new_book.pdf and b/pdfs/new_book.pdf differ diff --git a/site/dune b/site/dune index 550c914..d197a39 100644 --- a/site/dune +++ b/site/dune @@ -31,7 +31,7 @@ (target new_book.html) (deps README.md) (action - (system "pandoc -s %{deps} -o %{target} --katex --metadata title='Curious OCaml'"))) + (system "pandoc -s %{deps} -o %{target}"))) (rule (alias old_lectures_as_book) @@ -40,4 +40,4 @@ (deps old_lectures_as_book.md) (action (system - "pandoc -s %{deps} -o %{target} --katex --metadata title='Functional Programming Course'"))) + "pandoc -s %{deps} -o %{target}"))) diff --git a/site/index.html b/site/index.html index 84a6bc2..218f0bd 100644 --- a/site/index.html +++ b/site/index.html @@ -4,28 +4,7 @@ A Curious OCaml Book - - - - - - + Lukasz Stafiniak @@ -34,21 +13,6 @@

Curious OCaml

Functional Programming 2012-2013

Functional Programming Course 2012-2013 slides converted to a book format -- conversion cleanup in progress. -

Test math rendering

-

How can we define them? Think in terms of derivation trees: -

-

\frac{\begin{array}{ll} - \frac{\begin{array}{ll} - \frac{\,}{\text{a premise}} & \frac{\,}{\text{another premise}} - \end{array}}{\text{some fact}} & \frac{\frac{\,}{\text{this we have by default}}}{\text{another fact}} - \end{array}}{\text{final conclusion}}

-

Define by providing rules for using the connectives: for example, a - rule \frac{\begin{array}{ll} a & b - \end{array}}{c} matches parts of the tree that have two premises, - represented by variables a and b, and have any - conclusion, represented by - variable c. -

\ No newline at end of file diff --git a/site/new_book.html b/site/new_book.html index 15c68ec..df5e185 100644 --- a/site/new_book.html +++ b/site/new_book.html @@ -4,6 +4,7 @@ + Curious OCaml - - - + + +

Curious OCaml

+

Lukasz Stafiniak

Curious OCaml

@@ -191,20 +179,20 @@

From logic rules to -\top -\bot -\wedge -\vee -\rightarrow +⊤ +⊥ +∧ +∨ +→ -a \wedge b -a \vee b -a \rightarrow b +a ∧ b +a ∨ b +a → b truth @@ -216,39 +204,39 @@

From logic rules to “trivial” “impossible” -a and b -a or b -a gives b +a and b +a or b +a gives b shouldn’t get got both got at least one -given a, we get b +given a, we get b

How can we define them? Think in terms of derivation trees:

-

+

$$ \frac{ \frac{\frac{\,}{\text{a premise}} \; \frac{\,}{\text{another premise}}}{\frac{\,}{\text{some fact}}} \; \frac{\frac{\,}{\text{a premise}} \; \frac{\,}{\text{another premise}}}{\frac{\,}{\text{another fact}}}} {\text{final conclusion}} -

+$$

To define the connectives, we provide rules for using them: for -example, a rule \frac{a \; b}{c} +example, a rule $\frac{a \; b}{c}$ matches parts of the tree that have two premises, represented by -variables a and b, and have any conclusion, represented by -variable c.

+variables a and b, and have any conclusion, +represented by variable c.

Rules for Logical Connectives

Introduction rules say how to produce a connective. Elimination rules diff --git a/site/old_lectures_as_book.html b/site/old_lectures_as_book.html index 7831a69..944fdbd 100644 --- a/site/old_lectures_as_book.html +++ b/site/old_lectures_as_book.html @@ -4,7 +4,8 @@ - Functional Programming Course + + Curious OCaml - - - + + +

-

Functional Programming Course

+

Curious OCaml

+

Lukasz Stafiniak

Curious OCaml

@@ -328,20 +316,21 @@

1 In the Beginning there was

How can we define them?Think in terms of derivation trees:

-

\frac{\begin{array}{ll} +

$$ \frac{\begin{array}{ll} \frac{\begin{array}{ll} \frac{\,}{\text{a premise}} & \frac{\,}{\text{another premise}} \end{array}}{\text{some fact}} & \frac{\frac{\,}{\text{this we have by default}}}{\text{another fact}} - \end{array}}{\text{final conclusion}}

+ \end{array}}{\text{final conclusion}} $$

Define by providing rules for using the connectives: for example, a -rule \frac{\begin{array}{ll} a & b -\end{array}}{c} matches parts of the tree that have two premises, -represented by variables a and b, and have any conclusion, represented by -variable c.

+rule $\frac{\begin{array}{ll} a & b +\end{array}}{c}$ matches parts of the tree that have two +premises, represented by variables a and b, and have any conclusion, +represented by variable c.

Try to use only the connective you define in its definition.# 2 Rules for Logical Connectives

Introduction rules say how to produce a connective.

@@ -405,24 +394,25 @@

1 In the Beginning there was

Notations

-

{{{\frac{\,}{a} \tiny{x}} \atop +

$$ {{{\frac{\,}{a} \tiny{x}} \atop {\text{\textbar}}} \atop {b}} \text{, \ \ or \ \ } {{{\frac{\,}{a} \tiny{x}} \atop {\text{\textbar}}} \atop {c}} -

-

match any subtree that derives b (or -c) and can use a (by assumption \frac{\,}{a} \tiny{x}) although otherwise -a might not be warranted. For +$$

+

match any subtree that derives b (or c) and can use a (by assumption $\frac{\,}{a} \tiny{x}$) although otherwise +a might not be warranted. For example:

-

+

$$ \frac{\frac{\frac{\frac{\frac{\,}{\text{sunny}} \small{x}}{\text{go outdoor}}}{\text{playing}}}{\text{happy}}}{\text{sunny} \rightarrow - \text{happy}} \small{\text{ using } x}

+ \text{happy}} \small{\text{ using } x} $$

Such assumption can only be used in the matched subtree! But it can be used several times, e.g. if someone’s mood is more difficult to influence:

-

\frac{\frac{\begin{array}{ll} +

$$ \frac{\frac{\begin{array}{ll} \frac{\frac{\frac{\,}{\text{sunny}} \small{x}}{\text{go outdoor}}}{\text{playing}} & \frac{\begin{array}{ll} \frac{\,}{\text{sunny}} \small{x} & @@ -430,17 +420,17 @@

1 In the Beginning there was \small{x}}{\text{go outdoor}} \end{array}}{\text{nice view}} \end{array}}{\text{happy}}}{\text{sunny} \rightarrow \text{happy}} - \small{\text{ using } x} Elimination rule for disjunction + \small{\text{ using } x} $$Elimination rule for disjunction represents reasoning by cases.

How can we use the fact that it is sunny\veecloudy (but not rainy)?

-

\frac{\begin{array}{rrl} +class="math inline">∨cloudy (but not rainy)?

+

$$ \frac{\begin{array}{rrl} \frac{\,}{\text{sunny} \vee \text{cloudy}} \tiny{\text{ forecast}} & \frac{\frac{\,}{\text{sunny}} \tiny{x}}{\text{no-umbrella}} & \frac{\frac{\,}{\text{cloudy}} \tiny{y}}{\text{no-umbrella}} \end{array}}{\text{no-umbrella}} \small{\text{ using } x, y} -

+$$

We know that it will be sunny or cloudy, by watching weather forecast. If it will be sunny, we won’t need an umbrella. If it will be cloudy, we won’t need an umbrella. Therefore, won’t need an umbrella.We @@ -448,15 +438,15 @@

1 In the Beginning there was induction (it is somewhat similar to reasoning by cases). Example rule for induction on natural numbers:

$$ x $$

-

So we get any p for any natural -number n, provided we can get it for -0, and using it for x we can derive it for the successor x + 1, where x is a unique variable (we cannot substitute -for it some particular number, because we write “using x” on the side).# 3 Logos was Programmed in -OCaml

+

So we get any p for any +natural number n, provided we +can get it for 0, and using it for +x we can derive it for the +successor x + 1, where x is a unique variable (we cannot +substitute for it some particular number, because we write “using x” on the side).# 3 Logos was +Programmed in OCaml

@@ -568,16 +558,16 @@

3.1 Definitions

type ty = some type.

@@ -4406,13 +4413,14 @@

8.2 Example: pretty-printing

Your function cycle can either return LNil or fail for an empty list as argument. 1. Note that *inv_fact* from the lecture defines -the power series for the \exp -(\cdot) function (\exp (x) = -e^x). Using *cycle* and +the power series for the exp (⋅) +function (exp (x) = ex). +Using *cycle* and *inv_fact*, define the power series for \sin (\cdot) and \cos (\cdot), and draw their graphs -using helper functions from the lecture script +class="math inline">sin (⋅) and cos (⋅), and draw their graphs using +helper functions from the lecture script *Lec7.ml*.

Exercise 3: * Modify one of the puzzle solving programs (either from the previous lecture or from your previous @@ -4422,12 +4430,12 @@

8.2 Example: pretty-printing

than computing solutions by the original program.

Exercise 4: Hamming’s problem. Generate in increasing order the numbers of the form 2^{a_{1}} 3^{a_{2}} 5^{a_{3}} \ldots -p_{k}^{a_{k}}, that is numbers not divisible by prime numbers -greater than the kth prime number.

+class="math inline">2a13a25a3…pkak, +that is numbers not divisible by prime numbers greater than the kth prime number.

  • In the original Hamming’s problem posed by Dijkstra, k = 3*, which is related
    • +class="math inline">k = 3*, which is related

to* http://en.wikipedia.org/wiki/Regular_number.

@@ -4696,9 +4704,8 @@

3 Monads

  • as if ; was replaced by >>=
  • [] |-> … does not produce anything – as needed by guarding
    • -
  • [()] |-> … \rightsquigarrow (fun -_ -> …) () \rightsquigarrow … -i.e. keep without change
    • +
  • [()] |-> … ⇝ (fun _ -> …) () +⇝ … i.e. keep without change

  • Throwing away the binding argument is a common practice, with infix syntax >> in Haskell, and supported in do-notation @@ -4853,7 +4860,7 @@

    3.1 Monad laws

    • A parametric data type is a monad only if its bind and return operations meet axioms:

      -

      \begin{matrix} +

      $$ \begin{matrix} \operatorname{bind} (\operatorname{return}a) f & \approx & f a\\\\\\ \operatorname{bind}a (\lambda x.\operatorname{return}x) & \approx @@ -4862,7 +4869,7 @@

      3.1 Monad laws

      & \approx & \operatorname{bind}a (\lambda x.\operatorname{bind}b (\lambda -y.c)) \end{matrix}

      • +y.c)) \end{matrix} $$

    • Check that the laws hold for our example monad

      let bind a b = concatmap b alet return x = [x]

    @@ -4875,31 +4882,31 @@

    3.2 Monoid laws and
  • mplus : 'a monoid -> 'a monoid -> 'a monoid

    • that meet the laws:

    -

    \begin{matrix} +

    $$ \begin{matrix} \operatorname{mplus}\operatorname{mzero}a & \approx & a \\\\\\ \operatorname{mplus}a\operatorname{mzero} & \approx & a \\\\\\ \operatorname{mplus}a (\operatorname{mplus}b c) & \approx & \operatorname{mplus} (\operatorname{mplus}a b) c \end{matrix} -

    • +$$

  • We will define fail as synonym for mzero and infix ++ for mplus.

  • Fusing monads and monoids gives the most popular general flavor of monads which we call monad-plus after Haskell.

  • Monad-plus requires additional axioms that relate its “addition” and its “multiplication”.

    -

    \begin{matrix} +

    $$ \begin{matrix} \operatorname{bind}\operatorname{mzero}f & \approx & \operatorname{mzero}\\\\\\ \operatorname{bind}m (\lambda x.\operatorname{mzero}) & \approx & -\operatorname{mzero} \end{matrix}

    • -

  • Using infix notation with \oplus -as mplus, \boldsymbol{0} -as mzero, \vartriangleright as bind and -\boldsymbol{1} as return, -we get monad-plus axioms

    -

    \begin{matrix} +\operatorname{mzero} \end{matrix} $$

    • +

  • Using infix notation with ⊕ as +mplus, 0 +as mzero, ⊳ as +bind and 1 as return, we +get monad-plus axioms

    +

    $$ \begin{matrix} \boldsymbol{0} \oplus a & \approx & a \\\\\\ a \oplus \boldsymbol{0} & \approx & a \\\\\\ a \oplus (b \oplus c) & \approx & (a \oplus b) \oplus c\\\\\\ @@ -4912,7 +4919,7 @@

    3.2 Monoid laws and \boldsymbol{0} \vartriangleright f & \approx & \boldsymbol{0}\\\\\\ a \vartriangleright (\lambda x.\boldsymbol{0}) & \approx & -\boldsymbol{0} \end{matrix}

    • +\boldsymbol{0} \end{matrix} $$

  • The list type has a natural monad and monoid structure

    let mzero = [] let mplus = (@) let bind a b = concatmap b a let return a = [a]

    • @@ -4975,16 +4982,17 @@

    4 Monad “flavors”

    We will not cover it.

  • Probabilistic computation:

    choose : float -> ’a monad -> ’a monad -> ’a monad

    -

    satisfying the laws with a \oplus _{p} -b for choose p a b and pq for p*.q, 0 \leqslant p, q \leqslant 1:

    -

    \begin{matrix} +

    satisfying the laws with a⊕pb +for choose p a b and pq for p*.q, +0 ≤ p, q ≤ 1:

    +

    $$ \begin{matrix} a \oplus _{0} b & \approx & b \\\\\\ a \oplus _{p} b & \approx & b \oplus _{1 - p} a\\\\\\ a \oplus _{p} (b \oplus _{q} c) & \approx & \left( a \oplus _{\frac{p}{p + q - pq}} b \right) \oplus _{p + q - pq} c\\\\\\ - a \oplus _{p} a & \approx & a \end{matrix}

    • + a \oplus _{p} a & \approx & a \end{matrix} $$

  • Parallel computation as monad with access and parallel bind:

    parallel :’a monad-> ’b monad-> (’a -> ’b -> ’c monad) -> ’c monad

    @@ -5175,8 +5183,8 @@

    6.2 Monads as computation

    let assemblyLine w = perform c <– makeChopsticks w c’ <– polishChopsticks c c’’ <– wrapChopsticks c’ return c’’

  • Any expression can be spread over a monad, e.g. for \lambda-terms:

    -

    \begin{matrix} +class="math inline">λ-terms:

    +

    $$ \begin{matrix} \llbracket N \rrbracket = & \operatorname{return}N & \text{(constant)}\\\\\\ \llbracket x \rrbracket = & \operatorname{return}x & @@ -5191,7 +5199,7 @@

    6.2 Monads as computation

    \rrbracket (\lambda v_{a} .\operatorname{bind} \llbracket b \rrbracket (\lambda v_{b} .v_{a} v_{b})) & \text{(application)} \end{matrix} -

    • +$$

  • When an expression is spread over a monad, its computation can be monitored or affected without modifying the expression.

    • @@ -5463,12 +5471,13 @@

    8.4 The state monad

  • The state monad is useful to hide passing-around of a “current” value.

  • We will rename variables in \lambda-terms to get rid of possible name +class="math inline">λ-terms to get rid of possible name clashes.

      -
    • This does not make a \lambda-term -safe for multiple steps of \beta-reduction. Find a counter-example.
      • +
    • This does not make a λ-term safe for multiple steps of +β-reduction. Find a +counter-example.

  • type term =| Var of string| Lam of string * term| App of term * term

    • @@ -5668,9 +5677,10 @@

    10.1 The probability monad

    • choose : float -> ’a monad -> ’a monad -> ’a monad

      choose p a b represents an event or distribution which -is a with probability p and is b -with probability 1 - p.

      • +is a with probability p and is b with probability 1 − p.

    • val pick : (’a * float) list -> ’a t

      A result from the provided distribution over values. The argument must be a probability distribution: positive values summing to @@ -5724,15 +5734,15 @@

      10.1 The probability monad

      probability distribution – naive implementation. type ’a t = (’a * float) list
      let bind a b = merge``x w.p. p and then y w.p. q happens =[y, q*.p | (x,p) <- a; (y,q) -<- b x]y results w.p. p -q. let return a = [a, 1.]Certainly a. end include M -include MonadOps (M) let choose p a b = List.map (fun (e,w) -> e, -p.w) a @ List.map (fun (e,w) -> e, (1. -.p).w) b let pick -dist = dist let uniform elems = normalize (List.map (fun -e->e,1.) elems)let coin = [true, 0.5; false, 0.5] let flip p = [true, -p; false, 1. -. p]

      +class="math inline">p and then y w.p. q happens =[y, q*.p | (x,p) <- a; +(y,q) <- b x]y results w.p. pq. let return a = [a, +1.]Certainly a. end include M include MonadOps (M) let +choose p a b = List.map (fun (e,w) -> e, p.w) a @ List.map (fun +(e,w) -> e, (1. -.p).w) b let pick dist = dist let +uniform elems = normalize (List.map (fun e->e,1.) elems)let coin = +[true, 0.5; false, 0.5] let flip p = [true, p; false, 1. -. p]

      let prob p m = m |> List.filter (fun (e,) -> p e)All cases where p holds, |> List.map snd |> List.foldleft (+.) 0.add up.
      @@ -5789,12 +5799,13 @@

      10.3 Conditional monad?

    • We could use guard – conditional probabilities!

        -
      • P (A|B) +
      • P(A|B)
          -
        • Compute what is needed for both A -and B.
          • -
        • Guard B.
          • -
        • Return A.
          • +
        • Compute what is needed for both A and B.
          • +
        • Guard B.
          • +
        • Return A.

    • For the exact distribution monad it turns out very easy – we just @@ -5818,10 +5829,10 @@

      10.3 Conditional q*.p | (x,p) <- a; (y,q) <- b x] let return a = [a, 1.] let mzero = []Measure equal 0 everywhere is OK. let mplus = List.append end include MP include MonadPlusOps (MP) let choose p a b =It isn’t -a w.p. p & -b w.p. (1 - p) since -a and b List.map (fun (e,w) -> e, p.w) -a @are not +a w.p. p & +b w.p. (1−p) +since a and b List.map (fun (e,w) -> e, +p.w) a @are not normalized!List.map (fun (e,w) -> e, (1. -.p).w) b let pick dist = dist

      let uniform elems = normalize (List.map (fun e->e,1.) elems) let @@ -5997,9 +6008,9 @@

      10.4 Burglary example:

    • module Burglary (P : CONDPROBAB) = struct open P type whathappened =
      Safe | Burgl | Earthq | Burglnearthq

      -

      let check \simjohncalled \simmarycalled \simradio = perform
      +

      let check ∼johncalled ∼marycalled ∼radio = perform
      earthquake <– flip 0.002; guard (radio = None || radio = Some earthquake); burglary <– flip 0.001; let alarmp = match burglary, earthquake with | false, false -> 0.001 | false, true -> 0.29 | @@ -6073,9 +6084,10 @@

      11 Lightweight cooperative library, parallel \concat{e}{\rsub{a}} \concat{e}{\rsub{b}} c is equivalent to

      -

      perform let a = e_{a} in let b = -e_{b} in x <– a; y <– b; c x -y

      +

      perform let a = ea in let b = +eb in x +<– a; y <– b; c x y

      • We will follow this model, with an imperative implementation.
      • In any case, do not call run or access @@ -7245,7 +7257,7 @@

        5.2 Algorithmic optimizations

        • (All times measured with profiling turned on.)

        • Optim0.ml asymptotic time complexity: \mathcal{O} (n^2), time: 22.53s.

          +class="math inline">𝒪(n2), time: 22.53s.

          • Garbage collection takes 6% of time.
              @@ -7257,7 +7269,7 @@

              5.2 Algorithmic optimizations

              Hashtbl.find h w in Hashtbl.replace h w (c+1); h with Notfound -> Hashtbl.add h w 1; hlet iterate f h = Hashtbl.iter f h

              Optim1.ml asymptotic time complexity: \mathcal{O} (n), time: 0.63s.

              +class="math inline">𝒪(n), time: 0.63s.

              • Garbage collection takes 17% of time.
              @@ -7266,7 +7278,7 @@

              5.2 Algorithmic optimizations

              let k,c,h = List.foldleft (fun (k,c,h) w -> if k = w then k, c+1, h else w, 1, ((k,c)::h)) (““, 0, []) words in (k,c)::h

              Optim2.ml asymptotic time complexity: \mathcal{O} (n \log n), time: 1s.

              +class="math inline">𝒪(nlogn), time: 1s.

              • Garbage collection takes 40% of time.
              @@ -7274,8 +7286,8 @@

              5.2 Algorithmic optimizations

              attempt it.

            • With algorithmic optimizations we should be concerned with asymptotic complexity in terms of the \mathcal{O} (\cdot) notation, but we will not -pursue complexity analysis in the remainder of the lecture.

              • +class="math inline">𝒪(⋅) notation, but we will not pursue +complexity analysis in the remainder of the lecture.

            5.3 Low-level optimizations

              @@ -7326,9 +7338,9 @@

              5.4 Comparison of
            • We perform a rough comparison of association lists, tree-based maps and hashtables. Sets would give the same results.
            • We always create hashtables with initial size 511.
              • -
            • 10^7 operations of: adding an -association (creation), finding a key that is in the map, finding a key -out of a small number of keys not in the map.
              • +
            • 107 operations of: +adding an association (creation), finding a key that is in the map, +finding a key out of a small number of keys not in the map.
            • First row gives sizes of maps. Time in seconds, to two significant digits.

            @@ -8230,8 +8242,8 @@

            6.1.1 Example: Finding email “EDU” | “org” | “ORG” | “com” | “COM”of address.rule email state = parse| newlineCheck state before moving on.{ report state lexbuf; nextline lexbuf; email Seek -lexbuf }\swarrowDetected possible start -of address.| (addrchar+ as name) atsepsymb (addrchar+ as addr) { email +lexbuf }↙Detected possible start of +address.| (addrchar+ as name) atsepsymb (addrchar+ as addr) { email (Addr (false, name, [addr])) lexbuf }

            domsepsymb (addrdom as dom)Detected possible finish of address. { let
            @@ -8339,21 +8351,21 @@

            6.2 Parsing with Menhir

            optimization)

            %token < int > INT%token PLUS TIMES%left PLUS%left TIMESMultiplication has higher priority.%%expression:| i = INT { i -}\swarrow Without inlining, would not +}↙ Without inlining, would not distinguish priorities.| e = expression; o = op; f = expression { o e f }%inline op:Inline operator – generate corresponding rules.| PLUS { ( + ) }| TIMES { ( * ) }

            • -

          • Menhir is an \operatorname{LR} -(1) parser generator, i.e. it fails for grammars where looking -one token ahead, together with precedences, is insufficient to determine -whether a rule applies.

            +

          • Menhir is an LR (1) parser +generator, i.e. it fails for grammars where looking one token ahead, +together with precedences, is insufficient to determine whether a rule +applies.

            • In particular, only unambiguous grammars.
            • -

          • Although \operatorname{LR} (1) -grammars are a small subset of context free grammars, the -semantic actions can depend on context: actions can be functions that -take some form of context as input.

            • +

          • Although LR (1) grammars are a +small subset of context free grammars, the semantic actions can +depend on context: actions can be functions that take some form of +context as input.

          • Positions are available in actions via keywords $startpos(x) and $endpos(x) where x is name given @@ -8386,7 +8398,7 @@

            6.2.1 Example: parsing number val ( + ): number -> number -> number val ( - ): number -> number -> number val ( ): number -> number -> number val ( / ): number -> number -> number val ( \sim-): number -> numberend>%start +class="math inline">∼-): number -> numberend>%start <Semantics.number> main%{ open Semantics %}

            %%main:| e = expr EOL { e }expr:| i = INT { inject i }| LPAREN e = expr RPAREN { e }| e1 = expr PLUS e2 = expr { e1 + e2 }| e1 = expr MINUS @@ -8395,8 +8407,8 @@

            6.2.1 Example: parsing

          • File calc.ml:

            module FloatSemantics = struct type number = float let inject = floatofint let ( + ) = ( +. ) let ( - ) = ( -. ) let ( * ) = ( *. ) let -( / ) = ( /. ) let (\sim- ) = (\sim-. )endmodule FloatParser = +( / ) = ( /. ) let (∼- ) = (∼-. )endmodule FloatParser = Parser.Make(FloatSemantics)

            let () = let stdinbuf = Lexing.fromchannel stdin in while true do let linebuf = Lexing.fromstring (Lexer.line stdinbuf) in try
            @@ -8672,10 +8684,10 @@

            4 Bruteforce

          • Pairs of words are much less frequent than single words so storing them means less work for postings lists merging.

          • Can result in much bigger index size: \min (W^2, N) where W is the number of distinct words and N the total number of words in -documents.

            • +class="math inline">min (W2,N) where +W is the number of distinct +words and N the total number +of words in documents.

          • Invocation that gives us stack backtraces:

            ocamlbuild InvIndex3.native -cflag -g -libs unix; export OCAMLRUNPARAM="b"; ./InvIndex3.native

          • Time: 2.4s – disappointing.

            • @@ -8822,12 +8834,12 @@

            1 Zippers

          type btree = Tip | Node of int * btree * btree
          -

          \begin{matrix} +

          $$ \begin{matrix} T & = & 1 + xT^2\\\\\\ \frac{\partial T}{\partial x} & = & 0 + T^2 + 2 xT \frac{\partial T}{\partial x} = TT + 2 xT \frac{\partial T}{\partial x} -\end{matrix}

          +\end{matrix} $$

          type btree_dir = LeftBranch | RightBranch
 type btree_deriv =
@@ -8840,7 +8852,7 @@ 
          1 Zippers
          
 bottom.
          
 
          The part closest to the location should be on top.

        • Revisiting equations for trees and lists:

          -

          \begin{matrix} +

          $$ \begin{matrix} T & = & 1 + xT^2\\\\\\ \frac{\partial T}{\partial x} & = & 0 + T^2 + 2 xT \frac{\partial @@ -8849,7 +8861,7 @@

          1 Zippers

          L (y) & = & 1 + yL (y)\\\\\\ L (y) & = & \frac{1}{1 - y}\\\\\\ \frac{\partial T}{\partial x} & = & T^2 L (2 xT) \end{matrix} -

          +$$

          I.e. the context can be stored as a list with the root as the last node.

            @@ -8902,14 +8914,15 @@

            1.1 Example: Context rewriting

            as we can, but changing the whole expression as little as possible.
          • We can illustrate our algorithm using mathematical notation. Let:
              -
            • x be the thing we pull out
              • -
            • C [e] and D [e] be big expressions with subexpression -e
              • -
            • operator \circ stand for one of: -\ast, +
              • +
            • x be the thing we pull +out
              • +
            • C[e] and D[e] be big expressions +with subexpression e
              • +
            • operator ∘ stand for one of: *,+
            - \begin{matrix} +$$ \begin{matrix} D [(C [x] \circ e_{1}) \circ e_{2}] & \Rightarrow & D [C [x] \circ (e_{1} \circ e_{2})]\\\\\\ @@ -8922,7 +8935,7 @@

            1.1 Example: Context rewriting

            e_{1} e_{2}]\\\\\\ D [e \circ C [x]] & \Rightarrow & D [C [x] \circ e] \end{matrix} -
            • +$$
          • First the groundwork:

          type op = Add | Multype expr = Val of int | Var of string | App of @@ -8943,15 +8956,14 @@

          1.1 Example: Context rewriting

        let rec pullout loc = match loc.ctx with | [] -> locDone.| (Leftarg, op, l) :: upctx ->D [e \circ C [x]] \Rightarrow D [C [x] \circ -e] pullout {loc with ctx=(Rightarg, op, l) :: upctx} | (Rightarg, -op1, e1) :: (, op2, e2) :: upctx when op1 = op2 ->D [(C [x] \circ e_{1}) \circ e_{2}] / D [e_{2} \circ -(C [x] \circ e_{1})] \Rightarrow D [C [x] \circ (e_{1} \circ -e_{2})] pullout {loc with ctx=(Rightarg, op1, App(e1,op1,e2)) :: -upctx} | (Rightarg, Add, e1) :: (, Mul, e2) :: upctx -> pullout {loc -with ctx=D [(C [x] + e_{1}) e_{2}] / D [e_{2} -(C [x] + e_{1})] \Rightarrow D [C [x] e_{2} + e_{1} e_{2}] +class="math inline">D[e∘C[x]] ⇒ D[C[x]∘e] +pullout {loc with ctx=(Rightarg, op, l) :: upctx} | (Rightarg, op1, e1) +:: (, op2, e2) :: upctx when op1 = op2 ->D[(C[x]∘e1)∘e2]/D[e2∘(C[x]∘e1)] ⇒ D[C[x]∘(e1∘e2)] +pullout {loc with ctx=(Rightarg, op1, App(e1,op1,e2)) :: upctx} | +(Rightarg, Add, e1) :: (, Mul, e2) :: upctx -> pullout {loc with +ctx=D[(C[x]+e1)e2]/D[e2(C[x]+e1)] ⇒ D[C[x]e2+e1e2] (Rightarg, Mul, e2) :: (Rightarg, Add, App(e1,Mul,e2)) :: upctx} | (Rightarg, op, r)::upctx ->Move up the context. pullout {sub=App(loc.sub, op, r); ctx=upctx}

        @@ -9076,11 +9088,11 @@

        2.1 Example using Froc

        display x y >>= fun -> r >>= display x y

      • let growat (x, depth, upd) = let xl = x-f2i -(width.(2.0(\sim-.(i2f +(width.(2.0(∼-.(i2f (depth+1))))) in let l, updl = changeable (Leaf (xl, (depth+1)20)) in
        let xr = x+f2i (width        .(2.0        (\sim-.(i2f (depth+1))))) in let r, updr = +class="math inline">∼-.(i2f (depth+1))))) in let r, updr = changeable (Leaf (xr, (depth+1)        20)) in write upd (Node (x, depth*20, l, r));Update the old leaf propagate ();and keep handles to make future updates. [xl, depth+1, updl; xr, depth+1, updr]

        • @@ -9245,8 +9257,10 @@

        3 Functional Reactive happens.

      • Turning behaviors and events from functions of time into input-output streams is similar to optimizing interesction of ordered -lists from O (mn) to O (m + n) time.

        • +lists from O(mn) to O(m+n) +time.

      • Now we can in turn define events in terms of behaviors:

        type ’a event = ’a option behavior

        although it betrays the discrete character of events (happening at @@ -9363,8 +9377,8 @@

        4 Reactivity by Stream sampling times.

        let integral fb = let rec loop t0 acc uts bs = let Cons ((,t1), uts) = Lazy.force uts in let Cons (b, bs) = Lazy.force bs in let acc = acc +. -(t1 -. t0) *. b inb =\operatorname{fb} -(t_{1}), \operatorname{acc} \approx \int_{t \leqslant t_{0}} f. +(t1 -. t0) *. b inb = fb (t1), acc  ≈ ∫t ≤ t0f. Cons (acc, lazy (loop t1 acc uts bs)) in memo1 (fun uts -> lazy ( let Cons ((,t), uts’) = Lazy.force uts in Cons (0., lazy (loop t 0. uts’ (fb $ uts)))))

        @@ -9398,7 +9412,7 @@

        1 The Paddle Game example

        ->
        fillrect (f2i tx+x) (f2i ty+y) w h | Circle (x, y, r) -> fillcircle (f2i tx+x) (f2i ty+y) r | Group scs -> List.iter (aux tx ty) -scs\swarrow Set color for +scs↙ Set color for sc objects.| Color (c, sc) -> setcolor c; aux tx ty sc | Translate (x, y, sc) -> aux (tx+.x) (ty+.y) sc in
        cleargraph ();‘‘Fast and clean’’ removing of previous picture. aux 0. 0. @@ -9452,10 +9466,10 @@

        1 The Paddle Game example

      • Unfortunately OCaml, being an eager language, does not let us encode recursive behaviors in elegant way. We need to unpack behaviors and events as functions of the input stream.
        • -
      • xbounce ->> (\sim-.) event is +
      • xbounce ->> (∼-.) event is just the negation function happening at each horizontal bounce.
      • stepaccum vel (xbounce ->> (\sim-.)) behavior is vel value +class="math inline">∼-.)) behavior is vel value changing sign at each horizontal bounce.
      • liftB intoffloat (integral xvel) +* width /* !*2 – first integrate velocity, then truncate it to integers and offset to the middle of the @@ -9467,19 +9481,19 @@

        1 The Paddle Game example

    let pbal vel = let rec xvel uts = stepaccum vel (xbounce ->> -(\sim-.)) $ uts and xvel = {memof = -xvel; memor = None} and xpos uts = (liftB intoffloat (integral xvel) +* -width /* !2) $ uts and xpos = {memof = xpos; memor = None} and -xbounce uts = whenB ((xpos > width -* !27) || (xpos -<* !27)) $ uts and xbounce = {memof = xbounce; memor = None} in -let rec yvel uts = (stepaccum vel (ybounce ->> (\sim-.))) $ uts and yvel = {memof = yvel; -memor = None} and ypos uts = (liftB intoffloat (integral yvel) + -height /* !2) $ uts and ypos = {memof = ypos; memor = None} and -ybounce uts = whenB ( (ypos > height -* !27) || ((ypos -<* !17) && (ypos >* !7) && (xpos ->* mousex) &&* (xpos <* mousex +* !*50))) $ uts and -ybounce = {memof = ybounce; memor = None} in liftB2 (fun x y -> Color +(∼-.)) $ uts and xvel = {memof = xvel; +memor = None} and xpos uts = (liftB intoffloat (integral xvel) +* width +/* !2) $ uts and xpos = {memof = xpos; memor = None} and xbounce uts += whenB ((xpos > width -* !27) || (xpos <* !27)) +$ uts and xbounce = {memof = xbounce; memor = None} in let rec yvel uts += (stepaccum vel (ybounce ->> (∼-.))) $ uts and yvel = {memof = yvel; memor += None} and ypos uts = (liftB intoffloat (integral yvel) + height +/* !2) $ uts and ypos = {memof = ypos; memor = None} and ybounce uts += whenB ( (ypos > height -* !27) || ((ypos <* +!17) && (ypos >* !7) && (xpos >* +mousex) &&* (xpos <* mousex +* !*50))) $ uts and ybounce = +{memof = ybounce; memor = None} in liftB2 (fun x y -> Color (Graphics.red, Circle (x, y, 6))) xpos ypos

    • Invocation:

      @@ -9683,10 +9697,10 @@

      6 Direct Control

    • We follow our (or Lwt) implementation of lightweight threads, adapting it to the need of cancelling flows.

      module F = Froctype ’a result =| Return of 'a\downarrowNotifications to cancel when -cancelled.| Sleep of (’a -> unit) list * F.cancel ref list| -Cancelled| Link of ’a stateand ’a state = {mutable state : ’a -result}type cancellable = unit state

      • +class="math inline">↓Notifications to cancel when cancelled.| +Sleep of (’a -> unit) list * F.cancel ref list| Cancelled| Link of ’a +stateand ’a state = {mutable state : ’a result}type cancellable = unit +state

    • Functions find, wakeup, connect are as in lecture 8 (but connecting to cancelled thread cancels the other thread).

      • @@ -9735,12 +9749,12 @@

      6 Direct Control

      (perform
      await mbuttonpressed;Start when button down. let opn = ref [] in
      repeat (perform mpos <– await mousemove;\swarrowAdd next position to line. emit (opn -:= mpos :: !opn; !opn :: !cld))
      -\simuntil:mbuttonreleased;\swarrowStart new shape. emit (cld := !opn :: -!cld; opn := []; [] :: !cld))let painter, cancelpainter = behaviorflow -[] painterlet () = reactimate painter

      +class="math inline">↙Add next position to line. emit (opn := mpos +:: !opn; !opn :: !cld))
      +∼until:mbuttonreleased;↙Start new shape. emit (cld := !opn :: !cld; +opn := []; [] :: !cld))let painter, cancelpainter = behaviorflow [] +painterlet () = reactimate painter

    1 Flows and state

    @@ -9790,15 +9804,14 @@

    7.1 Calculator Flow

    <– repeat
    (performEnter the digits of a number (on later turns d <– await digits;starting from the second digit) emit (now := 10. *. !now +. d; -!now)) \simuntil:ops;until operator -button is pressed.
    +!now)) ∼until:ops;until operator button +is pressed.
    emit (now := !f !now; f := op !now; !now); d <– -repeat\nwarrowCompute the -result and ‘‘store away’’ the operator.(perform op <– await ops; -return (f := op !now)) \simuntil:digits;The user can pick a -different operator. emit (now := d; !now))Reset the state to a new -number.let calce, cancelcalc = eventflow calcNotifies display +repeat↖Compute the result +and ‘‘store away’’ the operator.(perform op <– await ops; return (f +:= op !now)) ∼until:digits;The user can +pick a different operator. emit (now := d; !now))Reset the state to a +new number.let calce, cancelcalc = eventflow calcNotifies display update.

    7.2 Tk: LablTk

      @@ -9822,53 +9835,53 @@

      7.2 Tk: LablTk

      edit fields) are for entering info from keyboard.

      • Actions are callback functions passed as the \simcommand argument.
        • +class="math inline">∼command argument.

    • Frames in Tk group widgets.

    • The parent is sent as last argument, after optional labelled arguments.

      let top = Tk.openTk ()let btnframe = Frame.create \simrelief:’Groove \simborderwidth:2 toplet buttons = Array.map +class="math inline">∼relief:’Groove ∼borderwidth:2 toplet buttons = Array.map (Array.map (function | text, ’Dot -> Button.create \simtext \simcommand:(fun () -> F.send dot ()) +class="math inline">∼text ∼command:(fun () -> F.send dot ()) btnframe | text, ’Di d -> Button.create \simtext \simcommand:(fun () -> F.send digit d) +class="math inline">∼text ∼command:(fun () -> F.send digit d) btnframe | text, ’O f -> Button.create \simtext \simcommand:(fun () -> F.send op f) +class="math inline">∼text ∼command:(fun () -> F.send op f) btnframe)) layoutlet result = Label.create \simtext:“0” \simrelief:’Sunken top

      • +class="math inline">∼text:“0” ∼relief:’Sunken top

    • GUI toolkits have layout algorithms, so we only need to tell which widgets hang together and whether they should fill all available space etc. – via pack, or grid for “rectangular” organization.

      • -

    • \simfill: the allocated space in +

    • ∼fill: the allocated space in ‘X, ‘Y, ‘Both or -‘None axes;\simexpand: +‘None axes;∼expand: maximally how much space is allocated or only as needed.

      • -

    • \simanchor: allows to glue a -widget in particular direction (‘Center, ‘E, +

    • ∼anchor: allows to glue a widget +in particular direction (‘Center, ‘E, ‘Ne etc.)

    • The grid packing flexibility: \simcolumnspan and \simrowspan.

      • +class="math inline">∼columnspan and ∼rowspan.

    • configure functions accept the same arguments as create but change existing widgets.

    • let () = Wm.titleset top “Calculator”; Tk.pack [result] \simside:’Top \simfill:’X; Tk.pack [btnframe] \simside:’Bottom \simexpand:true;
      +class="math inline">∼side:’Top ∼fill:’X; Tk.pack [btnframe] ∼side:’Bottom ∼expand:true;
      Array.iteri (fun column ->Array.iteri (fun row button -> Tk.grid -\simcolumn \simrow [button])) buttons; Wm.geometryset -top “200x200”;
      +∼column ∼row [button])) buttons; Wm.geometryset top +“200x200”;
      F.notifye calce (fun now -> Label.configure \simtext:(stringoffloat now) result); +class="math inline">∼text:(stringoffloat now) result); Tk.mainLoop ()

    @@ -9884,33 +9897,33 @@

    7.3 GTk+: LablGTk

  • Our events are called signals in GTk+.
  • Registering a notification is called connecting a signal handler, e.g.button#connect#clicked \simcallback:hello which takes \sim {\nobreak}callback:(unit -> unit) and -returns GtkSignal.id. +class="math inline">∼callback:hello which takes $\sim {\nobreak}$callback:(unit -> unit) +and returns GtkSignal.id.
    • As with Froc notifications, multiple handlers can be attached.
  • GTk+ events are a subclass of signals related to more specific window events, e.g.window#event#connect#delete \simcallback:deleteevent
    • +class="math inline">∼callback:deleteevent
  • GTk+ event callbacks take more info: \simcallback:(event -> unit) for some type +class="math inline">∼callback:(event -> unit) for some type event.

  • Automatic layout (aka. packing) seems less sophisticated than in Tk:

    • only horizontal and vertical boxes,
      • -
    • therefore \simfill is binary and -\simanchor is replaced by \simfrom ‘START or +
    • therefore ∼fill is binary and ∼anchor is replaced by ∼from ‘START or ‘END.

  • Automatic grid layout is called table.

      -
    • \simfill and \simexpand take ‘X, +
    • ∼fill and ∼expand take ‘X, ‘Y, ‘BOTH, ‘NONE.

  • The coerce method casts the type of the object (in @@ -9923,46 +9936,45 @@

    7.3 GTk+: LablGTk

  • The model part of application doesn’t change.

  • Setup:

    let = GtkMain.Main.init ()let window = GWindow.window \simwidth:200 \simheight:200 \simtitle:“Calculator” ()let top = GPack.vbox -\simpacking:window#add ()let result = -GMisc.label \simtext:“0” \simpacking:top#add ()let btnframe = -GPack.table \simrows:(Array.length -layout) \simcolumns:(Array.length -layout.(0)) \simpacking:top#add -()

    • +class="math inline">∼width:200 ∼height:200 ∼title:“Calculator” ()let top = GPack.vbox +∼packing:window#add ()let result = +GMisc.label ∼text:“0” ∼packing:top#add ()let btnframe = GPack.table +∼rows:(Array.length layout) ∼columns:(Array.length layout.(0)) ∼packing:top#add ()

  • Button actions:

    let buttons = Array.map (Array.map (function | label, ’Dot -> let -b = GButton.button \simlabel () in let +b = GButton.button ∼label () in let = +b#connect#clicked
    +∼callback:(fun () -> F.send dot ()) +in b | label, ’Di d ->
    +let b = GButton.button ∼label () in let += b#connect#clicked
    +∼callback:(fun () -> F.send digit d) +in b | label, ’O f ->
    +let b = GButton.button ∼label () in let = b#connect#clicked
    -\simcallback:(fun () -> F.send dot -()) in b | label, ’Di d ->
    -let b = GButton.button \simlabel () in -let = b#connect#clicked
    -\simcallback:(fun () -> F.send digit -d) in b | label, ’O f ->
    -let b = GButton.button \simlabel () in -let = b#connect#clicked
    -\simcallback:(fun () -> F.send op f) -in b)) layout

    • +∼callback:(fun () -> F.send op f) in +b)) layout

  • Button layout, result notification, start application:

    let deleteevent = GMain.Main.quit (); falselet () = let = window#event#connect#delete \simcallback:deleteevent in Array.iteri (fun +class="math inline">∼callback:deleteevent in Array.iteri (fun column->Array.iteri (fun row button -> btnframe#attach \simleft:column \simtop:row \simfill:’BOTH \simexpand:’BOTH (button#coerce)) ) buttons; +class="math inline">∼left:column ∼top:row ∼fill:’BOTH ∼expand:’BOTH (button#coerce)) ) buttons; F.notifye calce (fun now -> result#setlabel (stringoffloat now)); window#show (); GMain.Main.main ()

  • Functional Programming

    • Zippers, Reactivity, GUIs

    Exercise 1: Introduce operators -, / into the context rewriting “pull out +class="math inline">−,/ into the context rewriting “pull out subexpression” example. Remember that they are not commutative.

    Exercise 2: Add to the paddle game example:

    @@ -10073,7 +10085,7 @@

    Chapter 11

    with new constructs:

    • lambda calculus: variables Var, \lambda-abstractions Abs, +class="math inline">λ-abstractions Abs, function applications App;
    • arithmetics: variables Var, constants Num, addition Add, multiplication Mult; …
      • @@ -10113,7 +10125,7 @@

      Chapter 11

      dedicated variant.let0.5emevalvar0.5emwrap0.5emsub0.5em(s0.5em:0.5emvar)0.5em=0.5em0.5emtry0.5emList.assoc0.5ems0.5emsub0.5emwith0.5emNotfound0.5em->0.5emwrap0.5emstype0.5em’a0.5emlambda0.5em=Here we define the sub-language of \lambda-expressions.0.5em0.5emVarL0.5emof0.5emvar0.5em|0.5emAbs0.5emof0.5emstring0.5em0.5em’a0.5em|0.5emApp0.5emof0.5em’a0.5em0.5em’aDuring +class="math inline">λ-expressions.0.5em0.5emVarL0.5emof0.5emvar0.5em|0.5emAbs0.5emof0.5emstring0.5em0.5em’a0.5em|0.5emApp0.5emof0.5em’a0.5em0.5em’aDuring evaluation, we need to freshen variables to avoid capturelet0.5emgensym0.5em=0.5emlet0.5emn0.5em=0.5emref0.5em00.5emin0.5emfun0.5em()0.5em->0.5emincr0.5emn;0.5em”“0.5emˆ0.5emstringofint0.5em!n(mistaking distinct variables with the same @@ -10135,10 +10147,10 @@

      Chapter 11

      ->0.5emwrap0.5em(App0.5em(l1’,0.5eml2’)))Wrap into the completed language.0.5em0.5em0.5emSome0.5em(Abs0.5em(s,0.5eml1))0.5em->0.5em0.5em0.5em0.5emlet0.5ems’0.5em=0.5emgensym0.5em()0.5eminRename variable to avoid capture (\alpha-equivalence).0.5em0.5em0.5em0.5emwrap0.5em(Abs0.5em(s’,0.5emevalrec0.5em((s,0.5emwrap0.5em(VarL0.5ems’))::subst)0.5eml1))0.5em0.5em0.5emNone0.5em->0.5emeFalling-through +class="math inline">α-equivalence).0.5em0.5em0.5em0.5emwrap0.5em(Abs0.5em(s’,0.5emevalrec0.5em((s,0.5emwrap0.5em(VarL0.5ems’))::subst)0.5eml1))0.5em0.5em0.5emNone0.5em->0.5emeFalling-through when not in the current sub-language.type0.5emlambdat0.5em=0.5emLambdat0.5emof0.5emlambdat0.5emlambdaDefining -\lambda-expressionsas the completed +λ-expressionsas the completed language,let0.5emrec0.5emeval10.5emsubst0.5em=and the corresponding eval function.0.5em0.5emevallambda0.5emeval10.5em0.5em0.5em0.5em(fun0.5eme0.5em->0.5emLambdat0.5eme)0.5em(fun0.5em(Lambdat0.5eme)0.5em->0.5emSome0.5eme)0.5emsubsttype0.5em’a0.5emexpr0.5em=The @@ -10153,7 +10165,7 @@

      Chapter 11

      arithmetic expressionsas the completed language,let0.5emrec0.5emeval20.5emsubst0.5em=aka. ‘‘tying the recursive knot’‘.0.5em0.5emevalexpr0.5emeval20.5em0.5em0.5em0.5em(fun0.5eme0.5em->0.5emExprt0.5eme)0.5em(fun0.5em(Exprt0.5eme)0.5em->0.5emSome0.5eme)0.5emsubsttype0.5em’a0.5emlexpr0.5em=The -language merging \lambda-expressions +language merging λ-expressions and arithmetic expressions,0.5em0.5emLambda0.5emof0.5em’a0.5emlambda0.5em0.5emExpr0.5emof0.5em’a0.5emexprcan also be used asa sub-language for further @@ -10168,10 +10180,9 @@

      Chapter 11

      • Exceptions have always formed an extensible variant type in OCaml, whose pattern matching is done using the try\ldotswith syntax. Since recently, new -extensible variant types can be defined. This augments the normal -function extensibility of FP with straightforward data -extensibility.
        • +class="math inline">…with syntax. Since recently, new extensible +variant types can be defined. This augments the normal function +extensibility of FP with straightforward data extensibility.
      • Non-solution penalty points:
        • Giving up exhaustivity checking, which is an important aspect of @@ -10295,12 +10306,12 @@

          Chapter 11

        type0.5emvarname0.5em=0.5emstringlet0.5emgensym0.5em=0.5emlet0.5emn0.5em=0.5emref0.5em00.5emin0.5emfun0.5em()0.5em->0.5emincr0.5emn;0.5em”“0.5em0.5emstringofint0.5em!nclass0.5emvirtual0.5em[’lang]0.5emevaluable0.5em=The abstract class for objects supporting the eval -method.object0.5emFor \lambda-calculus, -we need helper +method.object0.5emFor λ-calculus, we need helper functions:0.5em0.5emmethod0.5emvirtual0.5emeval0.5em:0.5em(varname0.5em0.5em’lang)0.5emlist0.5em->0.5em’lang0.5em0.5emmethod0.5emvirtual0.5emrename0.5em:0.5emvarname0.5em->0.5emvarname0.5em->0.5em'langrenaming of free variables,0.5em0.5emmethod0.5emapply0.5em(arg0.5em:0.5em’lang)\beta-reduction if possible (fallback +class="math inline">β-reduction if possible (fallback otherwise).0.5em0.5em0.5em0.5em(fallback0.5em:0.5emunit0.5em->0.5em’lang)0.5em(subst0.5em:0.5em(varname0.5em0.5em’lang)0.5emlist)0.5em=0.5em0.5em0.5em0.5emfallback0.5em()endclass0.5em[’lang]0.5emvar0.5em(v0.5em:0.5emvarname)0.5em=object0.5em(self)We name the current object self.0.5em0.5eminherit0.5em[’lang]0.5emevaluable0.5em0.5emval0.5emv0.5em=0.5emv0.5em0.5emmethod0.5emeval0.5emsubst0.5em=0.5em0.5em0.5em0.5emtry0.5emList.assoc0.5emv0.5emsubst0.5emwith0.5emNotfound0.5em->0.5emself0.5em0.5emmethod0.5emrename0.5emv10.5emv20.5em=Renaming @@ -10308,7 +10319,7 @@

        Chapter 11

        variable:0.5em0.5em0.5em0.5emif0.5emv0.5em=0.5emv10.5emthen0.5em{<0.5emv0.5em=0.5emv20.5em>}0.5emelse0.5emselfwe clone the current object putting the new name.endclass0.5em[’lang]0.5emabs0.5em(v0.5em:0.5emvarname)0.5em(body0.5em:0.5em’lang)0.5em=object0.5em(self)0.5em0.5eminherit0.5em[’lang]0.5emevaluable0.5em0.5emval0.5emv0.5em=0.5emv0.5em0.5emval0.5embody0.5em=0.5embody0.5em0.5emmethod0.5emeval0.5emsubst0.5em=We -do \alpha-conversion prior to +do α-conversion prior to evaluation.0.5em0.5em0.5em0.5emlet0.5emv’0.5em=0.5emgensym0.5em()0.5eminAlternatively, we could evaluate with0.5em0.5em0.5em0.5em{<0.5emv0.5em=0.5emv’;0.5embody0.5em=0.5em(body#rename0.5emv0.5emv’)#eval0.5emsubst0.5em>}substitution @@ -10319,7 +10330,7 @@

        Chapter 11

        v=v1.0.5em0.5em0.5em0.5emelse0.5em{<0.5embody0.5em=0.5embody#rename0.5emv10.5emv20.5em>}0.5em0.5emmethod0.5emapply0.5emargsubst0.5em=0.5em0.5em0.5em0.5embody#eval0.5em((v,0.5emarg)::subst)endclass0.5em[’lang]0.5emapp0.5em(f0.5em:0.5em’lang)0.5em(arg0.5em:0.5em’lang)0.5em=object0.5em(self)0.5em0.5eminherit0.5em[’lang]0.5emevaluable0.5em0.5emval0.5emf0.5em=0.5emf0.5em0.5emval0.5emarg0.5em=0.5emarg0.5em0.5emmethod0.5emeval0.5emsubst0.5em=We use apply to differentiate between f = abs0.5em0.5em0.5em0.5emlet0.5emarg’0.5em=0.5emarg#eval0.5emsubst0.5emin -(\beta-redexes) and +(β-redexes) and f ≠ abs.0.5em0.5em0.5em0.5emf#apply0.5emarg’0.5em(fun0.5em()0.5em->0.5em{<0.5emf0.5em=0.5emf#eval0.5emsubst;0.5emarg0.5em=0.5emarg’0.5em>})0.5emsubst0.5em0.5emmethod0.5emrename0.5emv10.5emv20.5em=Cloning the object ensures that it will be a subtype of 'lang0.5em0.5em0.5em0.5em{<0.5emf0.5em=0.5emf#rename0.5emv10.5emv2;0.5emarg0.5em=0.5emarg#rename0.5emv10.5emv20.5em>}rather @@ -10331,8 +10342,8 @@

        Chapter 11

        need0.5em0.5emmethod0.5emcompute0.5em:0.5emint0.5emoption0.5em=0.5emNone0.5em0.5ema heper method compute.endclass0.5em[’lang]0.5emvarc0.5emv0.5em=0.5emobjectTo -use \lambda-expressions together with -arithmetic +use λ-expressions together +with arithmetic expressions0.5em0.5eminherit0.5em[’lang]0.5emvar0.5emvwe need to upgrade them with the helper method.0.5em0.5eminherit0.5emcomputemixinendclass0.5em[’lang]0.5emabsc0.5emv0.5embody0.5em=0.5emobject0.5em0.5eminherit0.5em[’lang]0.5emabs0.5emv0.5embody0.5em0.5eminherit0.5emcomputemixinendclass0.5em[’lang]0.5emappc0.5emf0.5emarg0.5em=0.5emobject0.5em0.5eminherit0.5em[’lang]0.5emapp0.5emf0.5emarg0.5em0.5eminherit0.5emcomputemixinendclass0.5em[’lang]0.5emnum0.5em(i0.5em:0.5emint)0.5em=A @@ -10386,7 +10397,7 @@

        Chapter 11

        type.class0.5em[’visitor]0.5emabs0.5em(v0.5em:0.5emvarname)0.5em(body0.5em:0.5em’visitor0.5emvisitable)0.5em=object0.5em(self)0.5em0.5emmethod0.5emv0.5em=0.5emv0.5em0.5emmethod0.5embody0.5em=0.5embody0.5em0.5emmethod0.5emaccept0.5em:0.5em’visitor0.5em->0.5emunit0.5em=0.5em0.5em0.5em0.5emfun0.5emvisitor0.5em->0.5emvisitor#visitAbs0.5emselfendlet0.5emnewabs0.5emv0.5embody0.5em=0.5em(new0.5emabs0.5emv0.5embody0.5em:>0.5em’a0.5emvisitable)class0.5em[’visitor]0.5emapp0.5em(f0.5em:0.5em’visitor0.5emvisitable)0.5em(arg0.5em:0.5em’visitor0.5emvisitable)0.5em=object0.5em(self)0.5em0.5emmethod0.5emf0.5em=0.5emf0.5em0.5emmethod0.5emarg0.5em=0.5emarg0.5em0.5emmethod0.5emaccept0.5em:0.5em’visitor0.5em->0.5emunit0.5em=0.5em0.5em0.5em0.5emfun0.5emvisitor0.5em->0.5emvisitor#visitApp0.5emselfendlet0.5emnewapp0.5emf0.5emarg0.5em=0.5em(new0.5emapp0.5emf0.5emarg0.5em:>0.5em’a0.5emvisitable)class0.5emvirtual0.5em[’visitor]0.5emlambdavisit0.5em=This abstract class has two uses:objectit defines the visitors for the sub-langauge of \lambda-expressions,0.5em0.5emmethod0.5emvirtual0.5emvisitVar0.5em:0.5em’visitor0.5emvar0.5em->0.5emunitand +class="math inline">λ-expressions,0.5em0.5emmethod0.5emvirtual0.5emvisitVar0.5em:0.5em’visitor0.5emvar0.5em->0.5emunitand it will provide an early check0.5em0.5emmethod0.5emvirtual0.5emvisitAbs0.5em:0.5em’visitor0.5emabs0.5em->0.5emunitthat the visitor @@ -10415,7 +10426,7 @@

        Chapter 11

        use result as an accumulator.0.5em0.5eminherit0.5em[’visitor]0.5emlambdavisit0.5em0.5emmethod0.5emvisitVar0.5emvar0.5em=0.5em0.5em0.5em0.5emresult0.5em:=0.5emvar#v0.5em::0.5em!result0.5em0.5emmethod0.5emvisitAbs0.5emabs0.5em=0.5em0.5em0.5em0.5em(abs#body)#accept0.5emself;0.5em0.5em0.5em0.5emresult0.5em:=0.5emList.filter0.5em(fun0.5emv’0.5em->0.5emv’0.5em<>0.5emabs#v)0.5em!result0.5em0.5emmethod0.5emvisitApp0.5emapp0.5em=0.5em0.5em0.5em0.5emapp#arg#accept0.5emself;0.5emapp#f#accept0.5emselfendtype0.5emlambdavisitt0.5em=0.5emlambdavisitt0.5emlambdavisitVisitor for the language of \lambda-expressions.type0.5emlambdat0.5em=0.5emlambdavisitt0.5emvisitablelet0.5emeval10.5em(e0.5em:0.5emlambdat)0.5emsubst0.5em:0.5emlambdat0.5em=0.5em0.5emlet0.5emresult0.5em=0.5emref0.5em(newvar0.5em”“)0.5eminThis +class="math inline">λ-expressions.type0.5emlambdat0.5em=0.5emlambdavisitt0.5emvisitablelet0.5emeval10.5em(e0.5em:0.5emlambdat)0.5emsubst0.5em:0.5emlambdat0.5em=0.5em0.5emlet0.5emresult0.5em=0.5emref0.5em(newvar0.5em”“)0.5eminThis initial value will be ignored.0.5em0.5eme#accept0.5em(new0.5emevallambda0.5emsubst0.5emresult0.5em:>0.5emlambdavisitt);0.5em0.5em!resultlet0.5emfreevars10.5em(e0.5em:0.5emlambdat)0.5em=0.5em0.5emlet0.5emresult0.5em=0.5emref0.5em[]0.5eminInitial value of the @@ -10440,7 +10451,7 @@

        Chapter 11

        branches’’.object0.5em0.5eminherit0.5em[’visitor]0.5emevalexpr0.5emresult0.5em0.5eminherit0.5em[’visitor]0.5emevallambda0.5emsubst0.5emresultendclass0.5em[’visitor]0.5emfreevarslexpr0.5emresult0.5em=object0.5em0.5eminherit0.5em[’visitor]0.5emfreevarsexpr0.5emresult0.5em0.5eminherit0.5em[’visitor]0.5emfreevarslambda0.5emresultendtype0.5emlexprvisitt0.5em=0.5emlexprvisitt0.5emlexprvisitThe language combiningtype0.5emlexprt0.5em=0.5emlexprvisitt0.5emvisitable\lambda-expressions and arithmetic +class="math inline">λ-expressions and arithmetic expressions.let0.5emeval30.5em(e0.5em:0.5emlexprt)0.5emsubst0.5em:0.5emlexprt0.5em=0.5em0.5emlet0.5emresult0.5em=0.5emref0.5em(newnum0.5em0)0.5emin0.5em0.5eme#accept0.5em(new0.5emevallexpr0.5emsubst0.5emresult);0.5em0.5em!resultlet0.5emfreevars30.5em(e0.5em:0.5emlexprt)0.5em=0.5em0.5emlet0.5emresult0.5em=0.5emref0.5em[]0.5emin0.5em0.5eme#accept0.5em(new0.5emfreevarslexpr0.5emresult);0.5em0.5em!resultlet0.5emtest30.5em=0.5em0.5em(newadd0.5em(newmult0.5em(newnum0.5em3)0.5em(newvar0.5em”x”))0.5em(newnum0.5em1)0.5em:>0.5emlexprt)let0.5emetest0.5em=0.5emeval30.5emtest30.5em[]let0.5emfvtest0.5em=0.5emfreevars30.5emtest3let0.5emoldetest0.5em=0.5emeval30.5em(test20.5em:>0.5emlexprt)0.5em[]let0.5emoldfvtest0.5em=0.5emeval30.5em(test20.5em:>0.5emlexprt)0.5em[]Polymorphic Variant Types: Subtyping

          @@ -10473,9 +10484,9 @@

          Chapter 11

          • The need to “tie the recursive knot” separately both at the type level and the function level. At the function level, an \eta-expansion is required due to value -recursion problem. At the type level, the type variable can be -confusing.
            • +class="math inline">η-expansion is required due to +value recursion problem. At the type level, the type variable +can be confusing.
          • There can be a slight time cost compared to the visitor pattern-based approach: additional dispatch at each level of type aggregation (i.e.  merging sub-languages).
            • @@ -10531,21 +10542,24 @@

            Chapter 11

            composing definitions of smaller languages. For example, the combinators of the Extended Backus-Naur Form notation are:

              -
            • concatenation: S = A, B stands for -S = \lbrace a b|a \in A, b \in b -\rbrace,
              • -
            • alternation: S = A|B stands for -S = \lbrace a|a \in A \vee a \in B -\rbrace,
              • -
            • option: S = [A] stands for S = \lbrace \epsilon \rbrace \cup A, where -\epsilon is an empty string,
              • -
            • repetition: S = \lbrace A \rbrace -stands for S = \lbrace \epsilon \rbrace \cup -\lbrace a s|a \in A, s \in S \rbrace,
              • -
            • terminal string: S ='' -a'' stands for S = \lbrace a -\rbrace.
              • +
            • concatenation: S = A, B stands +for S = {ab|a ∈ A, b ∈ b},
              • +
            • alternation: S = A|B stands for +S = {a|a ∈ A ∨ a ∈ B},
              • +
            • option: S = [A] +stands for S = {ϵ} ∪ A, where +ϵ is an empty string,
              • +
            • repetition: S = {A} stands for S = {ϵ} ∪ {as|a ∈ A, s ∈ S},
              • +
            • terminal string: S = ″a″ stands for S = {a}.

          • Parsers implemented directly in a functional programming paradigm are functions from character streams to the parsed values. @@ -10563,13 +10577,13 @@

            Chapter 11

          • Return: val return : 'a -> 'a parser

            • return x parses an empty string, symbolically S = \lbrace \epsilon \rbrace, and returns +class="math inline">S = {ϵ}, and returns x.

          • MZero: val fail : 'a parser

            • fail fails to parse anything, symbolically S = \varnothing = \lbrace \rbrace.
              • +class="math inline">S = ⌀ = {}.

          • MPlus: either val <|> : 'a parser -> 'a parser -> 'a parser,

            @@ -10597,10 +10611,12 @@

            Chapter 11

            consuming any character can be entered when a parse failure should occur, the cycle will keep repeating.

              -
            • For example, if we define numbers N := D | -N D, where D stands for digits, -then a stack of uses of the rule N \rightarrow -N D will build up when the next character is not a digit.
              • +
            • For example, if we define numbers N := D|ND, +where D stands for digits, +then a stack of uses of the rule N → ND will build +up when the next character is not a digit.
            • On the other hand, rules can share common prefixes.Parser Combinators: Implementation
            • @@ -10687,19 +10703,21 @@

            Chapter 11

          • File Plugin1.ml:

          open0.5emPluginBase.ParseMlet0.5emdigitofchar0.5emd0.5em=0.5emintofchar0.5emd0.5em-0.5emintofchar0.5em’0’let0.5emnumber=0.5em0.5emlet0.5emrec0.5emnum0.5em=Numbers: -N := D N | D where D is +N := DN|D +where D is digits.0.5em0.5em0.5em0.5emlazy0.5em(0.5em0.5em(perform0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5emd0.5em<–0.5emdigit;0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em(n,0.5emb)0.5em<–0.5emLazy.force0.5emnum;0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5em0.5emreturn0.5em(digitofchar0.5emd0.5em0.5emb0.5em+0.5emn,0.5emb0.5em0.5em10))0.5em0.5em0.5em0.5em0.5em0.5em<>0.5emlazy0.5em(digit0.5em>>=0.5em(fun0.5emd0.5em->0.5emreturn0.5em(digitofchar0.5emd,0.5em10))))0.5emin0.5em0.5emLazy.force0.5emnum0.5em>>0.5emfstlet0.5emaddition0.5emlang0.5em=Addition -rule: S \rightarrow (S + -S).0.5em0.5emperformRequiring a parenthesis ( turns the rule into +rule: S → (S+S).0.5em0.5emperformRequiring +a parenthesis ( turns the rule into non-left-recursive.0.5em0.5em0.5em0.5emliteral0.5em”(“;0.5emn10.5em<–0.5emlang;0.5emliteral0.5em”+“;0.5emn20.5em<–0.5emlang;0.5emliteral0.5em”)“;0.5em0.5em0.5em0.5emreturn0.5em(n10.5em+0.5emn2)let0.5em()0.5em= PluginBase.(grammarrules0.5em:=0.5emnumber0.5em::0.5emaddition0.5em::0.5em!grammarrules)

          • File Plugin2.ml:

          open0.5emPluginBase.ParseMlet0.5emmultiplication0.5emlang0.5em=0.5em0.5emperformMultiplication -rule: S \rightarrow (S \ast -S).0.5em0.5em0.5em0.5emliteral0.5em”(“;0.5emn10.5em<–0.5emlang;0.5emliteral0.5em”“;0.5emn20.5em<–0.5emlang;0.5emliteral0.5em”)“;0.5em0.5em0.5em0.5emreturn0.5em(n10.5em0.5emn2)let0.5em()0.5em= +rule: S → (S*S).0.5em0.5em0.5em0.5emliteral0.5em”(“;0.5emn10.5em<–0.5emlang;0.5emliteral0.5em”“;0.5emn20.5em<–0.5emlang;0.5emliteral0.5em”)“;0.5em0.5em0.5em0.5emreturn0.5em(n10.5em0.5emn2)let0.5em()0.5em= PluginBase.(grammarrules0.5em:=0.5emmultiplication0.5em::0.5em!grammarrules) Functional ProgrammingŁukasz Stafiniak

          The Expression Problem

          @@ -10761,7 +10779,7 @@

          Chapter 11

          Exercise 10: Streamline the solution PolyRecM.ml by extending the language of \lambda-expressions with arithmetic +class="math inline">λ-expressions with arithmetic expressions, rather than defining the sub-languages separately and then merging them. See slide on page 15 of Jacques Garrigue Structural Types, Recursive Modules, and the Expression Problem.

          @@ -10857,31 +10875,35 @@

          Exam set 1

          lists or trees).

          Exercise 11: (Purple.) One way to express constraints on a polymorphic function is to write its type in the form: -\forall \alpha _{1} \ldots \alpha _{n} [C] . -\tau, where \tau is the type of -the function, \alpha _{1} \ldots \alpha -_{n} are the polymorphic type variables, and C are additional constraints that the -variables \alpha _{1} \ldots \alpha -_{n} have to meet. Let’s say we allow “local variables” in C: for example C = -\exists \beta . \alpha _{1} \dot{=} \operatorname{list} (\beta). -Why the general form \forall \beta [C] . -\beta is enough to express all types of the general form \forall \alpha _{1} \ldots \alpha _{n} [C] . -\tau?

          +∀α1…αn[C].τ, +where τ is the type of the +function, α1…αn +are the polymorphic type variables, and C are additional constraints that +the variables α1…αn +have to meet. Let’s say we allow “local variables” in C: for example $C = \exists \beta . \alpha _{1} \dot{=} +\operatorname{list} (\beta)$. Why the general form ∀β[C].β is enough +to express all types of the general form ∀α1…αn[C].τ?

          Exercise 12: (Purple.) Define a type that corresponds to a set with a googleplex of elements (i.e. 10^{10^{100}} elements).

          +class="math inline">1010100 elements).

          Exercise 13: (Red.) In a height-balanced binary tree, the following property holds for every node: The height of its left subtree and the height of its right subtree are almost equal, which means their difference is not greater than one. Consider a height-balanced binary tree of height h. What is the maximum number of nodes it can -contain? Clearly, \operatorname{maxN}= 2 h - -1. However, finding the minimum number \operatorname{minN} is more difficult.

          +class="math inline">h. What is the maximum number of +nodes it can contain? Clearly, maxN  = 2h − 1. However, finding the +minimum number minN  is more +difficult.

          Construct all the height-balanced binary trees with a given nuber of nodes. hbal_tree_nodes n returns a list of all height-balanced binary tree with n nodes.

          @@ -10967,10 +10989,12 @@

          Exam set 1

          fold_left in terms of fold_right. Hint: continuation passing style.

          Exercise 11: (Purple.) Show why for a monomorphic -specification, if datastructures d_{1} -and d_{2} have the same behavior under -all operations, then they have the same representation d_{1} = d_{2} in all implementations.

          +specification, if datastructures d1 and d2 have the same behavior +under all operations, then they have the same representation d1 = d2 +in all implementations.

          Exercise 12: (Purple.) append for lazy lists returns in constant time. Where has its linear-time complexity gone? Explain how you would account for this in a time complexity @@ -11032,16 +11056,18 @@

          Exam set 3

          elements. The required sizes of subsets are given as a list of numbers.

          Exercise 6: (Yellow.) A complete binary tree with -height H is defined as follows: The -levels 1, 2, 3, \ldots, H - 1 contain -the maximum number of nodes (i.e 2^{i - -1} at the level i, note that we -start counting the levels from 1 at the -root). In level H, which may contain -less than the maximum possible number of nodes, all the nodes are -“left-adjusted”. This means that in a levelorder tree traversal all -internal nodes come first, the leaves come second, and empty successors -(the nil’s which are not really nodes!) come last.

          +height H is defined as +follows: The levels 1, 2, 3, …, H − 1 contain the +maximum number of nodes (i.e 2i − 1 at the level i, note that we start counting the +levels from 1 at the root). In level +H, which may contain less than +the maximum possible number of nodes, all the nodes are “left-adjusted”. +This means that in a levelorder tree traversal all internal nodes come +first, the leaves come second, and empty successors (the nil’s which are +not really nodes!) come last.

          We can assign an address number to each node in a complete binary tree by enumerating the nodes in levelorder, starting at the root with number 1. In doing so, we realize that for every node X with address A @@ -11081,9 +11107,11 @@

          Exam set 3

          Exercise 10: (Orange.) Write a function that transposes a rectangular matrix represented as a list of lists.

          Exercise 11: (Purple.) Find the bijective functions -between the types corresponding to a (a^b + -c) and a^{b + 1} + ac (in -OCaml).

          +between the types corresponding to a(ab+c) +and ab + 1 + ac +(in OCaml).

          Exercise 12: (Purple.) Show the monad-plus laws for OptionM monad.

          Exercise 13: (Red.) As a preparation for drawing the @@ -11144,9 +11172,9 @@

          Exam set 3

          left child is at least as large as the rank of its right sibling. The rank of a node is defined to be the length of its right spine, i.e. the rightmost path from the node in question to an empty node. -Implement O (\log n) worst case time -complexity Priority Queues based on leftist heaps. Each node of the tree -should contain its rank.

          +Implement O(logn) +worst case time complexity Priority Queues based on leftist heaps. Each +node of the tree should contain its rank.

          Note that the elements along any path through a heap-ordered tree are stored in sorted order. The key insight behind leftist heaps is that two heaps can be merged by merging their right spines as you would merge