A guessing game implementation in ATS

Here is the quintessential guessing game as implemented in ATS.

The SATS file (the public external specification)

(* guessing_game.sats *)

fun play(): void

and the DATS file (the implementation):

(* guessing_game.dats *)

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

staload "guessing_game.sats"

staload STDLIB = "libats/libc/SATS/stdlib.sats"
staload UN = "prelude/SATS/unsafe.sats"
staload TIME = "libats/libc/SATS/time.sats"

fun generate_secret
  (lower: int, upper: int): int =
  let 
    val () = $STDLIB.srand48($UN.cast{lint}($TIME.time_get()))
    val range = $UN.cast{lint}(upper - lower + 1)
    val random = $STDLIB.lrand48() mod range + $UN.cast{lint}(lower)
  in
    $UN.cast{int}(random)
  end

fun read_guess(): int = 
  let
    macdef MAXLEN = 20
    var inp = @[char][MAXLEN]()
    val () = print!("Enter guess: ")
    val bc = $extfcall(int, "scanf", "%s", addr@inp)
    val () = assertloc(bc != 0)
  in
    g0string2int($UN.cast{string}(addr@inp))
  end

fun play_aux
  (secret: int, guesses: int): void = 
  let
    val guess = read_guess()
  in
    ifcase
      | guess < secret => (println!("Too small! Try again..."); play_aux(secret, guesses + 1))
      | guess > secret => (println!("Too big! Try again..."); play_aux(secret, guesses + 1))
      | _ => 
          let
            val guesses = guesses + 1
          in
            println!("You win! You took ", guesses, " guesses.")
          end
  end

implement play() = 
  let
    val secret = generate_secret(1, 100)
    val guesses = 0
  in
    play_aux(secret, guesses)
  end

implement main0() = play()

and finally, the Makefile:

ATSFLAGS := -DGNU_SOURCE -DATS_MEMALLOC_LIBC -cleanaft -flto -O3 -latslib

GUESSING_GAME_SRC := guessing_game.sats guessing_game.dats
GUESSING_GAME_OBJ := ${GUESSING_GAME_SRC}
GUESSING_GAME_OBJ := ${patsubst %.sats, %_sats.o, ${GUESSING_GAME_OBJ}}
GUESSING_GAME_OBJ := ${patsubst %.dats, %_dats.o, ${GUESSING_GAME_OBJ}}

guessing_game: ${GUESSING_GAME_OBJ}
    acc pc ${ATSFLAGS} -o $@ $^

%_sats.o: %.sats
    acc pc -c $< || touch $@

%_dats.o: %.dats
    acc pc -DATS_MEMALLOC_LIBC -c $< || touch $@

clean:
    rm -f *.o *_?ats.c guessing_game

Running it:

$ make clean && make && ./guessing_game
rm -f *.o *_?ats.c guessing_game
acc pc -c guessing_game.sats || touch guessing_game_sats.o

------------------ C COMPILER MESSAGES ------------------

clang: warning: argument unused during compilation: '-L/Users/z0ltan/dev/forks/ATS2-Postiats/ccomp/atslib/lib' [-Wunused-command-line-argument]

-------------- END C COMPILER MESSAGES ------------------

acc pc -DATS_MEMALLOC_LIBC -c guessing_game.dats || touch guessing_game_dats.o

------------------ C COMPILER MESSAGES ------------------

clang: warning: argument unused during compilation: '-L/Users/z0ltan/dev/forks/ATS2-Postiats/ccomp/atslib/lib' [-Wunused-command-line-argument]

-------------- END C COMPILER MESSAGES ------------------

acc pc -DGNU_SOURCE -DATS_MEMALLOC_LIBC -cleanaft -flto -O3 -latslib -o guessing_game guessing_game_sats.o guessing_game_dats.o
Enter guess: 50
Too small! Try again...
Enter guess: 75
Too small! Try again...
Enter guess: 88
Too big! Try again...
Enter guess: 82
Too big! Try again...
Enter guess: 78
Too small! Try again...
Enter guess: 80
Too small! Try again...
Enter guess: 81
You win! You took 7 guesses.

Functional Insertion Sort in ATS

I had presented a functional merge sort implementation in a previous blog. Here is an example of a functional implementation of insertion sort in ATS:

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

staload "libats/ML/SATS/basis.sats"
staload STDLIB = "libats/libc/SATS/stdlib.sats"
staload TIME = "libats/libc/SATS/time.sats"
staload UN = "prelude/SATS/unsafe.sats"

staload RG = "contrib/atscntrb/atscntrb-hx-mytesting/SATS/randgen.sats"
staload "contrib/atscntrb/atscntrb-hx-mytesting/DATS/randgen.dats"

staload "libats/ML/SATS/list0.sats"
staload "libats/ML/DATS/list0.dats"

typedef lte (a: t@ype) = (a, a) -> bool

