Library FingerTree.FingerTreeModule
FingerTree: a non-dependent interface
As shown before, we can wrap the measure and the tree in a dependent pair to offer a simpler interface to Finger Trees.
Module FingerTree(M : Monoid) (Ms : Measured with Module Mon := M).
Module FT := DependentFingerTree M.
Definition v := M.m.
Definition finger_tree :=
{ m : v & fingertree measure m }.
Notation " ts :| t " := (existT _ ts t) (at level 20).
This gives us a type finger_tree v mono A measure, which can be compared with
the original finger_tree v a datatype in Haskell. It adds the monoid implementation
and measure function as explicit parameters whereas in Haskell they are passed implicitely
using the typeclass mechanism. Morally, the parameterization we did using the section
mechanism correspond to the systematic prefixing of functions on FingerTree objects by a
Measured v a constraint in Haskell (Measured v a is a class with a single function
measure of type a → v where v must have a Monoid instance). We
think this equivalence indicates an interesting field of investigations
on how to integrate overloading in a language like Russell, or a section system in Haskell.
We do not describe the wrapping in detail, it is just destructuring a finger_tree object, calling the appropriate function on fingertrees and packing back the measure and the tree. However, an important point is that we can wrap views too and obviously recover the associated measure:
Inductive left_view : Type :=
| nil_left : left_view | cons_left : A → finger_tree → left_view.
Lemma view_left_size : ∀ t x t', view_left t = cons_left x t' →
tree_size t' < tree_size t.
We can finally wrap splitting
on finger_trees along a predicate. We offer the same
simply-typed interface as Haskell by definining the function split_with p x.
It splits any tree x by first checking if x is empty and if
not calls the split function on it using the predicate p with an empty accumulator.
Program Definition split_with (p : v → bool)
(x : finger_tree) : finger_tree × finger_tree :=
if is_empty_dec x then (empty, empty)
else let (l, x, r) := split p epsilon x in (l, cons x r).
End FingerTree.