Examples from Introduction to Programming in ATS

.gitignore

*.c
a.out

000-start.md

Examples from Introduction to Programming in ATS

Full repo here →

This is my catalogue of all the examples and concepts described in the book Introduction to Programming in ATS.

Motivation

I'm learning ATS, so I thought I would catalogue my learnings into a sort of cheatsheet as I go through the book. I and other (potential) learners can use it as a quick reference.

The code samples are formatted according to my Haskelly aesthetic. ATS is notorious for looking very ugly, but I've attempted to make it pretty. For comparison see here.

Compiling the examples

Compile with:

$ atscc foo.dats

Run with:

$ ./a.out

or:

$ atscc foo.dats -o foo

Run with:

$ ./foo

001-hello.dats

(* Simple Hello, World! program. *)

(* Main entry point. *)
val _ = print "Hello, world!\n"

implement main () = ()

002-imports.dats

(* Import some prelude-like functions. *)

staload _ = "libc/SATS/stdio.sats"
staload _ = "prelude/DATS/array.dats"
staload _ = "prelude/DATS/array0.dats"
staload _ = "prelude/DATS/list.dats"
staload _ = "prelude/DATS/list0.dats"
staload _ = "prelude/DATS/list_vt.dats"
staload _ = "prelude/DATS/matrix.dats"
staload _ = "prelude/DATS/matrix0.dats"
staload _ = "prelude/DATS/option.dats"
staload _ = "prelude/DATS/option0.dats"
staload _ = "prelude/DATS/pointer.dats"
staload _ = "prelude/DATS/reference.dats"

(* Main entry point. *)
val _ = print "Here is a bunch of useful imports, like a prelude.\n"

implement main () = ()

003-exprs.dats

(* Examples of expression types. *)

(* Integrals are like this. *)
val integral = 1 * 2

(* Numbers are automatically floating if written like this. *)
val floating = 1.0 / 3

(* Operator functions can be used prefix like this. *)
val prefixOp = op/(1.0,3)

(* Characters. *)
val char = 'c'

(* Negative numbers use a tilde. *)
val negative = ~5

implement main () = ()

004-finalization.dats

(* No guarantee of order for finalization for pi and radius. *)
val pi = 3.14 and radius = 10.0

(* However, area will be finalized after both pi and radius. *)
val area = pi * radius * radius

(* Just print the area to stdout. *)
val _ = print area

implement main () = ()

005-local-bindings.dats

(* Local bindings. *)

(* You can use ‘let’ syntax to make the ‘area’ binding global, but pi *)
(* and ardius local. *)
val area =
  let val pi = 3.14
      val radius = 10.0
  in pi * radius * radius
  end

(* Alternatively, ‘where’ syntax can be used: *)
val area =
  pi * radius * radius
  where {
    val pi = 3.14
    val radius = 10.0
  }

(* Alternatively, to create many top-level bindings with the same *)
(* scope, you can use ‘local’. *)
local
  val pi = 3.14
  val radius = 10.0
in
  val area = pi * radius * radius
end

(* Use ‘and’ to make bindings share the same environment. *)
val area =
  let val pi = 3.14
      and radius = 10.0
  in pi * radius * radius
  end

(* Main entry point. *)
val _ = print area

implement main () = ()

006-tuples.dats

(* Demonstrating tuples. *)

(* Tuple syntax. *)
val xyz = ('A',1,2.0)

(* Tuple slots are accessed via their indexes. *)
val x = xyz.0
and y = xyz.1
and z = xyz.2

val _ = print x
val _ = print "\n"

val _ = print y
val _ = print "\n"

val _ = print z
val _ = print "\n"

(* Pattern matching upon tuples. *)
val (a,b,c) = xyz

val _ = print a
val _ = print "\n"

val _ = print b
val _ = print "\n"

val _ = print c
val _ = print "\n"

implement main () = ()

007-records.dats

(* Records. *)

(* Defines an unboxed record type named ‘point2d’ with fields ‘x’ and ‘y’. *)
typedef Point2D = @{x = double,y = double}

(* Make a record of type ‘Point2D’: *)
val origin = @{x = 1.0,y = 2.0} : Point2D

(* Access the fields of the record: *)
val originX = origin.x
and originY = origin.y

