Functional Programming & Proofs
back
Other collections with illustration
- Marks management with Sets and Maps
let s1 = set ["john";"kate";"bill"];;
let s2 = set ["kate";"sam";"amy"];;
let (&&), (||) = Set.intersect, Set.union;; // overloadind
s1 && s2, s1 || s2;;
let marks1 = Map [("bill",12);("amy",18);("john",15);("kate",16)];;
marks1 |> Map.find "bill";;
marks1 |> Map.values |> Seq.sort;;
let marks2 = Map [("bill",15);("amy",11);("john",5);("kate",19)];;
let marks n =
let m1 = marks1 |> Map.find n |> fun m ->("PF",m)
let m2 = marks2 |> Map.find n |> fun m ->("UML",m)
[m1;m2];;
marks "bill"
- Sets are similar to lists except they don't have duplicate elements and ordering is omitted. They have other operators such as union, intersection, difference, etc.
- Maps are sets of pairs (key,value) and can encode a function by the way of data that can be changed.
As an exercise, how to define the functions used in the preceding examples ?
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide
docteur dr laurent thiry uha mulhouse france functional programming fsharp proof theory coq coqide