Lecture 2.1 - Structural Induction on Trees (optional)

Generalize the structural induction on list to general structures like trees.

To prove a property P(t) for all trees t:
* show for any leave l, P(l) holds
* for each internal node t with subtrees s1...sn, show P(s1)&...&P …

Intro

ML lang family

statically strongly typed languages

  • fisrt-class functions
  • type inference
  • pattern matching

highlights of ocaml

  • safty: static typing, pattern matching
  • efficiency: high performance
  • expressiveness: functional+type inference+polymorphism

  • package manager: opam

  • debugger
  • profiler
  • REPL: "toplevel"
  • bytecode compiler: ccamlc
  • native compiler: ocamlopt

programming environment fully online: https://try.ocamlpro …

Recap: Functions and Pattern Matching

case classes

ex: json json objects can be seq, num, str, bool,...

⇒ represented as abstract class and case classes.

pattern matching

→ question: what is the type of the {case(key, value)=>"..."} clause?

it is (JBinding => String) type, which is a shorthand for Function1[JBinding, String …