commit 7d38e9e1686d610201799505fcf506e6f4f289ea
parent 098e731afa4bd512cf09ad7358204a0d26e6e118
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Thu, 28 Dec 2023 13:21:17 -0800
Add tsils
Motivation in comment.
Diffstat:
| A | tsil.ml | | | 35 | +++++++++++++++++++++++++++++++++++ |
1 file changed, 35 insertions(+), 0 deletions(-)
diff --git a/tsil.ml b/tsil.ml
@@ -0,0 +1,35 @@
+(* A tsil is a backwards list (i.e., tail to left and head to right). In
+ * dependent type systems, telescopes/contexts are essentially tsils, because
+ * later variables can depend on earlier variables. Thus, we sometimes use
+ * tsils instead of lists to aid readability. Moreover, one can view lists as
+ * reversed tsils and vice versa (and this module provides functions in service
+ * of this viewpoint), so disciplined use of tsils and lists can help prevent
+ * accidental telescope/context reversal via static checks in OCaml. That is,
+ * if a tsil is a context and a list is a reversed context, then it is
+ * impossible to accidentally reverse a context, because that would amount to
+ * an OCaml type error. *)
+
+type 'a t = Nil | Snoc of 'a t * 'a
+
+(* Miraculously, (<@) is left associative and (@>) is right associative, as
+ * one would expect. *)
+
+let rec (<@) l r = match r with
+| x :: r -> Snoc (l, x) <@ r
+| [] -> l
+let appendl = (<@)
+
+let rec (@>) l r = match l with
+| Snoc (l, x) -> l @> (x :: r)
+| Nil -> r
+let appendr = (@>)
+
+let of_list r = Nil <@ r
+
+let to_list l = l @> []
+
+module Global = struct
+ type 'a tsil = 'a t = Nil | Snoc of 'a tsil * 'a
+ let (<@) = (<@)
+ let (@>) = (@>)
+end
