From 4651edb462a048b3c7645f5eebef3703bc57b97e Mon Sep 17 00:00:00 2001
From: Vesa Karvonen <vesa.a.j.k@gmail.com>
Date: Sun, 12 Jul 2020 11:15:35 +0300
Subject: [PATCH] Add functional trie example

---
 examples/trie.1ml | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)
 create mode 100644 examples/trie.1ml

diff --git a/examples/trie.1ml b/examples/trie.1ml
new file mode 100644
index 00000000..acae5c2e
--- /dev/null
+++ b/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}
+    }
+}