add ats post

posts/2022-09-16-ats.md

@@ -0,0 +1,436 @@
+---
+title: a little ats program
+date: 2022-09-16
+tags: [computer, ATS, cool languages]
+show-toc: true
+...
+
+[ats] is a language that is a little infamous among type system likers, for its
+complexity, its weird syntax, and its thin documentation. well i won't be beat,
+so here's a little implementation of simply-typed lambda calculus. right now it
+doesn't actually use many ats-specific features, since i just didn't end up
+needing them.
+
+[ats]: http://www.ats-lang.org
+
+it does leak memory without gc though, so maybe i should have.
+oh well one thing at a time
+
+# installation, et cetera
+
+instead of trying to install ats myself, i just used [nix], since i already
+have it installed as the least annoying package manager for idris. i just run
+`nix shell nixpkgs#ats2` and i'm in a shell with `patscc` and `patsopt`
+available. if you want to try building it yourself, that's, uh, your choice.
+
+[nix]: https://nixos.org
+
+to compile the program, i wrote a makefile. just a small one!
+
+```makefile
+ATSCC := patscc
+ATSFLAGS := \
+  -DATS_MEMALLOC_GCBDW -lgc \
+  -atsccomp \
+    'gcc -I$${PATSHOME} -I$${PATSHOME}/ccomp/runtime \
+         -L$${PATSHOME}/ccomp/atslib/lib -std=gnu99'
+
+%: %.dats
+	$(ATSCC) $< $(ATSFLAGS) -o $@
+```
+
+(in some installs the compiler is just called `atscc` for some reason.)
+
+the first line of `ATSFLAGS` tells it which allocator to use. in this case,
+`libgc`. the rest tells it to use `-std=gnu99`, so that it can find `alloca()`;
+the rest is the same as the default.
+
+one last thing. the first two lines of the program  have to be this. i didn't
+look into it too hard but they seem to define... something... and if you forget
+to include them the c output by ats isn't even syntactically correct. ouch.
+
+```ats
+#include "share/atspre_define.hats"
+#include "share/atspre_staload.hats"
+```
+
+# types
+
+let's start by defining the syntax for types. it's going to be a single base
+type, and functions.
+
+$$
+\newcommand\Typ{\mathit{typ}}
+\newcommand\OR{\mathrel|}
+\Typ ::= \bullet \OR \Typ_1 \to \Typ_2
+$$
+
+so obviously, my first attempt was to just write this:
+
+```ats
+datatype typ = Base | Arr of (typ, typ)
+```
+
+i'm going to need to check two types for equality, so let's do that next.
+
+```ats
+fun eq_typ (a : typ, b : typ) .<a>. :<> bool =
+case (a, b) of
+| (Base(),      Base())      => true
+| (Arr(a1, a2), Arr(b1, b2)) => eq_typ(a1, b1) && eq_typ(a2, b2)
+| (_,           _)           => false
+```
+
+alas: (it is talking about the `.<a>.`)
+
+```
+/home/niss/ats/lam.dats: 149(line=7, offs=33) -- 150(line=7, offs=34):
+  error(2): the static identifier [a] is unrecognized.
+```
+
+surprise! as far as i can tell ats only allows termination checking to be
+based on _static_ (compile time) information. so i need to index the
+datatype with, uh, something. when we define functions on syntax like this,
+they basically always recurse on a subterm. so the height of the syntax tree
+will do. what i _actually_ have are these more messy definitions.
+
+```ats
+datatype typ(int) =
+|                Base(1)
+| {h1, h2 : nat} Arr(1 + max(h1, h2)) of (typ(h1), typ(h2))
+
+typedef typ = [h : nat] typ(h)
+```
+
+the base type $\bullet$ has height 1, and an arrow type has a height one more
+than the max height of its subterms. `nat` is a version of `int` constrained to
+be at least zero, rather than a separate type, so that's why it says `int` one
+place and `nat` the other. the typechecker has a linear arithmetic solver for
+reasoning about inequalities and expressions like `1 + max(h1, h2)`.
+
+i don't want to be talking about "types of height $h$" unless i really have to,
+though, so there's a definition for just _a_ type too. the syntax `[x : t1] t2`
+is an existential type that is automatically wrapped and unwrapped, so in this
+case it is a `typ(h)` for some, unknown, `h`. also, names can be overloaded by
+their arity so `typ(h)` and `typ` can both be defined in the same scope.
+
+so now `eq_typ` has to have a more intricate type to talk about height. the
+definition is still the same though.
+
+```ats
+fun eq_typ {ha : nat} .<ha>. (a : typ(ha), b : typ) :<> bool =
+case (a, b) of
+| (Base(),      Base())      => true
+| (Arr(a1, a2), Arr(b1, b2)) => eq_typ(a1, b1) && eq_typ(a2, b2)
+| (_,           _)           => false
+
+overload = with eq_typ
+```
+
+since i only actually need to care about one of the arguments' height for the
+termination proof, the other can still just be a `typ`. the last line lets me
+write `a = b` instead of `eq_typ(a, b)`, which is nice.
+
+next, i want to be able to print types. ideally this would be a function that
+returns a string, but string stuff involves pointer weirdness i haven't worked
+out yet. so it just prints. the only two precedence levels in these types are
+"left of an arrow" and "not left of an arrow", so that can just be a `bool`.
+unfortunately `print` has no information about its termination behaviour so
+there's no point bothering with that stuff here either. :confused:
+
+```ats
+fun print_typ (parens : bool, t : typ) : void =
+case t of
+| Base()    => print "•"
+| Arr(a, b) => begin
+    if parens then print("(");
+    print_typ(true, a);
+    print(" → ");
+    print_typ(false, b);
+    if parens then print(")");
+  end
+
+fn print_typ (t : typ) : void = print_typ(false, t)
+overload print with print_typ
+```
+
+# terms
+
+types are done, now let's move on to terms. we just want names, lambdas, and
+application.
+
+$$
+\newcommand\Term{\mathit{term}}
+\newcommand\Var{\mathit{var}}
+\Term ::= \Var \OR \lambda \Var : \Typ. \Term \OR \Term_1 \; \Term_2
+$$
+
+for the same reason as before, terms are indexed by their height, but _also_ by
+the number of variables in scope, since i want de bruijn indices to be
+intrinsically well-scoped. why even have a type system otherwise. so a
+`term(n, h)` has $n$ variables and height $h$.
+
+```ats
+datatype term(int, int) =
+| {n, i : nat | i < n} Var(n, 1) of int(i)
+| {n, h : nat}         Lam(n, 1 + h) of (typ, term(1 + n, h))
+| {n, h1, h2 : nat}    App(n, 1 + max(h1, h2)) of (term(n, h1), term(n, h2))
+
+typedef term(n : int) = [h : nat] term(n, h)
+```
+
+a variable is [a de bruijn index][db], which is a natural less than `n`. to
+express this we need to bridge the static world, where `n` lives, and the
+dynamic, where `Var`'s field lives. to do this i use a singleton type
+`int(i)`, whose only value is `i` itself. with this type, you can constraint the
+static `i`, and in turn the value of the field.
+
+[db]: https://en.wikipedia.org/wiki/De_Bruijn_index
+
+
+# contexts
+
+```ats
+typedef ctx(n: int) = list(typ, n)
+```
+
+a typing context is just a list of types of the appropriate length. since
+there's no binding in types here, that's all we need.
+
+looking up into a context is just list lookup, with some constraints to make it
+work.
+
+```ats
+fun lookup {n, i : nat | i < n} .<n>. (g : ctx(n), i : nat(i)) :<> typ =
+let val+ list_cons(x, g) = g in
+  if i = 0 then x else lookup(g, i - 1)
+end
+```
+
+from the constraints $n \ge 0, i \ge 0, i < n$, the compiler can see that, as
+$n \ge 1$, the list is nonempty and `list_cons` _is_ the only case. it can also
+propagate the $i \ne 0$ condition from the `else` to see the recursive call is
+ok too, and this function is total.
+
+:::aside
+while writing this post i discovered that this is actually a restatement of
+the type of `xs[i]` in the standard library and i could have just used that.
+oops!
+:::
+
+
+# typechecker
+
+i'm going to write the type checker using exceptions for error handling, because
+using an error monad without `do` notation was just too annoying. but from the
+outside it is still going to use a `result` type.
+
+```ats
+datatype result(t@ype, t@ype) =
+| {a, e : t@ype} Ok(a, e)  of a
+| {a, e : t@ype} Err(a, e) of e
+```
+
+the funky looking `t@ype` refers to a type of unknown size, as opposed to `type`
+which can only be instantiated with pointer-sized types. that will not come up
+again here but "`t@ype`" is definitely the funniest part of ats's syntax.
+
+the errors we need here are:
+
+- a function takes an argument of type $A$, but is given one of type $B$;
+- a term of a non-arrow type is being applied.
+
+```ats
+datatype err =
+| Clash of (typ, typ)
+| NotArr of typ
+
+fn print_err (e : err) : void = … // incredibly uninteresting
+overload print with print_err
+
+
+typedef typ_res = result(typ, err)
+
+fn print_res (r : typ_res) : void = …
+overload print with print_res
+```
+
+so onto the typechecker. like i said, it's going to use a local exception for
+errors, but then catch it on the outside so that it has a pure type.
+
+```ats
+fn typ_of {n : nat} (g : ctx n, t : term(n)) :<> typ_res =
+let
+  exception ERR of err
+  fun go {n, h : nat} .<h>. (g : ctx(n), t : term(n, h)) :<!exn> typ =
+  case t of
+  | Var(i)    => lookup(g, i)
+  | Lam(a, t) => Arr(a, go(list_cons(a, g), t))
+  | App(s, t) => begin
+      case go(g, s) of
+      | Arr(a1, b) =>
+          let val a2 = go(g, t) in
+            if a1 = a2 then b else $raise ERR(Clash(a1, a2))
+          end
+      | b => $raise ERR(NotArr(b))
+    end
+in
+  $effmask_exn(try Ok(go(g, t)) with ~ERR(e) => Err(e))
+end
+
+fn typ_of (t : term(0)) :<> typ_res = typ_of(list_nil, t)
+```
+
+most of this is fine. a bit noisy i guess. but there are a couple of new things:
+
+- in the type of `go`, the `:<!exn>` part means it can throw exceptions, but has
+  no other effects.
+- `$effmask_exn(e)` hides the `exn` effect in `e`, because ats doesn't
+  distinguish different exceptions in effects so it can't tell that `ERR` is the
+  only one that is ever raised.
+- exceptions are linear, and the pattern `~ERR(e)` is consuming the outermost
+  constructor.
+- exceptions are the only reason we needed `alloca` in this program
+  :woozy_face:
+
+
+# the end
+
+ok, a quick `main` function, and that's it!
+
+```ats
+implement main0() = begin
+  print("type of [λx:•. x] is: ");
+  print(typ_of(Lam(Base, Var(0))));
+  print("\ntype of [λx:•. x x] is: ");
+  print(typ_of(Lam(Base, App(Var(0), Var(0)))));
+  print("\n")
+end
+```
+
+and it works, at least on these two examples.
+
+```
+type of [λx:•. x] is: • → •
+type of [λx:•. x x] is: expected an arrow type, but got [•]
+```
+
+uh. thank's for reading. maybe i'll write another one if i think of another
+nice little program that actually uses more of ats's weirdness.
+
+--------------------------------------------------------------------------------
+
+<details>
+<summary>full code</summary>
+```ats
+#include "share/atspre_define.hats"
+#include "share/atspre_staload.hats"
+
+datatype typ(int) =
+|                Base(1)
+| {h1, h2 : nat} Arr(1 + max(h1, h2)) of (typ(h1), typ(h2))
+
+typedef typ = [h : nat] typ(h)
+
+fun eq_typ {ha : nat} .<ha>. (a : typ(ha), b : typ) :<> bool =
+case (a, b) of
+| (Base(),      Base())      => true
+| (Arr(a1, a2), Arr(b1, b2)) => eq_typ(a1, b1) && eq_typ(a2, b2)
+| (_,           _)           => false
+overload = with eq_typ
+
+fun print_typ (parens : bool, t : typ) : void =
+case t of
+| Base()    => print "•"
+| Arr(a, b) => begin
+    if parens then print("(");
+    print_typ(true, a);
+    print(" → ");
+    print_typ(false, b);
+    if parens then print(")");
+  end
+
+fn print_typ (t : typ) : void = print_typ(false, t)
+overload print with print_typ
+
+
+datatype term(int, int) =
+| {n, i : nat | i < n} Var(n, 1) of int(i)
+| {n, h : nat}         Lam(n, 1 + h) of (typ, term(1 + n, h))
+| {n, h1, h2 : nat}    App(n, 1 + max(h1, h2)) of (term(n, h1), term(n, h2))
+
+typedef term(n : int) = [h : nat] term(n, h)
+
+
+typedef ctx(n: int) = list(typ, n)
+
+fun lookup {n, i : nat | i < n} .<n>. (g : ctx(n), i : int(i)) :<> typ =
+let val+ list_cons(x, g) = g in
+  if i = 0 then x else lookup(g, i - 1)
+end
+
+
+datatype result(t@ype, t@ype) =
+| {a, e : t@ype} Ok(a, e)  of a
+| {a, e : t@ype} Err(a, e) of e
+
+
+datatype err =
+| Clash of (typ, typ)
+| NotArr of typ
+
+fn print_err (e : err) : void =
+case e of
+| Clash(a, b) => begin
+    print("clash between types [");
+    print(a);
+    print("] and [");
+    print(b);
+    print("]");
+  end
+| NotArr(t) => begin
+    print("expected an arrow type, but got [");
+    print(t);
+    print("]");
+  end
+overload print with print_err
+
+
+typedef typ_res = result(typ, err)
+
+fn print_res (r : typ_res) : void =
+case r of Ok(t) => print(t) | Err(e) => print(e)
+overload print with print_res
+
+
+fn typ_of {n : nat} (g : ctx n, t : term(n)) :<> typ_res =
+let
+  exception ERR of err
+  fun go {n, h : nat} .<h>. (g : ctx(n), t : term(n, h)) :<!exn> typ =
+  case t of
+  | Var(i)    => lookup(g, i)
+  | Lam(a, t) => Arr(a, go(list_cons(a, g), t))
+  | App(s, t) => begin
+      case go(g, s) of
+      | Arr(a1, b) =>
+          let val a2 = go(g, t) in
+            if a1 = a2 then b else $raise ERR(Clash(a1, a2))
+          end
+      | b => $raise ERR(NotArr(b))
+    end
+in
+  $effmask_exn(try Ok(go(g, t)) with ~ERR(e) => Err(e))
+end
+
+fn typ_of (t : term(0)) :<> typ_res = typ_of(list_nil, t)
+
+
+implement main0() = begin
+  print("type of [λx:•. x] is: ");
+  print(typ_of(Lam(Base, Var(0))));
+  print("\ntype of [λx:•. x x] is: ");
+  print(typ_of(Lam(Base, App(Var(0), Var(0)))));
+  print("\n")
+end
+```
+</details>