fun{a: t@ype}
insert
  (e: a, xs: list0 a, lte: lte a): list0 a =
  case+ xs of
    | list0_nil() => list0_cons(e, list0_nil())
    | list0_cons(x, xs) when e \lte x => list0_cons{a}(e, list0_cons{a}(x, xs))
    | list0_cons(x, xs) => list0_cons{a}(x, insert<a>(e, xs, lte))

fun{a: t@ype}
insertion_sort
  (xs: list0 a, lte: lte a): list0 a = 
  case+ xs of
    | list0_nil() => list0_nil()
    | list0_cons(x, xs) => insert<a>(x, insertion_sort<a>(xs, lte), lte)

macdef INTMAX = 1000L

typedef T1 = int
implement $RG.randgen_val<T1>() = let
  val x = $STDLIB.lrand48() mod INTMAX in $UN.cast2int(x)
end

typedef T2 = double
implement $RG.randgen_val<T2>() = $STDLIB.drand48()

implement main0 () = {
  #define N 10

  val xs1 = $RG.randgen_list<T1>(N)
  val () = fprintln!(stdout_ref, "before sorting:\t", xs1)
  val xs1 = g0ofg1(xs1)
  val ys1 = insertion_sort<int>(xs1, lam (x, y) => x <= y)
  val ys1 = g1ofg0(ys1)
  val () = fprintln!(stdout_ref, "after sorting (ascending): ", ys1)
  val () = print_newline()

  val xs2 = $RG.randgen_list<T2>(N)
  val () = fprintln!(stdout_ref, "input:\t", xs2)
  val xs2 = g0ofg1(xs2)
  val ys2 = insertion_sort<double>(xs2, lam (x, y) => x >= y)
  val ys2 = g1ofg0(ys2)
  val () = fprintln!(stdout_ref, "after sorting (descending):  ", ys2)
  val () = print_newline()
}

Running it:

$ make insertion_sort && ./insertion_sort
acc pc -DATS_MEMALLOC_LIBC -o insertion_sort insertion_sort.dats
before sorting: 618, 587, 491, 623, 517, 565, 914, 197, 519, 566
after sorting (ascending): 197, 491, 517, 519, 565, 566, 587, 618, 623, 914

input:  0.691004, 0.058859, 0.899854, 0.163546, 0.159072, 0.533065, 0.604144, 0.582699, 0.269971, 0.390478
after sorting (descending):  0.899854, 0.691004, 0.604144, 0.582699, 0.533065, 0.390478, 0.269971, 0.163546, 0.159072, 0.058859

A guessing game implementation in LOGO

The very first language that I ever learnt in my life was LOGO all the way back in the third grade (year/standard). I immediately fell in love with it, and I would eagerly wait for
the lab to open so that I could try out all the pictures that I had in mind – houses, spirals, animals, scenery and what not! The funny thing is that back then, as is the case today, LOGO has the slight misfortune of becoming synonymous with “Turtle Graphics”. In fact, for decades after, I myself believed that that was all thet LOGO was good for.

Imagine my surprise when I read on some forum that LOGO actually was a sort of Lisp. I could not believe it, and when I started digging back into LOGO, I realised that this belief is not unfounded. In fact, in some ways, LOGO is a better Lisp than many Lisps available today! I’ve been learning LOGO for a few days now (not just for the sheer edificational
fun of it, but perhaps also for some more pracical reasons which may become more concrete in the near future), and in fact it almost feels like Forth done right – the natural function composition based on the arity of the functions (procedures as well) themselves is nothing short of simplistic beauty.

The book I have been using to (re)learn LOGO is “Symbolic Computing” by Brian Harvey. This is the first of a series of books (and all of which I plan to complete). The thing that stood out most for me is that difference that a good pedagogical bent of mind can make. This book, along with JIm Blandy and Jason Orendorff’s “Programming Rust” and Graham Hutton’s “Programming in Haskell” are probably my most favourite programming language books of all time.

So I made a simple guessing game (my go to example when learning a new language or just fooling around) in LOGO. It runs in UCB LOGO. Here is the code:

to guessing.game
  print [Welcome to the guessing game!]
  print [Your task is to guess a secret number between 1 and 100 (exclusive)]
  play get.secret 1 100 1
end

to play :secret :score
  print [Enter your guess:]
  local "guess
  make "guess first readlist
  if lessp :guess :secret [print [Too small! Try again!] play :secret :score+1]
  if greaterp :guess :secret [print [Too big! Try again!] play :secret :score+1]  
  if equalp :guess :secret ~
    [print (sentence [Correct! You took] :score [guesses. Thank you for playing.]) stop] 
end

to get.secret :low :high
  output sum random :high-:low :low
end

A simple Monadic Parser Combinator library in Idris

Monadic parsing is a form of parsing that combines lexing, parsing, and often evaluation in the same recursive process. Languages with strong algebraic data types (and
thereby good pattern-matching) are excellent candidates for monadic parsing. Interestingly, Rust has a popular parser-combinator library called nom, but using it is not as clean as in ML-like languages due to the syntax used by Rust (not to mention involving the less-than-great macro system of Rust).