(* Alternatively, pattern matching can be used: *)
val @{x = originX,y = originY} = origin

(* Wildcards can be used to ignore all fields but a few: *)
val @{x = originX,...} = origin

implement main () = ()

008-if.dats

(* If expressions. *)

(* Some binding to use. *)
val x = 3

(* If expression can have two branches: *)
val neg =
  if x >= 0
     then x
     else ~x

implement main () = ()

009-sequences.dats

(* Sequence expressions. *)

(* Runs the print commands in sequence. *)
val _ = (print 'H'
        ;print 'e'
        ;print 'l'
        ;print 'l'
        ;print 'o')

(* Alternative form of sequencing. *)
val _ =
  begin
    print 'H';
    print 'e';
    print 'l';
    print 'l';
    print 'o';
  end

implement main () = ()

010-functions.dats

(* Functions. *)

(* Define a non-recursive symbol x² function. *)
fn square (x : double) : double =
  x * x

(* Anonymous function: *)
val square =
  lam (x : double) : double =>
    x * x

(* Defines a multi-argument function. *)
fn areaOfRing (R : double, r : double) : double =
  3.1416 * (square R - square r)

(* Defines a recursive function. *)
fun sum1 (n : int) : int =
  if n >= 1
     then sum1 (n - 1) + n
     else 0

(* Two-arg recursive function. *)
fun sum2 (m : int, n : int) : int =
  if m <= n
     then m + sum2 (m + 1, n)
     else 0

(* Cleverer sum. *)
fun sum3 (m : int, n : int) : int =
  if m <= n
     then let val mn2 = (m + n) / 2
          in sum3 (m,mn2 - 1) + mn2 + sum3 (mn2 + 1,n)
          end
     else 0

(* Fibonacci. *)
fun fib (n : int) : int =
  if n >= 2
     then fib (n - 1) + fib (n - 2)
     else n

(* Use the sum1 function: *)
val _ =
  begin print (sum1 10);
        print "\n";
  end

(* Use the sum3 function: *)
val _ =
  begin print (sum3 (10,100));
        print "\n";
  end

(* Use the square function: *)
val _ =
  begin print (square 5.0);
        print "\n";
  end

(* Use the areaOfRing function: *)
val _ =
  begin print (areaOfRing (5.0,2.0));
        print "\n";
  end

(* Use the fib function: *)
val _ =
  print (fib 10)

implement main () = ()

011-coins.dats

(* The classic coins denominations problem. *)

(* Define a 4-tuple of ints. *)
typedef Int4 = (int, int, int, int)

(* Some example coins. *)
val coins = (1, 5, 10, 25) : Int4

(* Get coin value by index. *)
fun coinIndex (n : int) : int =
  if n = 0
     then coins.0
     else if n = 1
             then coins.1
             else if n = 2
                     then coins.2
                     else if n = 3
                             then coins.3
                             else ~1

(* Calculate change given by a number. *)
fun coinChange (sum : int) =
  go (sum,3)
  where {
    fun go (sum : int,n : int) : int =
      if sum > 0
         then if n >= 0
                 then go (sum,n - 1) +
                      go (sum - coinIndex (n),n)
                 else 0
         else if sum < 0
                 then 0
                 else 1
  }

(* Example usages: *)
val _ =
  begin print (coinChange 25);
        print "\n";
        print (coinChange 100);
        print "\n";
        print (coinChange 0);
        print "\n";
        print (coinChange 1);
        print "\n";
  end

implement main () = ()

012-tco.dats

(* Tail-call optimization. *)

(* Lispers, MLers and Haskellers will be familiar with this problem. *)
(* You really need this if you want to write efficient loops. *)

(* Tail recursive sum function. *)
fun sum (n : int,acc : int) : int =
  if n > 0
     then sum (n - 1,n + acc)
     else acc

(* If you don't want to expose the accumulator argument,
   you can use a local function.
*)
fun sum (n : int) : int =
  go (n,0)
  where {
    fun go (n : int,acc : int) : int =
        if n > 0
           then go (n - 1,n + acc)
           else acc
  }

(* Example use: *)
val _ = print (sum 10)

implement main () = ()

013-nqueens.dats

(* N-queens problem. *)