style/page.css

@@ -405,3 +405,4 @@ aside {
 :is(.st, .fl, .dv, .sc) { color: hsl(143deg, 100%, 20%); }
 .wa { color: hsl(350deg, 80%,  25%); text-decoration: wavy 1.5px underline; }
 .al { color: hsl(350deg, 80%,  25%); }
+.cn { color: hsl(343deg, 100%, 30%); }

syntax/ats.xml

@@ -0,0 +1,210 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE language SYSTEM "language.dtd" [
+  <!ENTITY LETTER "A-Za-z\xc0-\xd6\xd8-\xf6\xf8-\xff">
+  <!ENTITY IDENT  "[&LETTER;_@$][&LETTER;0-9_@$']*">
+  <!ENTITY ESC    "(\\[ntbr'&quot;\\]|\\[0-9]{3}|\\x[0-9A-Fa-f]{2})">
+  <!ENTITY DEC    "([0-9][0-9_]*)">
+  <!ENTITY DECEXP "([eE][+-]?&DEC;)">
+  <!ENTITY HEX    "([0-9a-fA-F]+)">
+]>
+
+<language name="ATS" section="Sources" extensions="*.sats;*.dats;*.hats"
+          version="1" kateversion="5.53">
+  <highlighting>
+    <list name="decl">
+      <item>abstype</item> <item>abst@ype</item> <item>absprop</item>
+      <item>absview</item> <item>absvtype</item> <item>absvt@ype</item>
+      <item>absviewtype</item> <item>absviewt@ype</item>
+
+      <item>exception</item>
+
+      <item>datatype</item> <item>dataprop</item> <item>dataview</item>
+      <item>dataviewtype</item> <item>datavtype</item> <item>datasort</item>
+
+      <item>typedef</item> <item>propdef</item> <item>viewdef</item>
+      <item>vtypedef</item> <item>viewtypedef</item> <item>sortdef</item>
+      <item>tkindef</item> <item>classdec</item>
+      <item>macdef</item> <item>macrodef</item>
+
+      <item>withtype</item> <item>withprop</item> <item>withview</item>
+      <item>withvtype</item> <item>withviewtype</item>
+
+      <item>val</item> <item>fun</item> <item>fn</item> <item>fnx</item>
+      <item>prfun</item> <item>prfn</item> <item>praxi</item>
+      <item>castfn</item>
+      <item>and</item>
+
+      <item>var</item> <item>prvar</item>
+
+      <item>infix</item> <item>infixl</item> <item>infixr</item>
+      <item>prefix</item> <item>postfix</item> <item>nonfix</item>
+
+      <item>symintr</item> <item>symelim</item>
+
+      <item>sta</item> <item>stacst</item>
+      <item>stadef</item> <item>static</item>
+    </list>
+
+    <list name="meta">
+      <item>extern</item> <item>extype</item> <item>extvar</item>
+      <item>$extern</item> <item>$extype</item> <item>$extkind</item>
+      <item>$extype_struct</item>
+
+      <item>$myfilename</item> <item>$mylocation</item> <item>$myfunction</item>
+
+      <item>import</item> <item>staload</item> <item>dynload</item>
+    </list>
+
+    <list name="preproc">
+      <item>#include</item> <item>#staload</item> <item>#dynload</item>
+      <item>#require</item>
+
+      <item>#if</item> <item>#ifdef</item> <item>#ifndef</item>
+      <item>#then</item>
+      <item>#elif</item> <item>#elifdef</item> <item>#elifndef</item>
+      <item>#else</item> <item>#endif</item>
+
+      <item>#error</item> <item>#prerr</item> <item>#print</item>
+      <item>#assert</item>
+
+      <item>#define</item> <item>#undef</item>
+
+      <item>#pragma</item> <item>#codegen2</item> <item>#codegen3</item>
+    </list>
+
+    <list name="impl">
+      <item>assume</item> <item>reassume</item>
+      <item>implmnt</item> <item>implement</item>
+      <item>primplmnt</item> <item>primplement</item>
+      <item>overload</item>
+    </list>
+
+    <list name="expr">
+      <item>begin</item> <item>end</item>
+      <item>op</item> <item>as</item>
+
+      <item>case</item> <item>prcase</item> <item>of</item> <item>when</item>
+      <item>scase</item>
+
+      <item>let</item> <item>local</item> <item>in</item> <item>rec</item>
+      <item>if</item> <item>then</item> <item>else</item>
+      <item>ifcase</item> <item>sif</item>
+      <item>where</item>
+
+      <item>for</item> <item>do</item>
+      <item>$break</item> <item>$continue</item>
+
+      <item>lam</item> <item>llam</item> <item>lam@</item>
+      <item>fix</item> <item>fix@</item>
+
+      <item>try</item> <item>with</item> <item>$raise</item>
+
+      <item>$delay</item> <item>$ldelay</item>
+
+      <item>$arrpsz</item> <item>$arrptrsize</item>
+      <item>$tyrep</item> <item>$d2ctype</item>
+
+      <item>$effmask</item>
+      <item>$effmask_ntm</item> <item>$effmask_exn</item>
+      <item>$effmask_ref</item> <item>$effmask_wrt</item>
+      <item>$effmask_all</item>
+
+      <item>$lst</item> <item>$lst_t</item> <item>$lst_vt</item>
+      <item>$list</item> <item>$list_t</item> <item>$list_vt</item>
+
+      <item>$rec</item> <item>$rec_t</item> <item>$rec_vt</item>
+      <item>$record</item> <item>$record_t</item> <item>$record_vt</item>
+
+      <item>$tup</item> <item>$tup_t</item> <item>$tup_vt</item>
+      <item>$tuple</item> <item>$tuple_t</item> <item>$tuple_vt</item>
+
+      <item>$solver_assert</item>
+      <item>$solver_verify</item>
+
+      <item>$vararg</item>
+      <item>$showtype</item>
+      <item>$tempenver</item>
+    </list>
+
+    <list name="prim">
+      <item>type</item> <item>t@ype</item>
+      <item>view</item> <item>prop</item>
+      <item>viewtype</item> <item>viewt@ype</item>
+      <item>vtype</item> <item>vt@ype</item>
+    </list>
+
+    <list name="const">
+      <item>bool</item> <item>true</item> <item>false</item>
+      <item>int</item> <item>nat</item>
+    </list>
+
+    <contexts>
+      <context attribute="default" lineEndContext="#stay" name="default">
+        <Detect2Chars attribute="comment" context="comment-1"
+                      char="/" char1="/" />
+        <Detect2Chars attribute="comment" context="comment-c"
+                      char="/" char1="*" />
+        <Detect2Chars attribute="comment" context="comment-ml"
+                      char="(" char1="*" />
+
+        <keyword attribute="decl" context="#stay" String="decl" />
+        <keyword attribute="meta" context="#stay" String="meta" />
+        <keyword attribute="preproc" context="#stay" String="preproc" />
+        <keyword attribute="impl" context="#stay" String="impl" />
+        <keyword attribute="expr" context="#stay" String="expr" />
+        <keyword attribute="prim" context="#stay" String="prim" />
+        <keyword attribute="const" context="#stay" String="const" />
+
+        <RegExpr attribute="arrowlike" context="#stay"
+          String="[-=&lt;>:]|=/?=>>?|\.&lt;|>\." />
+
+        <DetectChar attribute="string" context="string" char="&quot;" />
+
+        <RegExpr attribute="decint" context="#stay" String="~?&DEC;" />
+        <RegExpr attribute="float" context="#stay"
+          String="~?((&DEC;\.&DEC;?|\.&DEC;)&DECEXP;?|&DEC;&DECEXP;)" />
+        <RegExpr attribute="hexint" context="#stay" String="~?0[xX]&HEX;" />
+      </context>
+
+      <context attribute="comment" lineEndContext="#pop" name="comment-1" />
+      <context attribute="comment" lineEndContext="#stay" name="comment-c">
+        <!-- not nestable -->
+        <Detect2Chars attribute="comment" context="#pop"
+                      char="*" char1="/" />
+      </context>
+      <context attribute="comment" lineEndContext="#stay" name="comment-ml">
+        <!-- nestable -->
+        <Detect2Chars attribute="comment" context="comment-ml"
+                      char="(" char1="*" />
+        <Detect2Chars attribute="comment" context="#pop"
+                      char="*" char1=")" />
+      </context>
+
+      <context attribute="string" lineEndContext="#stay" name="string">
+        <RegExpr attribute="esc" context="#stay" String="&ESC;" />
+        <DetectChar attribute="string" context="#pop" char="&quot;" />
+      </context>
+    </contexts>
+
+    <itemDatas>
+      <itemData name="default" defStyleNum="dsNormal" />
+      <itemData name="comment" defStyleNum="dsComment" />
+
+      <itemData name="decl" defStyleNum="dsDataType" />
+      <itemData name="meta" defStyleNum="dsKeyword" />
+      <itemData name="preproc" defStyleNum="dsPreprocessor" />
+      <itemData name="impl" defStyleNum="dsFunction" />
+      <itemData name="expr" defStyleNum="dsControlFlow" />
+      <itemData name="prim" defStyleNum="dsBuiltIn" />
+      <itemData name="const" defStyleNum="dsConstant" />
+
+      <itemData name="arrowlike" defStyleNum="dsOperator" />
+
+      <itemData name="string" defStyleNum="dsString" />
+      <itemData name="decint" defStyleNum="dsDecVal" />
+      <itemData name="float" defStyleNum="dsFloat" />
+      <itemData name="hexint" defStyleNum="dsBaseN" />
+      <itemData name="esc" defStyleNum="dsSpecialChar" />
+    </itemDatas>
+  </highlighting>
+</language>