This is a simple exercise in implementing one of my favourite chapters in any programming textbook, the chapter on Monadic Parsing in the book, “Programming in Haskell” (2nd Edition) by Professor Graham Hutton. He has written quite a few papers on the subject which are well worth reading as well. For instance, Monadic Parser Combinators, and Monadic Parsing in Haskell to mention a couple.

The basic idea here is to build up a relatively powerful parser-combinator library bottom-up – whereby we define a custom parser type, implement primitive parsers using the Monad andAlternative macghinery, and progressively build up more and more powerful parsers.

Let’s start off with the basic parser implementation:

module ParsCom

import Data.Strings

%default total

{-
  Note that we get some parsers for free - 

   * A parser that always succeeds - `pure` from the Applicative interface
   * A parser that is equivalent to epsilon (no choice) - `empty` from the Alternative interface
   * sequencing by using `do` from the Monad interface
   * Choice by using the `(<|>)` operator from the Alternative interface
   * Repetitions by using the `some` and `many` functions (that we define ourselves since the Alternative
     interface in Idris, unlike Haskell, does not seem to have them)
-}

||| The Parser data type - takes a string argument 
||| and produces a result and the unconsumed string
public export
data Parser : Type -> Type where
  MkParser : (String -> List (a, String)) -> Parser a

||| Helper function to apply a parser
export
parse : Parser a -> String -> List (a, String)
parse (MkParser p) inp = p inp

||| A parser that consumes a single character
export
item : Parser Char
item = MkParser (\inp => case (unpack inp) of
                            [] => []
                            (c :: cs) => [(c, pack cs)])

--- making the Parser types a monad so that we can 
--- use the `do` notation

public export
Functor Parser where
  -- fmap : (a -> b) -> Parser a -> Parser b
   map f p = MkParser (\inp => case parse p inp of
                                    [(v, out)] => [(f v, out)]
                                    _ => [])

public export
Applicative Parser where
  -- pure : a -> Parser a
  pure v = MkParser (\inp => [(v, inp)])

  -- (<*>) : Parser (a -> b) -> Parser a -> Parser b
  pf <*> p = MkParser (\inp => case parse pf inp of
                                  [(f, out)] => parse (map f p) out
                                  _ => [])

public export
Monad Parser where
  -- (>>=) : Parser a -> (a -> Parser b) -> Parser b
  p >>= f = MkParser (\inp => case parse p inp of
                                  [(v, out)] => parse (f v) out
                                  _ => [])

-- make the Parser an instance of the Alternative class so that 
-- we can use choice and epsilon (no choice) operators

public export
Alternative Parser where
  -- empty : Parser a
  empty = MkParser (\_ => [])

  -- (<|>) : Parser a -> Parser a -> Parser a
  p <|> q = MkParser (\inp => case parse p inp of
                                [(v, out)] => [(v, out)]
                                _ => parse q inp )

-- primitive parsers

||| A parser that matches against the supplied predicate
sat : (Char -> Bool) -> Parser Char
sat p = do x <- item
           if p x then pure x else empty

||| A parser that consumes a single character matching the supplied character
char : Char -> Parser Char
char c = sat (== c)

||| A Parser that matches against a digit character
digit : Parser Char
digit = sat isDigit

||| A Parser that matches against a lowercase letter
lower : Parser Char
lower = sat isLower

||| A Parser that matches against an uppercase letter
upper : Parser Char
upper = sat isUpper

||| A Parser that matches against an alphabetic character
alpha : Parser Char
alpha = sat isAlpha

||| A Parser that matches against an alphanumeric character
alphanum : Parser Char
alphanum = sat isAlphaNum

-- derived parsers

mutual
  export
  partial
  some : Parser a -> Parser (List a)
  some p = pure (::) <*> p <*> many p

  partial
  many : Parser a -> Parser (List a)
  many p = some p <|> pure []

||| A Parser that matches against whitespace
export
partial
space : Parser ()
space = do many (sat isSpace)
           pure ()

||| A Parser for a string of alphanumeric characters
partial
ident : Parser String
ident = do c <- item
           cs <- many alpha
           pure $ pack (c :: cs)

||| A Parser for an Nat value
partial
nat : Parser Nat
nat = do ns <- some digit
         pure (stringToNatOrZ (pack ns))

||| A Parser for an Int value
partial
int : Parser Int
int = do char '-'
         ns <- nat
         pure (-(cast ns))
      <|> do ns <- nat
             pure (cast ns)

||| A Parser that matches the supplied string
export
partial
string : String -> Parser String
string "" = pure ""
string cs = let (c :: cs) = unpack cs in
                do char c
                   string (pack cs)
                   pure $ pack (c :: cs)

-- higher-level parsers

||| A Parser that takes another Parser and handles spacing before and after
export
partial
token : Parser a -> Parser a
token p = do space
             v <- p
             space
             pure v