(* Board size. *)
val size : int = 8

(* Define an 8-tuple of ints. *)
typedef Int8 = (int,int,int,int,int,int,int,int)

(* Print n dots. *)
fun printDots (i : int) : void =
  if i > 0
     then begin print ". ";
                printDots (i-1);
          end

(* Print a row of the board. *)
fun printRow (i : int) : void =
  begin
    printDots i;
    print "Q ";
    printDots (size - i - 1);
    print "\n";
  end

(* Print rows of the board. *)
fun printBoard (bd : Int8) : void =
  begin
    printRow bd.0;
    printRow bd.1;
    printRow bd.2;
    printRow bd.3;
    printRow bd.4;
    printRow bd.5;
    printRow bd.6;
    printRow bd.7;
    print "\n";
  end

(* Get a slot from the board. *)
fun boardIndex (bd : Int8,i : int) : int =
  case i of
    | 0 => bd.0
    | 1 => bd.1
    | 2 => bd.2
    | 3 => bd.3
    | 4 => bd.4
    | 5 => bd.5
    | 6 => bd.6
    | 7 => bd.7
    | _ => ~1

(* Set a value in the board. *)
fun boardSet (bd : Int8,i : int,j:int) : Int8 =
  let val (x0,x1,x2,x3,x4,x5,x6,x7) = bd
  in case i of
       | 0 => (j,x1,x2,x3,x4,x5,x6,x7)
       | 1 => (x0,j,x2,x3,x4,x5,x6,x7)
       | 2 => (x0,x1,j,x3,x4,x5,x6,x7)
       | 3 => (x0,x1,x2,j,x4,x5,x6,x7)
       | 4 => (x0,x1,x2,x3,j,x5,x6,x7)
       | 5 => (x0,x1,x2,x3,x4,j,x6,x7)
       | 6 => (x0,x1,x2,x3,x4,x5,j,x7)
       | 7 => (x0,x1,x2,x3,x4,x5,x6,j)
       | _ => bd
  end

(* Can a queen piece on row i0 and column j0 capture another one on row i and column j? *)
fun canCapture (i0: int,j0: int,i1: int,j1: int) : bool =
  j0 <> j1 andalso
  abs (i0 - i1) <> abs (j0 - j1)

(* Can a queen piece on row i0 and column j0 capture any pieces on
   a given board with a row number less than or equal to i?
*)
fun canCaptureLess (i0: int,j0: int,bd: Int8,i: int) : bool =
  if i >= 0
     then if canCapture (i0,j0,i,boardIndex (bd,i))
             then canCaptureLess (i0,j0,bd,i-1)
             else false
     else true

(* Search for and print all solutions. *)
fun search (bd : Int8,i: int,j: int,nsol: int) : int =
  if j < size
     then
       if canCaptureLess (i,j,bd,i-1)
          then
            let val bd1 = boardSet (bd,i,j)
            in if i+1 = size
                  then begin
                         print! ("This is solution no. ",nsol + 1,":\n\n");
                         printBoard bd1;
                         search (bd,i,j + 1,nsol + 1);
                       end
                  else search (bd1,i + 1,0,nsol)
            end
          else search (bd,i,j + 1,nsol)
     else if i > 0
             then search (bd,i - 1,boardIndex (bd,i - 1) + 1,nsol)
             else nsol

(* Print a sample board. *)
val _ = printBoard @(0,1,2,3,4,5,6,7)

(* Print out solutions. *)
val _ = search (@(0,0,0,0,0,0,0,0),0,1,0)

implement main () = ()

014-mutualrecursive.dats

(* Mutually recursive functions. *)

(* Use the fn* function, sort of wildcard :  combine all the functions
   into one and uses local jumps for calling eachother.
*)
fn* isevn (n : int) : bool =
  if n > 0
     then isodd (n - 1)
     else true
and isodd (n : int) : bool =
  if n > 0
     then isevn (n - 1)
     else false

(* Print out a standard multiplication table for nonzero digits. *)
fun print_multable () =
  go1 1
  where {
    fn* go1 (i : int) : void =
      if i <= 9
         then go2 (i,1)
         else ()
    and go2 (i : int,j : int) : void =
      if j <= i
         then begin if j >= 2 then print " ";
                    printf ("%dx%d=%2.2d",@(j,i,j * i));
                    go2 (i,j + 1)
              end
         else begin print_newline ();
                    go1 (i + 1)
              end
  }

