Add functional trie example

examples/trie.1ml

@@ -0,0 +1,30 @@
+local import "prelude"
+
+FunctionalTrie = {
+  local
+    type I (type t _ _) = {
+      type case _ _
+      unit 'v         : opt v            ~> case {} v
+      alt  'v 'k1 'k2 : t k1 v ~> t k2 v ~> case (alt k1 k2) v
+      pair 'v 'k1 'k2 : t k1 (t k2 v)    ~> case (k1, k2) v
+    }
+    type T (type t _ _) k v = (m: I t) ~> m.case k v
+    ...rec {type t _ _} => {type t k v = wrap T t k v}
+    T = T t
+    I = I t
+    mk (fn: T _ _) = fn :# wrap T _ _ :@ t _ _
+
+  t
+  case (m: I) (e :# wrap T _ _ :@ t _ _) = e m
+  unit vO : t _ _ = mk fun (m: I) => m.unit vO
+  alt l r : t _ _ = mk fun (m: I) => m.alt l r
+  pair lr : t _ _ = mk fun (m: I) => m.pair lr
+
+  lookup = rec (lookup 'k 'v: t k v ~> k ~> opt v) =>
+    case {
+      type case k v = k ~> opt v
+      unit m {} = m
+      alt ta tb = Alt.case {inl = lookup ta, inr = lookup tb}
+      pair ta (a, b) = lookup ta a |> Opt.case {none, some tb = lookup tb b}
+    }
+}