||| A Parser for an identifier
export
partial
identifier : Parser String
identifier = token ident

||| A Parser for a natural number
export
partial
natural : Parser Nat
natural = token nat

||| A Parser for an integer
export
partial
integer : Parser Int
integer = token int

||| A Parser for a string
export
partial
symbol : String -> Parser String
symbol cs = token (string cs)

That’s it! Well, of course, it’s not going to be as efficient or generic as Parsec, for instance, but it is excellent for edificational purposes.

Now let’s use this mini-library to define a parser-cum-evaluator for basic arithmetic expressions. Note that the only error handling provided is using the Maybe type family.
For any industrial strength parser-combinator library, error handling would be, I imagine, one of the most important aspects of the library.

module ArithExpr

import ParsCom

{-
  EBNF grammar for arithmetic expressions:

  expr ::= term (+ expr | - expr |  epsilon)
  term ::= factor (* term | / term | epsilon)
  factor ::= ( expr ) | integer
  integer ::= -2 | -1 | 0 | 1 | 2 | 3 ...

-}

mutual
  partial
  expr : Parser Int
  expr = do t <- term
            do symbol "+"
               e <- expr 
               pure (t + e) 
             <|> do symbol "-"
                    e <- expr
                    pure (t - e)
             <|> pure t

  partial
  term : Parser Int
  term = do f <- factor
            do symbol "*" 
               t <- term 
               pure (f * t)
             <|> do symbol "/" 
                    t <- term
                    pure (if t == 0 then 0 else f `div` t) 
             <|> pure f

  partial
  factor : Parser Int
  factor = do symbol "("
              e <- expr
              symbol ")"
              pure e
           <|> integer

export
partial
eval : String -> Maybe Int
eval inp = case parse expr inp of
                [(v, "")] => Just v
                _ => Nothing

And finally, the runner:

module ParsMain

import ArithExpr

partial
main : IO ()
main = do e <- getLine
          case eval e of 
               Just v => putStrLn (show v)
               Nothing => putStrLn "Invalid input"

Let’s take it for a spin!

~/dev/timmyjose.github.io/testing_ground/nzo$ idris2 -o ParsMain ParsMain.idr && rlwrap ./build/exec/ParsMain
1 + 2 * 3
7
~/dev/timmyjose.github.io/testing_ground/nzo$ idris2 -o ParsMain ParsMain.idr && rlwrap ./build/exec/ParsMain
(1 + 2) * 3
9
~/dev/timmyjose.github.io/testing_ground/nzo$ idris2 -o ParsMain ParsMain.idr && rlwrap ./build/exec/ParsMain
(12 / 2) * 3 + 3 * (12 / (1 + 3))
27
~/dev/timmyjose.github.io/testing_ground/nzo$ idris2 -o ParsMain ParsMain.idr && rlwrap ./build/exec/ParsMain
(1 + 2
Invalid input
~/dev/timmyjose.github.io/testing_ground/nzo$ idris2 -o ParsMain ParsMain.idr && rlwrap ./build/exec/ParsMain
12 / 0
0
~/dev/timmyjose.github.io/testing_ground/nzo$ idris2 -o ParsMain ParsMain.idr && rlwrap ./build/exec/ParsMain
12 - (100 / 10) / (20 / 5)
10
~/dev/timmyjose.github.io/testing_ground/nzo$ idris2 -o ParsMain ParsMain.idr && rlwrap ./build/exec/ParsMain
(100 / 20 / 4)
20

Some notes:

Compared to the Haskell version, there were a couple of minor adjustments I had to make:

1). Idris StringS are different from Haskell StringS, and hence all the packing and unpacking business.

2). The Alternative interface in Idris doesn’t have the some and many repetition functions as Haskell’s
Alternative typeclass does, and hence I had to handroll my own version.

3). Again, owing to the in-progress nature of Idris, evaluating even simple expressions in the REPL quickly became
extremely (and I mean extremely) slow. I had to finally resort to compiling the code and running it from ParsMain.
There is quite a lot of scope for performance improvement in Idris in this regard.

4). The totality checking of Idris really does help in many tangible ways – unlike in Haskell, it forces you to be more
deeply aware of your own code, and to be able to justify why your code is total and covering (or not).

Overall, I quite enjoyed writing it, perhaps even more so than the Haskell version! 🙂

Lazy primes in Idris

I thought it would be an interesting experiment to compare the generation of primes, lazily, in both Haskell and Idris.

Haskell has lazy evaluation by default, and Idris does support it via the Lazy and Force primitives, and infinite data structures
using Streams etc.

Here is the code in Haskell (adapted from Graham Hutton’s book, “Programming in Haskell” (2nd Edition)):

module Main where

primes :: [Int]
primes = sieve [2..]

sieve :: [Int] -> [Int]
sieve (p : xs) = p : filter (\x -> x `mod` p /= 0) (sieve xs)

main :: IO ()
main = do ns <- getLine
          let n = read ns
              ps = take n primes in
              do sequence_ [putStr $ show p ++ " " | p <- ps]