val _ = print_multable ()

implement main () = ()

014-mutualrecursive.md

Prints out:

1x1=01
1x2=02 2x2=04
1x3=03 2x3=06 3x3=09
1x4=04 2x4=08 3x4=12 4x4=16
1x5=05 2x5=10 3x5=15 4x5=20 5x5=25
1x6=06 2x6=12 3x6=18 4x6=24 5x6=30 6x6=36
1x7=07 2x7=14 3x7=21 4x7=28 5x7=35 6x7=42 7x7=49
1x8=08 2x8=16 3x8=24 4x8=32 5x8=40 6x8=48 7x8=56 8x8=64
1x9=09 2x9=18 3x9=27 4x9=36 5x9=45 6x9=54 7x9=63 8x9=72 9x9=81

015-closures.dats

(* Closures

   Functions in ATS, like C, do not carry environments for
   closures. Use :<cloref1> to enable this.

 *)

(* Use the cloref1 type to indicate that `loop` closes over `n'.
   Note that there is no space between : and <cloref1>.
 *)
fun sum (n : int) : int =
  let fun loop (i : int, res : int) :<cloref1> int =
        if i <= n
           then loop (i + 1,res + i)
           else res
  in loop (1,0)
  end

(* Making anonymous closing functions. *)
fun addx (x : int) : int -<cloref1> int =
  lam y => x + y

(* plus1 has type int -<cloref1> int *)
val plus1 = addx (1)

(* plus2 has type int -<cloref1> int *)
val plus2 = addx (2)

(* Demonstrate closure calls. *)
val _ =
  begin print! (sum 10,"\n");
        print! (plus1 10,"\n");
        print! (plus2 10,"\n");
  end

implement main () = ()

016-higherorder.dats

(* Higher-order functions *)

(* Given a function from integers to integers, rtfind searches for the
   first natural number that is a root of the function. For instance,
   calling rtfind on the polynomial function lam x => x * x - x + 110
   returns 11. Note that rtfind loops forever if it is applied to a
   function that does not have a root.
 *)
fun rtfind (f : int -> int) : int =
  loop (f,0)
  where {
    fun loop (f : int -> int,n : int) : int =
      if f (n) = 0
         then n
         else loop (f,n + 1)
  }

(* An integer fold. *)
fun ifold (n : int,f : (int,int) -> int,ini : int) : int =
  if n > 0
     then f (ifold (n - 1,f,ini),n)
     else ini

(* Sum implemented in terms of ifold. *)
fun sum (n : int) : int =
  ifold (n,lam (res,x) => res + x,0)

(* Prod implemented in terms of ifold. *)
fun prod (n : int) : int =
  ifold (n,lam (res,x) => res * x,1)

(* Compute the sum of the squares of the integers ranging from 1 to a
given natural number. *)
fun sqrsum (n : int) : int =
  ifold (n,lam (res,x) => res + x * x,0)

(* Demos of functions defined in terms of higher-order functions. *)
val _ =
  begin print! (sqrsum 6,"\n");
        print! (prod 5,"\n");
        print! (sum 10,"\n");
  end

implement main () = ()

017-currying.dats

(* Currying *)

(* Uncurried Ackermann. *)
fun acker1 (m: int, n: int): int =
  if m > 0 then
    if n > 0 then acker1 (m-1, acker1 (m, n-1)) else acker1 (m-1, 1)
  else n+1

(* Curried Ackermann. *)
fun acker2 (m: int) (n: int): int =
  if m > 0 then
    if n > 0 then acker2 (m-1) (acker2 m (n-1)) else acker2 (m-1) 1
  else n+1

(* Demo of uncurried vs curried args. *)
val _ =
  begin print! (acker1 (2,2),"\n");
        print! (acker2 2 2,"\n");
  end

implement main () = ()

018-datatypes.dats

(* Data types *)

(* A type like Maybe or Option *)
datatype MaybeInt =
  | NothingInt of ()
  | JustInt of int

(* Day of the week. *)
datatype Day =
  | Monday of ()
  | Tuesday of ()
  | Wednesday of ()
  | Thursday of ()
  | Friday of ()
  | Saturday of ()
  | Sunday of ()

(* Char list *)
datatype ListChar =
  | NilChar of () | ConsChar of (char, ListChar)

(* Example of list of chars. *)
val exampleChars =
  ConsChar ('a',ConsChar ('b',ConsChar ('c',NilChar ())))

(* Get length of a list of chars. *)
fun charsLength (cs : ListChar) : int =
  case cs of
    | ConsChar (_,cs) => 1 + charsLength (cs)
    | NilChar () => 0

(* Tail-recursive version of charsLength. *)
fun charsLengthTCO (cs : ListChar) : int =
  go (cs,0)
  where {
    fun go (cs : ListChar,n : int) : int =
      case cs of
        | ConsChar (_,cs) => go (cs,n + 1)
        | NilChar ()      => n
  }
(* Is the given day a weekday? *)
fun isWeekday (x : Day) : bool =
  case x of
    | Saturday () => false
    | Sunday ()   => false
    | _           => true

(* Demo of types. *)
val mint = JustInt 10
val day =
  case mint of
    | JustInt 0 => Thursday ()
    | JustInt i => Wednesday ()
    | _ => Friday ()
val _ =
  begin print! (case mint of
                  | JustInt 0 => ~1
                  | JustInt i => i
                  | _ => 0
               ,"\n");
        case () of
          () => print! ("Unit is unit!","\n");
        print! (isWeekday day,"\n");
        print (isWeekday (Saturday ()))
  end

implement main () = ()

019-templates.dats

(* Function templates *)

(* This function is polymorphic over the two types of the tuple. *)
fun {a,b : t@ype} swap ((x,y) : (a,b)) = (y,x)
(*         ^ That is the "sort" (in Haskell: kind, in Idris: type) of
             the types a and b. I have no idea why such an ugly name
             as "t@ype" was chosen.
*)

(* Basic tuple. *)
val ab = (10,"foo")

(* Swapped tuple. *)
val ba = swap ab

(* Compose two functions. *)
typedef Compose (f : t@ype, g : t@ype) =
  f -<cloref1> g
(*  ^ Yep, that's also real. *)

(* Identity on boxed types. *)
fun {a : type} identB (x : a) : a = x

(* Identity on unboxed types. *)
fun {a : t@ype} identU (x : a) : a = x

val _ = identU (123 : int)

(* In Haskell this type is like:

   (.) :: (b -> c) -> (a -> b) -> (a -> c)

 *)
fun {a,b,c : t@ype} compose (f : Compose (b,c),g : Compose (a,b)) :<cloref1> Compose (a,c) =
  lam x => f (g x)

(* Simple function to be used in composition. *)
val plus1 = lam (x : int) : int =<cloref1>
  x + 1

(* Simple function to be used in composition. *)
val times2 = lam (x : int) : int =<cloref1>
  x * 2

(* Composition of two functions. *)
val plus1ThenTimes2: Compose (int,int) =
  compose (times2,plus1)

(* Composition of two functions: visa-versa *)
(* Alternate way of writing. *)
val times2ThenPlus1: int -<cloref1> int =
  compose (plus1,times2)

(* Demo of templates. *)
val _ =
  begin
    print! (ab.0,",",ab.1,"\n");
    print! (ba.0,",",ba.1,"\n");
    print! (times2ThenPlus1 5);
  end

implement main () = ()

020-polymorphic.dats

(* Polymorphic functions *)

(* Swapping of boxed tuples. *)
fun swapBoxed {a,b : type} ((x,y) : (a,b)) : (b,a) =
  (y,x)

fun swapUnoxed {a,b : t@ype} ((x,y) : (a,b)) : (b,a) =
  (y,x)

(* List data type. *)
datatype List (a : type) =
  | Nil (a) of ()
  | Cons (a) of (a,List a)

(* Option type. *)
datatype Option (a : type) =
  | None (a) of ()
  | Someome (a) of a

(* Length *)
fun {a : type} listLength (xs : List a) : int =
  case xs of
    | Cons (_,xs) => 1 + listLength xs
    | Nil ()      => 0

(* Sample tuple. *)
val AB = ("A","B")

(* The {string,string} arguments isn't necessary, but sometimes it is. *)
val BA1 = swapBoxed {string,string} AB
val BA2 = swapBoxed AB

implement main () = ()

021-exceptions.dats

(* Exceptions *)

(* List data type. *)
datatype List (a : t@ype) =
  | Nil (a) of ()
  | Cons (a) of (a,List a)

(* Product of a list of ints. *)
fun listProd (xs : List int) : int =
  (try go (xs)
   with ~DivisionByZero () => 0)
  where {
    exception DivisionByZero of ()
    fun go (xs : List int) : int =
      case xs of
        | Cons (x,xs) =>
          if x = 0
             then $raise DivisionByZero()
             else x * go (xs)
        | Nil => 1
  }

(* Demo of exception handling *)
val _ =
  begin print! (listProd(Cons (1,Cons (2,Nil ()))),"\n");
  end

implement main () = ()

022-io.dats

(* I/O *)

staload _(*anon*) = "libc/SATS/stdio.sats"

(* Open a file *)
val out = open_file_exn ("hello.txt",file_mode_w)

(* Do some actions with the file *)
val _ =
  begin fprint_string (out,"Hello,world!\n");
        close_file_exn (out);
  end

(* A simple get line / output line loop. *)
fun loop ():  void =
  let val line = input_line (stdin_ref)
  in if stropt_is_some (line)
        then begin output_line (stdout_ref,stropt_unsome (line));
                   loop ();
             end
        else ()
  end

val _ = loop ()

implement main () = ()

022-references.dats

(* References *)

(* Import references lib. *)
staload _(*anon*) = "prelude/DATS/reference.dats"

(* Create a ref and initialize it with 0. *)
val intr = ref<int> (0)

(* Increment the reference. *)
val () = !intr := !intr + 1
val i = !intr

(* A simple mutable counter. *)
typedef Counter =
 '{ get   = () -<cloref1> int
  , inc   = () -<cloref1> void
  , reset = () -<cloref1> void
  }

(* Make a new counter. *)
fun newCounter () : Counter =
  let val count = ref<int> (0)
  in '{get   = lam () => !count
      ,inc   = lam () => !count := !count + 1
      ,reset = lam () => !count := 0
      }
  end

(* Demo of *)
val _ =
  begin print! (i,"\n");
  end

implement main () = ()

023-arrays.dats

(* Arrays *)

staload _(*anon*) = "prelude/DATS/array.dats"
staload _(*anon*) = "prelude/DATS/array0.dats"

(* Insertion sort. *)
fun {a : t@ype} insertionSort (array : array0 (a),cmp : (a,a) -> int) : void =
  go 1
  where {
    val arraySize = array0_size array
    val length = int_of_size arraySize
    fun ins (x : a,i : int) :<cloref1> void =
      if i >= 0
         then
           if cmp (x,array[i]) < 0
              then begin array[i+ 1] := array[i];
                         ins (x,i - 1);
                   end
              else array[i+1] := x
         else array[0]  := x
    fun go (i : int) :<cloref1> void =
      if i < length
         then begin ins (array[i],i - 1);
                    go (i + 1);
              end
         else ()
  }

implement main () = ()

023-macros.dats

(* Macros *)

(* A macro to compute cubes. *)
macrodef cube (x) =
  `(,(x) * ,(x) * ,(x))

(* Example of using cube. *)
fun cubesum (i : int,j : int) : int =
  ,(cube `(i)) + ,(cube `(j))

implement main () = ()

024-matrices.dats

(* Matrices *)

(* Transpose a matrix. *)
fun {a : t@ype} transpose (matrix : matrix0 a) : void =
  goRows 0
  where {
    val nrow = matrix0_row (matrix)
    fn* goRows (i : size_t) :<cloref1> void =
      if i < nrow
         then goCols (i,0)
         else ()
    and goCols (i : size_t,j : size_t) :<cloref1> void =
      if j < i
         then let val tmp = matrix[i,j]
              in begin matrix[i,j] := matrix[j,i];
                       matrix[j,i] := tmp;
                       goCols (i,j + 1)
                 end
              end
         else goRows (i + 1)
  }

implement main () = ()