Testing it out:

~/dev/timmyjose.github.io/testing_ground$ ghc -O3 -o HPrimes Primes.hs && time ./HPrimes < input.in
Loaded package environment from /Users/z0ltan/.ghc/x86_64-darwin-8.10.1/environments/default
2 3 5 7 11 13 17 19 23 29 ... <output elided>

real    0m0.796s
user    0m0.775s
sys     0m0.009s

And here is the Idris version:

module Main 

import Data.Strings
import Data.Stream

-- for some reason, the Data.Stream module does not have 
-- this function built-in
filter : (a -> Bool) -> Stream a -> Stream a
filter p (x :: xs) = if p x 
                        then x :: filter p xs
                        else filter p xs

sieve : Stream Int -> Stream Int
sieve (p :: xs) = p :: filter (\x => x `mod` p /= 0) (sieve xs)

primes : Stream Int
primes = sieve (iterate (+1) 2)

main : IO ()
main = do ns <- getLine
          let n = stringToNatOrZ ns
          let ps = take n primes
          sequence_ [putStr $ show p ++ " " | p <- ps]

Running it:

~/dev/timmyjose.github.io/testing_ground$ idris2 -o IPrimes Primes.idr && time ./build/exec/IPrimes < input.in
2 3 5 7 11 13 17 19 23 29 ... <output elided>

real    0m0.712s
user    0m0.676s
sys     0m0.027s

The file input.in simply contains the number of primes to generate which is, in this case, 10000:

~/dev/timmyjose.github.io/testing_ground$ cat input.in
10000

Considering that Idris2 is still well before version 1.0, and is being worked on actively by a small number of core developers, it is still very impressive that Idris managed to get within the same order of performance!

Maybe a similar version written in ATS would be an interesting experiment!

EDIT: As pointed out by rmanne, the implementation was incorrect. I had mistakenly included the wrong version for both Haskell and Idris. The recursive
call to sieve is missing, and hence the massive performance figures due to it generating the completely incorrect output! Embarrassing mistake, and thanks to rmanne again!

With the fixed code, the input size has been cut down to 10000 to keep times under a second. Performance difference in this case is negligible between the Haskell and Idris version as can be
seen in the updated figures.

Basic Matrix operations in Idris

I had tried Idris some time back, and while I liked it, I didn’t follow through with it. One major reason was the fact that Idris’ focus appeared to be purely on research despite
marketing itself as a language for programmers. There is a bit of contradiction in that statement. Of late, however, especially with the ongoing rewrite of Idris in Idris (Idris2), as well as support for Linear Types, the general feeling appears to be that Idris2 is geared not only towards research but also for industry programming (there is still some way to goin this respect though).

Given that I am investing in ATS, which also has powerful support for Dependent Types as well as Linear Types, and quite a bit of theorem proving (albeit more on the imperative side), coupled with my longterm interest in Compilers, I decided to learn Idris and ATS together, with a special focus on creating compilers for my own languages. Compilers and Programming Languages are very appealing to me, always have been, and I have decided to invest in them for the long haul.

As part of restarting my study of Idris, I am working through the official book by Idris’ creator, Edwin Brady – “Type driven development with Idris”, which is still valid (with minor changes). This book does not contain any material on Linear Types, of course, but that’s where the official docs will come in handy.

I recall last time that I’d got stuck on the matrix multiplication example in the TDD book (and skipped it), and this time I decided to get over the hump for good.

So here is a small module with some very basic matrix operations, all runnable in Idris2.

module Matrix

import Data.Vect

%default total

||| Add two matrices together
addMatrix : Num elem => Vect m (Vect n elem) -> Vect m (Vect n elem) -> Vect m (Vect n elem)
addMatrix [] [] = []
addMatrix (x :: xs) (y :: ys) = zipWith (+) x y :: addMatrix xs ys

||| Subtract the second matrix from the first
subMatrix : (Neg elem, Num elem) => Vect m (Vect n elem) -> Vect m (Vect n elem) -> Vect m (Vect n elem)
subMatrix [] [] = []
subMatrix (x :: xs) (y :: ys) = zipWith (-) x y :: subMatrix xs ys

||| Transpose a matrix
transposeMatrix : { n : _ } -> Vect m (Vect n elem) -> Vect n (Vect m elem)
transposeMatrix [] = replicate n []
transposeMatrix (x :: xs) = let xsTrans = transposeMatrix xs in
                                zipWith (::) x xsTrans

||| Multiply two matrices together
multiplyMatrix : Num elem => { m, n, o : _ } -> Vect m (Vect n elem) -> Vect n (Vect o elem) -> Vect m (Vect o elem)
multiplyMatrix xs ys = multiply xs (transposeMatrix ys)
  where
    dotProduct : { n : _ } -> Vect n elem -> Vect n elem -> elem
    dotProduct [] [] = 0
    dotProduct (x :: xs) (y :: ys) = x * y + dotProduct xs ys

    multHelper : { n, o : _ } -> Vect n elem -> Vect o (Vect n elem) -> Vect o elem
    multHelper _ [] = []
    multHelper x (y :: ys) = dotProduct x y :: multHelper x ys

    multiply : { m, n, o : _ } -> Vect m (Vect n elem) -> Vect o (Vect n elem) -> Vect m (Vect o elem)
    multiply [] _ = []
    multiply (x :: xs) ys = multHelper x ys :: multiply xs ys

Testing it out:

Matrix> addMatrix [[1, 2, 3], [4, 5, 6]] [[2, 1, 3], [6, 5, 4]]
[[3, 3, 6], [10, 10, 10]]

Matrix> subMatrix [[1, 2, 3], [4, 5, 6]] [[2, 1, 3], [6, 5, 4]]
[[-1, 1, 0], [-2, 0, 2]]

Matrix> multiplyMatrix [[1, 2], [3, 4], [5, 6]] [[1, 2, 3, 4], [2, 3, 4, 5]]
[[5, 8, 11, 14], [11, 18, 25, 32], [17, 28, 39, 50]]

Matrix> transposeMatrix [[1, 2], [3, 4], [5, 6], [7, 8]]
[[1, 3, 5, 7], [2, 4, 6, 8]]

Epilogue: One nice thing that I’d not observed before, and which appears blatantly obvious now, is how the use of dependent types makes pattern matching much simpler. For instance, in the addMatrix example, we don’t have to consider every combination of the two matrices for the function to be total, since the dependent types ensure that the dimensions always
match up!

Note, however, also the extra verbosity in the type signatures due to the inclusion of the concept of “multiplicities” in Idris2. This means that implicit variables in Idris now havea multiplicity of 0, and hence must be explicitly introduced into scope to be used in the local context. This is especially amplified when the definitions are local, as in this case. If the local functions in multiplyMatrix were lifted to the top-level, it would simplify the type signature to a considerable extent.

A simple file copying example in ATS

The more I learn of ATS, the more I’m fascinated by it. Notwithstanding the talk which pokes sufficient (light-hearted) fun at ATS, I actually find it very logical, including the naming and organisation of files, libraries, and concepts.
After the initial get-go, it’s been a veritable pleasure learning ATS.

I’m halfway through the first book, and there are a few more to complete, but I can see myself using ATS for a wide variety of projects – all the way from low-level programming to the very highest abstractions.

Here is a simple program which copies the input file to the output file. Note the use of strptr_free which is required by the ATS tupe checker. Omitting this would lead to a compile-time error since the value returned by fileref_get_line_string is a linear type (of string). Very nice!

#include "share/atspre_staload.hats"

fn
copy_file (
  inpath: string,
  outpath: string
    ): void = 
    let val infil_ref = fileref_open_exn (inpath, file_mode_r)
        val outfil_ref = fileref_open_exn (outpath, file_mode_w)
        fun
       loop (
        infil_ref: FILEref,
        outfil_ref: FILEref
           ): void = 
           if fileref_isnot_eof (infil_ref) then
               let val line = fileref_get_line_string (infil_ref)
                   val () = fprint (outfil_ref, line)
                   val () = fprint_newline (outfil_ref)
                   val () = strptr_free (line)
               in
                loop (infil_ref, outfil_ref)
               end
    in
      loop (infil_ref, outfil_ref);
      fileref_close (infil_ref);
      fileref_close (outfil_ref)
    end

implement main0 () = 
  copy_file ("hamlet.in", "hamlet.out")

Testing it out:

$ cat hamlet.in
To be, or not to be. That is the question!
Exeunt.

$ patscc -DATS_MEMALLOC_LIBC -flto -cleanaft -O3 -latslib -o copyfile copyfile.dats && ./copyfile

$ cat hamlet.out
To be, or not to be. That is the question!
Exeunt.

A line number closure implementation in ATS

This is an implementation, in ATS, of one of my favourite exercises in closures – a line-number printing closure.

For reference, the Rust version is given first, and then the same in ATS, whih has a unique flavour of its own.

Here is the Rust version:

fn linum() -> impl FnMut() -> () {
    let mut line = 0;

    Box::new(move || {
        line = line + 1;
        println!("Current line number is {}", line);
    })
}

fn main() {
    let mut l0 = linum();
    for _ in 0..5 {
        l0();
    }

    l0 = linum();
    l0();
    l0();
    l0();
}

Running it:

$ rustc -O linum.rs && ./linum
Current line number is 1
Current line number is 2
Current line number is 3
Current line number is 4
Current line number is 5
Current line number is 1
Current line number is 2
Current line number is 3

And here is the same in ATS:

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

fn
linum () :<cloref1> () -<cloref1> void = 
  let val line = ref<int> (0)
  in
    lam () =<cloref1> (
      !line := !line + 1;
      println! ("Current line number is ", !line)
    )
  end

fun loop (li0: () -<cloref1> void, n: int): void = 
  if n > 0 then (li0 (); loop (li0, n - 1))

implement main0 () = {
  val li0 = linum ();
  val () = loop (li0, 5)

  val li0 = linum ()
  val () = li0 ()
  val () = li0 ()
  val () = li0 ()
}

Testing it out:

$ patscc -DATS_MEMALLOC_LIBC -O3 -o linum linum.dats && ./linum
Current line number is 1
Current line number is 2
Current line number is 3
Current line number is 4
Current line number is 5
Current line number is 1
Current line number is 2
Current line number is 3

Merge Sort in ATS

A simple, functional merge sort implementation for a custom list type in ATS:

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

(* our custom list data type *)
datatype
list0 (a: t@ype) =
  | list0_nil (a) of ()
  | list0_cons (a) of (a, list0 (a)) 

(* helper function to print out an int list *)
fun
print_int_list (xs: list0 (int)): void = 
  case+ xs of
    | list0_nil () => print_newline ()
    | list0_cons (x, xs) => (
      print! (x, " ");
      print_int_list (xs)
    )

fun
{a: t@ype}
list0_length (xs: list0 (a)): int = 
  case+ xs of
    | list0_nil () => 0
    | list0_cons (_, xs) => 1 + list0_length (xs)

(* return a list of the first n items of the list *)
fun
{a: t@ype}
list0_take (
  n: int,
  xs: list0 (a)
    ): list0 (a) = 
  case+ xs of
    | list0_nil () => list0_nil ()
    | list0_cons (x, xs) => 
        ifcase
          | n = 0 => list0_nil ()
          | _ => list0_cons (x, list0_take (n - 1, xs))

(* return the list with the first n items dropped *)
fun
{a: t@ype}
list0_drop (
  n: int,
  xs: list0 (a)
    ): list0 (a) = 
    case+ xs of
      | list0_nil () => list0_nil ()
      | list0_cons (x, xs) =>
        ifcase
          | n = 0 => list0_cons (x, xs)
          | _ => list0_drop (n - 1, xs)

typedef
cmp (a: t@ype) = (a, a) -> bool

(* merge two ordered lists into a single ordered list *)
fun
{a: t@ype}
list0_merge (
  cmp: cmp (a),
  xs: list0 (a),
  ys: list0 (a)
    ): list0 (a) =
    case+ (xs, ys) of
      | (list0_cons (x, xs), list0_cons (y, ys)) => 
          if cmp (x, y) then
            list0_cons (x, list0_merge (cmp, xs, list0_cons (y, ys)))
          else
            list0_cons (y, list0_merge (cmp, list0_cons (x, xs), ys))
      | (list0_nil (), ys) => ys
      | (xs, list0_nil ()) => xs

(* mergesort for our custom list type *)
fun
{a: t@ype}
list0_mergesort (
  cmp: cmp (a),
  xs: list0 (a)
    ): list0 (a) = 
    ifcase
      | list0_length (xs) = 1 => xs
       | _ => list0_merge (cmp, list0_mergesort (cmp, left), list0_mergesort (cmp, right)) where {
         val n = list0_length (xs) / 2
         val left = list0_take (n, xs)
         val right = list0_drop (n, xs)
       }

implement main0 () = {
  val li0 = list0_cons (1, 
            list0_cons (100, 
            list0_cons (~10, 
            list0_cons (12, 
            list0_cons (3, 
            list0_cons (~212, 
            list0_cons (0, 
            list0_cons (11, 
            list0_cons (~99, 
            list0_cons (0,
            list0_cons (1, 
            list0_cons (1, list0_nil ()))))))))))))
  val () = print_int_list (li0)

  val sorted_list_asc = list0_mergesort<int> (lam (x, y) => x <= y, li0)
  val () = print_int_list (sorted_list_asc)

  val sorted_list_desc = list0_mergesort<int> (lam (x, y) => x >= y, li0)
  val () = print_int_list (sorted_list_desc)

  val el0 = list0_nil ()
  val sel0 = list0_mergesort<int> (lam (x, y) => x <= y, el0)
  val () = print_int_list (sel0)

  val el1 = list0_cons (1, list0_nil ())
  val sel1 = list0_mergesort<int> (lam (x, y) => x <= y, el1)
  val () = print_int_list (sel1)

  val el2 = list0_cons (100, list0_cons (~99, list0_nil ()))
  val sel2 = list0_mergesort<int> (lam (x, y) => x >= y, el2)
  val () = print_int_list (el2)
}

Testing it out:

$ patscc -D_GNU_SOURCE -DATS_MEMALLOC_LIBC -O3 -o mergesort mergesort.dats

$ ./mergesort
1 100 -10 12 3 -212 0 11 -99 0 1 1
-212 -99 -10 0 0 1 1 1 3 11 12 100
100 12 11 3 1 1 1 0 0 -10 -99 -212

1
100 -99

Generic BST in ATS

The more I learn ATS, the more I love it. Never mind the naysayers and the detractors who claim it is an illogically complex language. So far, I’ve found it to be a very
logical and relatively consistent language. It also seems like a very intuitive language once you get the hang of the patterns in the language. Furthermore, it seems like a
very good candidate for writing compilers in with its excellent support of Algebraic Data Types, and of generics (templates).

The community is still small, but quite helpful and proactive. Queries on the Google groups are answered with alacrity, and the people
seem very technology-focused, which is always a good sign of a healthy software community.

The error messages in ATS can be a bit messy, and hopefully this will be addressed in future versions, but the following tool, recommended by Richard from the ATS lang Google group is quite helpful – ats-acc. It formats the error messages quite nicely, and also gives a nice indication of the line where the error was triggered. This has made life so much easier for me.

As a general exercise, I wanted to extend the BST example given in the official tutorials, and using the excellent ifcase suggestion by the creator of ATS himself, Hongwei Xi, here is the annotated version of the code. It should be pretty much self-explanatory:

NOTE: a: t@ype indicates a generic type/typeclass constraint. And the {a: t@type} syntax before the function name is how template types are introduced in ATS.

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

(* A generic binary search tree type *)
datatype
bstree (a: t@ype) = 
  | E of ()
  | B of (bstree (a), a, bstree (a))

(* insert a value into the bst, maintaining bst properties *)
fun
{a: t@ype}
insert (t0: bstree (a), k0: a): bstree (a) = 
  case+ t0 of
    | E () => B (E (), k0, E ())
    | B (t1, k, t2) => 
      let val sgn = gcompare_val_val<a>(k0, k)
      in ifcase
         | sgn < 0 => B (insert (t1, k0), k, t2) 
         | sgn > 0 => B (t1, k, insert (t2, k0))
         | _ => t0
      end

(* search for a value in the bst *)
fun
{a: t@ype}
search (t0: bstree (a), k0: a): bool = 
  case+ t0 of
    | E () => false
    | B (t1, k, t2) =>
      let val sgn = gcompare_val_val<a>(k0, k)
      in ifcase
          | sgn < 0 => search (t1, k0)
          | sgn > 0 => search (t2, k0)
          | _ => true
      end

(* pre-order traversal with a custom callback function *)
fun
{a: t@ype}
preorder (t0: bstree (a), fwork: a -<cloref1> void): void = 
  case+ t0 of
    | E () => ()
    | B (t1, k, t2) => {
        val () = fwork (k)
        val () = preorder (t1, fwork)
        val () = preorder (t2, fwork)
    }

(* in-order traversal with a custom callback function *)
fun
{a: t@ype}
inorder (t0: bstree (a), fwork: a -<cloref1> void): void = 
  case+ t0 of
    | E () => ()
    | B (t1, k, t2) => {
        val () = inorder (t1, fwork)
        val () = fwork (k)
        val () = inorder (t2, fwork)
    }

(* post-order traversal with a custom callback function *)
fun
{a: t@ype}
postorder (t0: bstree (a), fwork: a -<cloref1> void): void = 
  case+ t0 of
    | E () => ()
    | B (t1, k, t2) => {
        val () = postorder (t1, fwork)
        val () = postorder (t2, fwork)
        val () = fwork (k)
    }

implement main0 () = {
  val ti0: bstree (int) = E ()
  val ti0 = insert (ti0, 10)
  val ti0 = insert (ti0, 1)
  val ti0 = insert (ti0, 2)
  val ti0 = insert (ti0, 11)
  val ti0 = insert (ti0, 3)
  val ti0 = insert (ti0, 3)
  val ti0 = insert (ti0, 5)
  val () = preorder (ti0, lam k => print! (k, " "))
  val () = println! ()
  val () = inorder (ti0, lam k => print! (k, " "))
  val () = println! ()
  val () = postorder (ti0, lam k => print! (k, " "))
  val () = println! ()
  val () = assertloc (search (ti0, 11))
  val () = assertloc (search (ti0, 100) = false)

  val si0: bstree (string) = E ()
  val si0 = insert (si0, "hello")
  val si0 = insert (si0, "world")
  val si0 = insert (si0, "nice")
  val si0 = insert (si0, "to")
  val si0 = insert (si0, "meet")
  val si0 = insert (si0, "you")
  val si0 = insert (si0, "again")
  val () = preorder (si0, lam k => print! (k, " "))
  val () = println! ()
  val () = inorder (si0, lam k => print! (k, " "))
  val () = println! ()
  val () = postorder (si0, lam k => print! (k, " "))
  val () = println! ()
  val () = assertloc (search (si0, "hello"))
  val () = assertloc (search (si0, "hallo") = false)
}

Testing it out:

$ patscc -DATS_MEMALLOC_LIBC -o gen_tree gen_tree.dats && ./gen_tree
10 1 2 3 5 11
1 2 3 5 10 11
5 3 2 1 11 10
hello again world nice meet to you
again hello meet nice to world you
again meet to nice you world hello