Factor is a programming language I've written about before and in the early days of Factor development I wrote a number of libraries and contributed to development. It's been a while since I've contributed but I still use Factor. The development environment has a very Smalltalk-like feel to it and it includes full documentation and browseable source code of libraries.
This post isn't about Factor the language, but is about some of the neat fun libraries that people have written that shows off the graphical development system a bit.
The first example is an implementation of the game Minesweeper in Factor. A blog post by the author explains the implementation. To run it inside Factor, do the following:
"minesweeper" run
A new window will open showing the game. Help can be shown with:
"minesweeper" help
Another fun example is displaying XKCD comics inside the Factor REPL. The implementation is explained by the author here.
USE: xkcd
latest-xkcd.
...comic displayed here...
random-xkcd.
...comic displayed here...
If it seems like all the examples I'm using are from the excellent re-factor blog - well, most of them are. This blog post from re-factor shows pulling historical facts from Wikipedia:
USE: wikipedia
USE: calendar
today historical-events.
...a list of historical events from wikipedia for today...
yesterday historical-births.
...a list of historical births from wikipedia for yesterday...
5 weeks ago historical-deaths.
...a list of historical deaths from wikipedia for five weeks ago...
The items in the list are graphical elements that can be manipulated. Left clicking on the coloured words will open a URL in the default web browser. Right clicking allows you to push the element on the Factor stack and manipulate it.
The calendar vocab has a lot of interesting words that allow doing calculations like "5 weeks ago".
There's a hacker-news vocabulary that provides words to list current articles on the Hacker News website. Like the previous Wikipedia example, the graphical elements are clickable objects:
USE: hacker-news
hacker-news-top.
...list of top articles...
hacker-news-show.
...list articles related to showing projects...
A number of years ago I wrote a CPU 8080 emulator in Factor and used this to implement a Space Invaders Emulator and then emulators for a couple of other 8080 arcade games, Balloon Bomber and Lunar Rescue. These examples require the original arcade ROMs and instructions for using them are in the online help:
"rom.space-invaders" run
...opens in a new window...
"rom.balloon-bomber" run
...opens in a new window...
"rom.lunar-rescue" run
...opens in a new window...
"rom.space-invaders" help
...displays help...
Another magical implementation from the re-factor blog, a Gopher server and a graphical Gopher Client. This is a video I made of the gopher client on YouTube:
I also did a video that shows some Factor development tools on the running Gopher client to show how everything is live in Factor:
There's much more buried inside Factor. The list of articles and list of vocabularies from the online help is a good way to explore. This help system is also available offline in a Factor install. By default many libraries aren't loaded when Factor starts but you can force loading everything using load-all
:
load-all
...all vocabs are loaded - prepare to wait for a while...
save
...saves the image so when factor is restarted the vocabs remain loaded...
The benefit of doing this while developing is all the online help, source and words are available via the inbuilt tools like "apropos", "usage", etc.
The Shen programming language has an extensible type system. Types are defined using sequent calculus and the system is powerful enough to create a variety of exotic types but it can be difficult when first starting with Shen to know how to use that power. In this post I hope to go through some basic examples of defining types in Shen without needing to know too much sequent calculus details.
For an overview of Shen there is Shen in 15 minutes and the Shen OS Kernel Manual. An interactive JavaScript REPL exists to try examples in the browser or pick on one of the existing Shen language ports. For these examples I'm using my Wasp Lisp port of Shen.
Shen is optionally typed. The type checker can be turned off and on. By default it is off and this can be seen in the Shen prompt by the presence of a '-
' character:
(0-) ...shen code...
Turning type checking on is done by using (tc +)
. The '-
' in the prompt changes to a '+
' to show type checking is active. It can be turned off again with (tc -)
:
(0-) (tc +)
(1+) (tc -)
(2-) ...
Types in Shen are defined using datatype
. The body of the datatype
definition contains a series of sequent calculus rules. These rules define how an object in Shen can be proved to belong to a particular type. Rather than go through a detailed description of sequent calculus, I'm going to present common examples of types in Shen to learn by example and dive into details as needed. There's the Shen Language Book for much more detail if needed.
One way of storing collections of data in Shen is to use lists or vectors. For example, given an the concept of a 'person' that has a name and age, this can be stored in a list with functions to get the relevent data:
(tc -)
(define make-person
Name Age -> [Name Age])
(define get-name
[Name Age] -> Name)
(define get-age
[Name Age] -> Age)
(get-age (make-person "Person1" 42))
=> 42
In the typed subset of Shen we can define a type for this person object using datatype
:
(datatype person
N : string; A : number;
_______________________
[N A] : person;)
This defines one sequent calculus rule. The way to read it is starting with the code below the underscore line, followed by the code above it. In this case the rule states that if an expression matching the pattern [N A]
is encountered, where N
is a string
and A
is a number, then type that expression as person
. With that rule defined, we can ask Shen if lists are of the type person
:
(0+) ["Person" 42] : person
["Person1" 42] : person
(1+) ["Person1" "Person1"] : person
[error shen "type error"]
(2+) ["Person 42"]
["Person1" 42] : person
Given this person
type, we might write a get-age
function that is typed such that it only works on person
objects as follows (The { ...}
syntax in function definitions provides the expected type of the function):
(define get-age
{ person --> number }
[N A] -> A)
[error shen "type error in rule 1 of get-age"]
Shen rejects this definition as not being type safe. The reason for this is because our datatype
definition only states that [N A]
is a person
if N
is a string
and A
is a number
. It does not state that a person
object is constructed only of a string
and number
. For example, we could have an additional definition as follows:
(datatype person2
N : string; A : string;
_______________________
[N A] : person;)
Now we can create different types of person
objects:
(0+) ["Person" 42 ] : person
["Person" 42] : person
(1+) ["Person" "young"] : person
["Person" "young"] : person
get-age
is obviously badly typed in the presence of this additional type of person
which is why Shen rejected it originally. To resolve this we need to tell Shen that an [N A]
is a person
if and only if N
is a string
and A
is a person
. This is done with what is called a 'left rule'. Such a rule defines how a person
object can be deconstructed. It looks like this:
(datatype person3
N : string, A: number >> P;
___________________________
[N A] : person >> P;)
The way to read this type of rule is that, if [N A]
is a person
then N
is a string
and A
is a number. With that loaded into Shen, get-age
type checks:
(define get-age
{ person --> number }
[N A] -> A)
get-age : (person --> number)
(0+) (get-age ["Person" 42])
42 : number
The need to create a left rule, dual to the right rule, is common enough that Shen has a short method of defining both in one definition. It looks like this - note the use of '=' instead of '_' in the separator line:
(datatype person
N : string; A : number;
=======================
[N A] : person;)
(define get-age
{ person --> number }
[N A] -> A)
get-age : (person --> number)
(0+) (get-age ["Person" 42])
42 : number
The above datatype
is equivalent to declaring the two rules:
(datatype person
N : string; A : number;
_______________________
[N A] : person;
N : string, A: number >> P;
___________________________
[N A] : person >> P;)
When progamming at the REPL of Shen it's common to create datatype
definitions that are no longer needed, or part of a line of thought you don't want to pursue. Shen provides ways of excluding or including rules in the typechecker as needed. When defining a set of rules in a datatype
, that datatype
is given a name:
(datatype this-is-the-name
...
)
The rules within that definition can be removed from selection by the typechecker using preclude
, which takes a list of datatype
names to ignore during type checking:
(preclude [this-is-the-name])
To re-add a dataype
, use include
:
(include [this-is-the-name])
There is also include-all-but
and preclude-all-but
to include or remove all but the listed names. These commands are useful for removing definitions you no longer want to use at the REPL, but also for speeding up type checking in a given file if you know the file only uses a particular set of datatypes.
An example of an enumeration type would be days of the week. In an ML style language this can be done like:
datatype days = monday | tuesday | wednesday
| thursday | friday | saturday | sunday
In Shen this would be done using multiple sequent calculus rules.
(datatype days
____________
monday : day;
____________
tuesday : day;
____________
wednesday : day;
____________
thursday : day;
____________
friday : day;
____________
saturday : day;
____________
sunday : day;)
Here there are no rules above the dashed underscore line, meaning that the given symbol is of the type day
. A function that uses this type would look like:
(define day-number
{ day --> number }
monday -> 0
tuesday -> 1
wednesday -> 2
thursday -> 3
friday -> 4
saturday -> 5
sunday -> 6)
It's quite verbose to define a number of enumeration types like this. It's possible to add a test above the dashed underline which allows being more concise. The test is introduced using if
:
(datatype days
if (element? Day [monday tuesday wednesday thursday friday saturday sunday])
____________________________________________________________________________
Day : day;)
(0+) monday : day
monday : day
Any Shen code can be used in these test conditions. Multiple tests can be combined:
(datatype more-tests
if (number? X)
if (>= X 5)
if (<= X 10)
___________
X : between-5-and-10;)
(2+) 5 : between-5-and-10
5 : between-5-and-10
(3+) 4 : between-5-and-10
[error shen "type error\n"]
To create types that are polymorphic (ie. generic), like the built-in list
type, include a free variable representing the type. For example, something like the built in list where the list elements are stored as pairs can be approximated with:
(datatype my-list
_____________________
my-nil : (my-list A);
X : A; Y : (my-list A);
========================
(@p X Y) : (my-list A);)
(define my-cons
{ A --> (my-list A) --> (my-list A) }
X Y -> (@p X Y))
(0+) (my-cons 1 my-nil)
(@p 1 my-nil) : (my-list number)
(1+) (my-cons 1 (my-cons 2 my-nil))
(@p 1 (@p 2 my-nil)) : (my-list number)
(2+) (my-cons "a" (my-cons "b" my-nil))
(@p "a" (@p "b" my-nil)) : (my-list string)
Notice the use of the '=====' rule to combine left and right rules. This is required to enable writing something like my-car
which requires proving that the type of the car
of the list is of type A
:
(define my-car
{ (my-list A) --> A }
(@p X Y) -> X)
Using peano numbers we can create a list where the length of the list is part of the type:
(datatype list-n
______
[] : (list-n zero A);
X : A; Y : (list-n N A);
================================
[ X | Y ] : (list-n (succ N) A);)
(define my-tail
{ (list-n (succ N) A) --> (list-n N A) }
[Hd | Tl] -> Tl)
(define my-head
{ (list-n (succ N) A) --> A }
[Hd | Tl] -> Hd)
This gives a typesafe head
and tail
operation whereby they can't be called on an empty list:
(0+) [] : (list-n zero number)
[] : (list-n zero number)
(1+) [1] : (list-n (succ zero) number)
[1] : (list-n (succ zero) number)
(2+) (my-head [])
[error shen "type error\n"]
(3+) (my-head [1])
1 : number
(4+) (my-tail [1 2 3])
[2 3] : (list-n (succ (succ zero)) number)
(5+) (my-tail [])
[error shen "type error\n"]
Shen gives a lot of power in creating types, but trusts you to make those types consistent. For example, the following creates an inconsistent type:
(datatype person
N : string; A : number;
_______________________
[N A] : person;
N : string; A : string;
_______________________
[N A] : person;
N : string, A: number >> P;
___________________________
[N A] : person >> P;)
Here we are telling Shen that a string
and number
in a list
is a person
, and so too is a string
and another string
. But the third rule states that given a person
, that is is composed of a string
and a number
only. This leads to:
(0+) (get-age ["Person" "Person"])
...
This will hang for a long time as Shen attempts to resolve the error we've created.
Shen provides a programmable type system, but the responsibility lies on the programmer for making sure the types are consisitent. The examples given here provide a brief overview. For much more see The Book of Shen. The Shen OS Kernel Manual also gives some examples. There are posts on the Shen Mailing List that have more advanced examples of Shen types. Mark Tarver has a case study showing converting a lisp interpreter in Shen to use types.
Mercury is a logic programming language, similar to Prolog, but with static types. It feels like a combination of SML and Prolog at times. It was designed to help with programming large systems - that is large programs, large teams and better reliability, etc. The commercial product Prince XML is written in Mercury.
I've played around with Mercury in the past but haven't done anything substantial with it. Recently I picked it up again. This post is a short introduction to building Mercury, and some example "Hello World" style programs to test the install.
Mercury is written in the Mercury language itself. This means it needs a Mercury compiler to bootstrap from. The way I got a build going from source was to download the source for a release of the day version, build that, then use that build to build the Mercury source from github. The steps are outlined in the README.bootstrap file, but the following commands are the basic steps:
$ wget http://dl.mercurylang.org/rotd/mercury-srcdist-rotd-2019-06-22.tar.gz
$ tar xvf mercury-srcdist-rotd-2019-06-22.tar.gz
$ cd mercury-srcdist-rotd-2019-06-22
$ ./configure --enable-minimal-install --prefix=/tmp/mercury
$ make
$ make install
$ cd ..
$ export PATH=/tmp/mercury/bin:$PATH
With this minimal compiler the main source can be built. Mercury has a number of backends, called 'grades' in the documentation. Each of these grades makes a number of tradeoffs in terms of generated code. They define the platform (C, assembler, Java, etc), whether GC is used, what type of threading model is available (if any), etc. The Adventures in Mercury blog has an article on some of the different grades. Building all of them can take a long time - multiple hours - so it pays to limit it if you don't need some of the backends.
For my purposes I didn't need the CSharp backend, but wanted to
explore the others. I was ok with the time tradeoff of building the
system. To build from the master
branch of the github repository I
did the following steps:
$ git clone https://github.com/Mercury-Language/mercury
$ cd mercury
$ ./prepare.sh
$ ./configure --enable-nogc-grades --disable-csharp-grade \
--prefix=/home/myuser/mercury
$ make PARALLEL=-j4
$ make install PARALLEL=-j4
$ export PATH=/home/myuser/mercury/bin:$PATH
Change the prefix
to where you want Mercury installed. Add the
relevant directories to the PATH as specified by the end of the build
process.
A basic "Hello World" program in Mercury looks like the following:
:- module hello.
:- interface.
:- import_module io.
:- pred main(io, io).
:- mode main(di, uo) is det.
:- implementation.
main(IO0, IO1) :-
io.write_string("Hello World!\n", IO0, IO1).
With this code in a hello.m
file, it can be built and run with:
$ mmc --make hello
Making Mercury/int3s/hello.int3
Making Mercury/ints/hello.int
Making Mercury/cs/hello.c
Making Mercury/os/hello.o
Making hello
$ ./hello
Hello World!
The first line defines the name of the module:
:- module hello.
Following that is the definitions of the public interface of the module:
:- interface.
:- import_module io.
:- pred main(io, io).
:- mode main(di, uo) is det.
We publically import the io
module, as we use io
definitions in
the main
predicate. This is followed by a declaration of the
interface of main
- like C this is the user function called by the
runtime to execute the program. The definition here declares that
main
is a predicate, it takes two arguments, of type io
. This is a
special type that represents the "state of the world" and is how I/O
is handled in Mercury. The first argument is the "input world state"
and the second argument is the "output world state". All I/O functions
take these two arguments - the state of the world before the function
and the state of the world after.
The mode
line declares aspects of a predicate related to the logic
programming side of things. In this case we declare that the two
arguments passed to main
have the "destructive input" mode and the
"unique output" mode respectively. These modes operate similar to how
linear types work in other languages, and the reference manual has a
section describing
them. For
now the details can be ignored. The is det
portion identifies the
function as being deterministic. It always succeeds, doesn't backtrack
and only has one result.
The remaining code is the implementation. In this case it's just the implementation of the main
function:
main(IO0, IO1) :-
io.write_string("Hello World!\n", IO0, IO1).
The two arguments to main
, are the io
types representing the before and after representation of the world. We call write_string
to display a string, passing it the input world state, IO0
and receiving the new world state in IO1
. If we wanted to call an additional output function we'd need to thread these variables, passing the obtained output state as the input to the new function, and receiving a new output state. For example:
main(IO0, IO1) :-
io.write_string("Hello World!\n", IO0, IO1),
io.write_string("Hello Again!\n", IO1, IO2).
This state threading can be tedious, especially when refactoring - the need to renumber or rename variables is a pain point. Mercury has syntactic sugar for this called state variables, enabling this function to be written like this:
main(!IO) :-
io.write_string("Hello World!\n", !IO),
io.write_string("Hello Again!\n", !IO).
When the compiler sees !Variable_name
in an argument list it creates two arguments with automatically generated names as needed.
Another syntactic short cut can be done in the pred
and mode
lines. They can be combined into one line that looks like:
:- pred main(io::di, io::uo) is det.
Here the modes di
and uo
are appended to the type prefixed with a ::
. The resulting program looks like:
- module hello.
:- interface.
:- import_module io.
:- pred main(io::di, io::uo) is det.
:- implementation.
main(!IO) :-
io.write_string("Hello World!\n", !IO),
io.write_string("Hello Again!\n", !IO).
The following is an implementation of factorial:
:- module fact.
:- interface.
:- import_module io.
:- pred main(io::di, io::uo) is det.
:- implementation.
:- import_module int.
:- pred fact(int::in, int::out) is det.
fact(N, X) :-
( N = 1 -> X = 1 ; fact(N - 1, X0), X = N * X0 ).
main(!IO) :-
fact(5, X),
io.print("fact(5, ", !IO),
io.print(X, !IO),
io.print(")\n", !IO).
In the implementation section here we import the int
module
to access functions across machine integers. The fact
predicate is
declared to take two arguments, both of type int
, the first an input
argument and the second an output argument.
The definition of fact
uses Prolog syntax for an if/then
statement. It states that if N
is 1
then (the ->
token) the
output variable, X
is 1
. Otherwise (the ;
token), calculate the
factorial recursively using an intermediate variable X0
to hold the
temporary result.
There's a few other ways this could be written. Instead of the Prolog style if/then, we can use an if/then syntax that Mercury has:
fact(N, X) :-
( if N = 1 then X = 1 else fact(N - 1, X0), X = N * X0 ).
Instead of using predicates we can declare fact
to be a function. A function has no output variables, instead it returns a result just like functions in standard functional programming languages. The changes for this are to declare it as a function:
:- func fact(int) = int.
fact(N) = X :-
( if N = 1 then X = 1 else X = N * fact(N - 1) ).
main(!IO) :-
io.print("fact(5, ", !IO),
io.print(fact(5), !IO),
io.print(")\n", !IO)
Notice now that the call to fact
looks like a standard function call and is inlined into the print
call in main
. A final syntactic shortening of function implementations enables removing the X
return variable name and returning directly:
fact(N) = (if N = 1 then 1 else N * fact(N - 1)).
Because this implementation uses machine integers it won't work for values that can overflow. Mercury comes with an arbitrary precision integer module, integer, that allows larger factorials. Replacing the use of the int
module with integer
and converting the static integer numbers is all that is needed:
:- module fact.
:- interface.
:- import_module io.
:- pred main(io::di, io::uo) is det.
:- implementation.
:- import_module integer.
:- func fact(integer) = integer.
fact(N) = (if N = one then one else N * fact(N - one)).
main(!IO) :-
io.print("fact(1000, ", !IO),
io.print(fact(integer(1000)), !IO),
io.print(")\n", !IO).
There's a lot more to Mercury. These are just first steps to test the system works. I'll write more about it in later posts. Some further reading:
The ATS programming language supports defining Generalized Algebraic Data Types (GADTS). They allow defining datatypes where the constructors for the datatype are explicitly defined by the programmer. This has a number of uses and I'll go through some examples in this post. GADTs are sometimes referred to as Guarded Recursive Datatypes.
Some useful resources for reading up on GADTs that I used to write this post are:
The examples here were tested with ATS2-0.3.11.
This is probably the most common demonstration of GADT usage and it's useful to see how to do it in ATS. The example is taken from the Haskell/GADT Wikibook.
First we'll create datatype to represent a simple expression language, and write an evaluation function for it, without using GADTs:
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"
datatype Expr =
| I of int
| Add of (Expr, Expr)
| Mul of (Expr, Expr)
fun eval (x:Expr): int =
case+ x of
| I i => i
| Add (t1, t2) => eval(t1) + eval(t2)
| Mul (t1, t2) => eval(t1) * eval(t2)
implement main0() = let
val term = Mul(I(2), I(4))
val res = eval(term)
in
println!("res=", res)
end
Expr
is a datatype with three constructors. I
represents an
integer, Add
adds two expressions together and Mul
multiples two
expressions. The eval
function pattern matches on these and
evaluates them. The example can be compiled with the following if
placed in a file arith1.dats
:
$ patscc -DATS_MEMALLOC_LIBC -o arith1 arith1.dats
$ ./arith1
res=8
Now we extend the expression language with another type, booleans, and
add an Expr
constructor to compare for equality:
datatype Expr =
| I of int
| B of bool
| Add of (Expr, Expr)
| Mul of (Expr, Expr)
| Eq of (Expr, Expr)
(* Does not typecheck *)
fun eval (x:Expr): int =
case+ x of
| I i => i
| B b => b
| Add (t1, t2) => eval(t1) + eval(t2)
| Mul (t1, t2) => eval(t1) * eval(t2)
| Eq (t1, t2) => eval(t1) = eval(t2)
This code fails to typecheck - the eval
function is defined to
return an int
but the B b
pattern match returns a boolean. We can
work around this by making the result value of eval
return a
datatype that can represent either an int
or a bool
but then we
have to add code throughout eval
to detect the invalid addition or
multiplication of a boolean and raise a runtime error. Ideally we'd
like to have make it impossible to construct invalid expressions such
that they error out at compile time.
We can imagine the type constructors for Expr
as if they were
functions with a type signature. The type signature of the
constructors would be:
fun I(n:int): Expr
fun B(b:bool): Expr
fun Add(t1:Expr, t2:Expr): Expr
fun Mul(t1:Expr, t1:Expr): Expr
fun Eq(t1:Expr, t2:Expr): Expr
The problem here is that Add
and Mul
both take Expr
as arguments
but we want to restrict them to integer expressions only - we need to
differentiate between integer and boolean expressions. We'd like to
add a type index to the Expr
datatype that indicates if it is a
boolean or an integer expression and change the constructors so they
have types like:
fun I(n:int): Expr int
fun B(b:bool): Expr bool
fun Add(t1:Expr int, t2:Expr int): Expr int
fun Mul(t1:Expr int, t1:Expr int): Expr int
fun Eq(t1:Expr int, t2:Expr int): Expr bool
Using these constructors would make it impossible to create an
expression that would give a runtime error in an eval
function. Creating an Expr
with a type index looks like:
datatype Expr(a:t@ype) =
| I(a) of int
| B(a) of bool
| Add(a) of (Expr int, Expr int)
| Mul(a) of (Expr int, Expr int)
| Eq(a) of (Expr int, Expr int)
This adds a type index of sort t@ype
. A 'sort' in ATS is the type of
type indexes. The t@ype
is for types that have a flat memory
structure of an unknown size. The '@' sigil looks odd inside the name,
but '@' is used elsewhere in ATS when defining flat records and tuples
which is a useful mnemonic for remembering what the '@' within the
sort name means.
This doesn't help our case though as the type signatures for the constructors would be:
fun I(n:int): Expr a
fun B(b:bool): Expr a
fun Add(t1:Expr int, t2:Expr int): Expr a
fun Mul(t1:Expr int, t1:Expr int): Expr a
fun Eq(t1:Expr int, t2:Expr int): Expr a
There is still the problem that an Expr a
is not an Expr int
for
Add
, Mul
and Eq
, and requiring runtime errors when pattern
matching. This is where GADTs come in. GADTs enable defining a
datatype that provides constructors where the generic a
of the type
index can be constrained to a specific type, different for each
constructor. The Expr
datatype becomes:
datatype Expr(t@ype) =
| I(int) of int
| B(bool) of bool
| Add(int) of (Expr int, Expr int)
| Mul(int) of (Expr int, Expr int)
| Eq(bool) of (Expr int, Expr int)
The constructor type signature now match those that we wanted earlier
and it becomes possible to check at compile time for invalid
expressions. The eval
functions looks similar, but is parameterized
over the type index:
fun{a:t@ype} eval(x:Expr a): a =
case+ x of
| I i => i
| B b => b
| Add (t1, t2) => eval(t1) + eval(t2)
| Mul (t1, t2) => eval(t1) * eval(t2)
| Eq (t1, t2) => eval(t1) = eval(t2)
The "{a:t@ype}
" syntax following fun
is ATS' way of defining a
function template where a
is the template argument. ATS will
generate a new function specific for each a
type used in the
program.
An example main
function to demonstrate the new GADT enabled Expr
and eval
:
implement main0() = let
val term1 = Eq(I(5), Add(I(1), I(4)))
val term2 = Mul(I(2), I(4))
val res1 = eval(term1)
val res2 = eval(term2)
in
println!("res1=", res1, " and res2=", res2)
end
$ patscc -DATS_MEMALLOC_LIBC -o arith2 arith2.dats
$ ./arith2
res1=true and res2=8
You may have noticed that our Expr
type can't represent equality
between booleans, or between booleans and integers. It's defined to
only allow equality between integers. It's possible to make equality
polymorphic but I'll go through this later as it brings up some more
complicated edge cases in types with ATS beyond just using GADTs.
This example of GADT usage in ATS tries to implement a sprintf
function that allows providing a format specification to sprintf
which then processes it and accepts arguments of types as defined by
the format specification.
The format specification is defined as a GADT:
datatype Format (a:type) =
| I(int -<cloref1> a) of (Format a)
| S_(a) of (string, Format a)
| S0(string) of string
Each constructor represents part of a format string. The type index is the type that sprintf
will return given a format string for that type. sprintf
is declared as:
fun sprintf {a:type} (fmt: Format a): a
Here are some example invocations and the types that should result:
// Returns a string
sprintf (S0 "hello")
// Returns a string
sprintf (S_ ("hello", S0 "world"))
// Returns a function that takes an int and returns a string
sprintf (I (S0 "<- is a number"))
The last example shows how sprintf
emulates variable arguments using closures. By returning a function any immediately following tokens are treated as arguments to that function. For example:
sprintf (I (S0 "<- is a number")) 42
(int -> string) 42
With some syntactic sugar using currying we can make this look nicer. Curried functions is a feature that isn't often used in ATS as it requires the garbage collector (to clean up partially curried functions) and performance is diminished due to the allocation of closures but it's useful for this example.
With the Format
datatype defined, here's the implementation of sprintf
:
fun sprintf {a:type} (fmt: Format a): a = let
fun aux {a:type}(pre: string, fmt': Format a): a =
case fmt' of
| I fmt => (lam (i) => aux(append(pre, int2string(i)), fmt))
| S_ (s, fmt) => aux(append(pre, s), fmt)
| S0 s => append(pre, s)
in
aux("", fmt)
end
It uses an inner function, aux
, that does the work of deconstructing the format argument and returning a closure when needed, and appending strings as the result string is computed. For this example I'm cheating with memory management to keep the focus on GADT, and off dealing with the intricacies of linear strings. The example should be run with the garbage collector to free the allocated strings.
Here's an example of executing what we have so far:
implement main0() = let
val fmt = S_ ("X: ", (I (S_ (" Y: ", (I (S0 ""))))))
val s = sprintf fmt 5 10
in
println!(s)
end
$ ./format
X: 5 Y: 10
The format string is pretty ugly though. Some helper functions make it a bit more friendly:
fun Str {a:type} (s: string) (fmt: Format a) = S_ (s, fmt)
fun Int {a:type} (fmt: Format a) = I (fmt)
fun End (s:string) = S0 (s)
infixr 0 >:
macdef >: (f, x) = ,(f) ,(x)
Now the format definition is:
val fmt = Str "X: " >: Int >: Str " Y: " >: Int >: End ""
The string handling functions that I threw together to append strings and convert an integer to a string without dealing with linear strings follow.
fun append(s0: string, s1: string): string = let
extern castfn from(s:string):<> Strptr1
extern castfn to(s:Strptr0):<> string
extern prfun drop(s:Strptr1):<> void
val s0' = from(s0)
val s1' = from(s1)
val r = strptr_append(s0', s1')
prval () = drop(s0')
prval () = drop(s1')
in
to(r)
end
fun int2string(x: int): string =
tostring(g0int2string x) where {
extern castfn tostring(Strptr0):<> string
}
These example of GADT usage were pulled from the papers and articles mentioned at the beginning of the post. They were written for Haskell or Dependent ML (a predecessor to ATS). There may be better ways of approaching the problem in ATS and some constraints on the way ATS generates C code limits how GADTs can be used. One example of the limitation was mentioned in the first example of the expression evaluator.
If the Expr
datatype is changed so that Eq
can work on any type, not just int
, then a compile error results:
datatype Expr(a:t@ype) =
| I(a) of int
| B(a) of bool
| Add(a) of (Expr int, Expr int)
| Mul(a) of (Expr int, Expr int)
| Eq(a) of (Expr a, Expr a)
The error occurs due to the Eq
branch in the case statement in eval
:
fun{a:t@ype} eval(x:Expr a): a =
case+ x of
| I i => i
| B b => b
| Add (t1, t2) => eval(t1) + eval(t2)
| Mul (t1, t2) => eval(t1) * eval(t2)
| Eq (t1, t2) => eval(t1) = eval(t2)
The compiler is unable to find a match for the overloaded =
call for the general case of any a
(vs the specific case of int
as it was before). This is something I've written about before and the workaround in that post gets us past that error:
extern fun{a:t@ype} equals(t1:a, t2:a): bool
implement equals<int>(t1,t2) = g0int_eq(t1,t2)
implement equals<bool>(t1,t2) = eq_bool0_bool0(t1,t2)
fun{a:t@ype} eval(x:Expr a): a =
case+ x of
| I i => i
| B b => b
| Add (t1, t2) => eval(t1) + eval(t2)
| Mul (t1, t2) => eval(t1) * eval(t2)
| Eq (t1, t2) => equals(eval(t1), eval (t2))
Now the program typechecks but fails to compile the generated C code. This can usually be resolved by explicitly stating the template parameters in template function calls:
fun{a:t@ype} eval(x:Expr a): a =
case+ x of
| I i => i
| B b => b
| Add (t1, t2) => eval<int>(t1) + eval<int>(t2)
| Mul (t1, t2) => eval<int>(t1) * eval<int>(t2)
| Eq (t1, t2) => equals<?>(eval<?>(t1), eval<?>(t2))
The problem here is what types to put in the '?
' in this snippet? The Expr
type defines this as being any a
but we want to constrain it to the index used by t1
and t2
but I don't think ATS allows us to declare that. This mailing list thread discusses the issue with some workarounds.
SWI Prolog is an open source Prolog implementation with good documentation and many interesting libraries. One library that was published recently is Web Prolog. While branded as a 'Web Logic Programming Language' the implementation in the github repository runs under SWI Prolog and adds Erlang style distributed concurrency. There is a PDF Book in the repository that goes into detail about the system. In this post I explore some of features.
The first step is to install and run the SWI Prolog development version. There is documentation on this but the following are the basic steps to download and build from the SWI Prolog github repository:
$ git clone https://github.com/SWI-Prolog/swipl-devel
$ cd swipl-devel
$ ./prepare
... answer yes to the various prompts ...
$ cp build.tmpl build
$ vim build
...change PREFIX to where you want to install...
$ make install
$ export PATH=<install location>/bin:$PATH
There may be errors about building optional libraries. They can be ignored or view dependancies to see how to install.
The newly installed SWI Prolog build can be run with:
$ swipl
Welcome to SWI-Prolog (threaded, 64 bits, version 7.7.19-47-g4c3d70a09)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.
Please run ?- license. for legal details.
For online help and background, visit http://www.swi-prolog.org
For built-in help, use ?- help(Topic). or ?- apropos(Word).
?-
I recommend reading Basic Concepts in The Power of Prolog to get a grasp of Prolog syntax if you're not familiar with it.
Installing the Web Prolog libraries involves cloning the github repository and loading the prolog libraries held within. The system includes a web based tutorial and IDE where each connected web page is a web prolog node that can send and receive messages to other web prolog nodes. I'll beiefly mention this later but won't cover it in detail in this post - for now some simple examples will just use the SWI Prolog REPL. We'll need two nodes running, which can be done by running on different machines. On each machine run:
$ git clone https://github.com/Web-Prolog/swi-web-prolog/
$ cd swi-web-prolog
$ swipl
...
?- [web_prolog].
...
The [web_prolog].
command at the prolog prompt loads the web prolog libraries. Once loaded we need to instantiate a node, which starts the socket server and machinery that handles messaging:
?- node.
% Started server at http://localhost:3060/
true.
This starts a node on the default port 3060
. If you're running multiple nodes on the same machine you can change the port by passing an argument to node
:
?- node(localhost:3061).
% Started server at http://localhost:3061/
true.
In the rest of this post I refer to node A
and node B
for the two nodes started above.
Each process has an id that can be used to reference it. It is obtained via self
:
?- self(Self).
Self = thread(1)@'http://localhost:3061'.
We can send a message using '!
'. Like Erlang, it takes a process to send to and the data to send:
?- self(Self),
Self ! 'Hello World'.
This posts 'Hello World' to the current process mailbox. Messages can be received using receive
. This takes a series of patterns to match against and code to run if an item in the process mailbox matches that pattern. Like Erlang it is a selective receive - it will look through messages in the mailbox that match the pattern, not just the topmost message:
?- receive({ M -> writeln(M) }).
Hello World
M = 'Hello World'.
Notice the receive
rules are enclosed in '{ ... }
' and are comprised of a pattern to match against and the code to run separated by ->
. Variables in the pattern are assigned the value of what they match. In this case M
is set to Hello World
as that's the message we sent earlier. More complex patterns are possible:
?- $Self ! foo(1, 2, bar('hi', [ 'a', 'b', 'c' ])).
Self = thread(1)@'http://localhost:3061'.
?- receive({ foo(A, B, bar(C, [D | E])) -> true }).
A = 1,
B = 2,
C = hi,
D = a,
E = [b, c].
Here I make use of a feature of the SWI Prolog REPL - prefixing a variable with $
will use the value that was assigned to that variable in a previous REPL command. This also shows matching on the head and tail of a list with the [Head | Tail]
syntax.
To send to another process we just need to use the process identifier. In this case I can send a message from node A to node B:
# In Node A
?- self(Self).
Self = thread(1)@'http://localhost:3060'.
# This call blocks
?- receive({ M -> format('I got: ~s~n', [M])}).
# In Node B
?- thread(1)@'http://localhost:3060' ! 'Hi World'.
true.
# Node A unblocks
I got: Hi World
M = 'Hi World'.
Use spawn
to spawn a new process the runs concurrencly on a node. It will have its own process Id:
?- spawn((self(Self),
format('My process id is ~w~n', [Self]))).
true.
My process id is 21421552@http://localhost:3060
The code to run in the process is passed as the first argument to spawn
and must be between brackets. An optional second argument will provide the process id to the caller:
?- spawn((self(Self),
format('My process id is ~w~n', [Self])),
Pid).
My process id is 33869438@http://localhost:3060
Pid = '33869438'.
A third argument can be provided to pass options to control spawning. These include the ability to link processes, monitor them or register a name to identify it in a registry.
Using the REPL we can define new rules and run them in processes, either by consulting a file, or entering them via [user]
. The following code will define the code for a 'ping' server process:
server :-
receive({
ping(Pid) -> Pid ! pong, server
}).
This can be added to a file and loaded in the REPL with consult
, or it can be entered directly using [user]
(note the use of Ctrl+D to exit the user input):
# on Node A
?- [user].
|: server :-
|: receive({
|: ping(Pid) -> Pid ! pong, server
|: }).
|: ^D
% user://1 compiled 0.01 sec, 1 clauses
true.
server
blocks receiving messages looking for a ping(Pid)
message. It sends a pong
message back to the process id it extracted from the message and calls itself recursively using a tail call. Run on the node with:
# on node A
?- spawn((server), Pid).
Pid = '18268992'.
Send a message from another node by referencing the Pid along with the nodes address:
# on node B
?- self(Self), 18268992@'http://localhost:3060' ! ping(Self).
Self = thread(1)@'http://localhost:30601.
?- flush.
% Got pong
true.
The flush
call will remove all messages from the process' queue and display them. In this case, the pong
reply from the other nodes server.
Web Prolog provides the ability to spawn processes to run on remote nodes. This is done by passing a node
option to spawn
. To demonstrate, enter the following to create an add
rule in node A:
# on node A
?- [user].
|: add(X,Y,Z) :- Z is X + Y.
|: ^D
% user://1 compiled 0.01 sec, 1 clauses
true.
This creates an 'add' predicate that works as follows:
# on node A
?- add(1,2,Z).
Z = 3.
We can call this predicate from node B by spawning a remote process that executes code in node A. In node B, it looks like this:
# on node B
?- self(Self),
spawn((
call(add(10, 20, Z)),
Self ! Z
), Pid, [
node('http://localhost:3060'),
monitor(true)
]),
receive({ M -> format('Result is ~w~n', [M])})
Result is 30
Self = thread(1)@'http://localhost:3061',
Pid = '24931627'@'http://localhost:3060',
M = 30.
Passing node
as an option to spawn/3
results in a process being spawned on that referenced node and the code runs there. In the code we call the add
predicate that only exists on node A and return it by sending it to node B's identifier. The monitor
option provides status information about the remote process - including getting a message when the process exits. Calling flush
on node B shows that the process on node A exits:
# on Node B
?- flush.
% Got down('24931627'@'http://localhost:3060',exit)
true.
Note the indirection in the spawn
call where add
isn't called directly, instead call
is used to call it. For some reason Web Prolog requires add
to exist on node B even though it is not called. The following gives an error on node B for example:
# on node B
?- self(Self),
spawn((
add(10, 20, Z),
Self ! Z
), Pid, [
node('http://localhost:3060'),
monitor(true)
]),
receive({ M -> format('Result is ~w~n', [M])})
ERROR: Undefined procedure: add/3 (DWIM could not correct goal)
I'm unsure if this is an error in web prolog or something I'm doing.
The previous example can be simplified using RPC functions provided by web prolog. A synchronous RPC call from node B can be done that is aproximately equivalent to the above:
?- rpc('http://localhost:3060', add(1,2,Z)).
Z = 3.
Or ansynchronously using promises:
?- promise('http://localhost:3060', add(1,2,Z), Ref).
Ref = '119435902516515459454946972679206500389'.
?- yield($Ref, Answer).
Answer = success(anonymous, [add(1, 2, 3)], false),
Ref = '119435902516515459454946972679206500389'.
The following example, based on one I did for Wasp Lisp, is a process that maintains a count that can be incremented, decremented or retrieved:
server(Count) :-
receive({
inc -> Count2 is Count + 1, server(Count2);
dec -> Count2 is Count - 1, server(Count2);
get(Pid) -> Pid ! value(Count), server(Count)
}).
Once defined, it can be spawned in node A with:
?- spawn((server(0)), Pid).
Pid = '33403644'.
And called from Node B with code like:
?- self(Self), 33403644@'http://localhost:3060' ! get(Self).
Self = thread(1)@'http://localhost:3061'.
?- flush.
% Got value(0)
true.
?- 33403644@'http://localhost:3060' ! inc.
true.
?- self(Self), 33403644@'http://localhost:3060' ! get(Self).
Self = thread(1)@'http://localhost:3061'.
?- flush.
% Got value(1)
true.
We can modify the server so it accepts an upgrade
message that contains the new code that the server will execute:
server(Count) :-
writeln("server receive"),
receive({
inc -> Count2 is Count + 1, server(Count2);
dec -> Count2 is Count - 1, server(Count2);
get(Pid) -> Pid ! value(Count), server(Count);
upgrade(Pred) -> writeln('upgrading...'), call(Pred, Count)
}).
Run the server and send it some messages. Then define a new_server
on node A's REPL:
new_server(Count) :-
writeln("new_server receive"),
receive({
inc -> Count2 is Count + 1, new_server(Count2);
dec -> Count2 is Count - 1, new_server(Count2);
mul(X) -> Count2 is Count * X, new_server(Count2);
get(Pid) -> Pid ! value(Count), new_server(Count);
upgrade(Pred) -> writeln(Pred), writeln(Count), call(Pred, Count)
}).
And send an upgrade
message to the existing server:
# on node A
?- $Pid ! upgrade(new_server).
upgrading...
new_server receive
Now the server understands the mul
message without having to be shut down and restarted.
There's a web based IDE and tutorial based on SWISH, the online SWI-Prolog system. To start this on a local node, run the following script from the web prolog source:
$ cd web-client
$ swipl run.pl
Now visit http://localhost:3060/apps/swish/index.html
in a web browser. This displays a tutorial on the left and a REPL on the right. Each loaded web page has its own namespace and local environment. You can send messages to and from individual web pages and the processes running in the local node. It uses websockets to send data to and from instances.
There's a lot to the Web Prolog system and the implementation for SWI Prolog has some rough edges but it's usable to experiment with and get a feel for the system. I hope to write a more about some of the features of it, and SWI Prolog, as I get more familiar with it.
I'm very pleased to announce the release of Factor 0.98!
OS/CPU Windows Mac OS X Linux x86 x86-64 Source code: 0.98
This release is brought to you with almost 4,300 commits by the following individuals:
Alexander Ilin, Arkady Rost, Benjamin Pollack, Björn Lindqvist, Cat Stevens, Chris Double, Dimage Sapelkin, Doug Coleman, Friedrich von Never, John Benediktsson, Jon Harper, Mark Green, Mark Sweeney, Nicolas Pénet, Philip Dexter, Robert Vollmert, Samuel Tardieu, Sankaranarayanan Viswanathan, Shane Pelletier, @catb0t, @hyphz, @thron7, @xzenf
Besides several years of bug fixes and library improvements, I want to highlight the following changes:
Some possible backwards compatibility issues:
unicode
namespace (either USE: ascii
or USE: unicode
).CONSTRUCTOR:
syntax to include generated word namecd
to change directory when launching processes; there is another mechanism for thatlibc
, renamed (io-error)
to throw-errno
match
, renamed ?1-tail
to ?rest
sequences
, renamed iota
to <iota>
sequences
, renamed start
/start*
to subseq-start
/subseq-start-from
syntax
, renamed GENERIC#
to GENERIC#:
buffered-port
not have a length, because of problem with Linux virtual files and TCP socketscase
statementsFactor is a concatenative, stack-based programming language with high-level features including dynamic types, extensible syntax, macros, and garbage collection. On a practical side, Factor has a full-featured library, supports many different platforms, and has been extensively documented.
The implementation is fully compiled for performance, while still supporting interactive development. Factor applications are portable between all common platforms. Factor can deploy stand-alone applications on all platforms. Full source code for the Factor project is available under a BSD license.
"I :heart: Factor :+1:"
)/etc/hosts
file parser/etc/ld.so.cache
filelibtls
functions.SRT
filescomdlg32.dll
functionscrypt32.dll
functionsswap-when
file-readable?
to check current user's permissionsM\ c-reader stream-read-until
binpack
and map-binpack
logn
format-float
for known format stringsv>integer
monotonic-split
.sort-keys
and sort-values
on hashtables
map-sort
\u{snowman}
and \u{2603}
with-test-file
and with-test-directory
helper wordsz-values
Minesweeper is a fun game that was probably made most popular by its inclusion in various Microsoft Windows versions since the early 1990's.
I thought it would be fun to build a simple Minesweeper clone using Factor.
You can run this by updating to the latest code and running:
IN: scratchpad "minesweeper" run
We are going to represent our game grid as a two-dimensional array of "cells".
Each cell contains the number of mines contained in the (up to eight) adjacent cells, whether the cell contains a mine, and a "state" flag showing whether the cell was +clicked+
, +flagged+
, or marked with a +question+
mark.
SYMBOLS: +clicked+ +flagged+ +question+ ;
TUPLE: cell #adjacent mined? state ;
Making a (rows, cols)
grid of cells:
: make-cells ( rows cols -- cells )
'[ _ [ cell new ] replicate ] replicate ;
We can lookup a particular cell using its (row, col)
index:
:: cell-at ( cells row col -- cell/f )
row cells ?nth [ col swap ?nth ] [ f ] if* ;
Placing a number of mines into cells, just looks for a certain number of unmined cells at random, and then marks them as mined:
: unmined-cell ( cells -- cell )
f [ dup mined?>> ] [ drop dup random random ] do while nip ;
: place-mines ( cells n -- cells )
[ dup unmined-cell t >>mined? drop ] times ;
We can count the number of adjacent mines for each cell, by looking at its neighbors:
CONSTANT: neighbors {
{ -1 -1 } { -1 0 } { -1 1 }
{ 0 -1 } { 0 1 }
{ 1 -1 } { 1 0 } { 1 1 }
}
: adjacent-mines ( cells row col -- #mines )
neighbors [
first2 [ + ] bi-curry@ bi* cell-at
[ mined?>> ] [ f ] if*
] with with with count ;
The each-cell
word looks at all the cells, helping us update the "adjacent mines" counts:
:: each-cell ( ... cells quot: ( ... row col cell -- ... ) -- ... )
cells [| row |
[| cell col | row col cell quot call ] each-index
] each-index ; inline
:: update-counts ( cells -- cells )
cells [| row col cell |
cells row col adjacent-mines cell #adjacent<<
] each-cell cells ;
Since we aren't storing the number of rows and columns, we can get it from the array of cells:
: cells-dim ( cells -- rows cols )
[ length ] [ first length ] bi ;
We can get the number of mines contained in the grid by counting them up:
: #mines ( cells -- n )
[ [ mined?>> ] count ] map-sum ;
We can reset the game by making new cells and then placing the same number of mines in them:
: reset-cells ( cells -- cells )
[ cells-dim make-cells ] [ #mines place-mines ] bi update-counts ;
The player wins if they click on all cells that aren't mines:
: won? ( cells -- ? )
[ [ { [ state>> +clicked+ = ] [ mined?>> ] } 1|| ] all? ] all? ;
The player loses if they click on any cell that's a mine:
: lost? ( cells -- ? )
[ [ { [ state>> +clicked+ = ] [ mined?>> ] } 1&& ] any? ] any? ;
And then the game is over if the player either wins or loses:
: game-over? ( cells -- ? )
{ [ lost? ] [ won? ] } 1|| ;
We can tell this is a new game if no cells are clicked on:
: new-game? ( cells -- ? )
[ [ state>> +clicked+ = ] any? ] any? not ;
When we click on a cell, if it is not adjacent to any mines, we click on all the "clickable" (non-mined) cells around it:
DEFER: click-cell-at
:: click-cells-around ( cells row col -- )
neighbors [
first2 [ row + ] [ col + ] bi* :> ( row' col' )
cells row' col' cell-at [
mined?>> [
cells row' col' click-cell-at
] unless
] when*
] each ;
Handle clicking a cell. If it's the first click and the cell is mined, we move it to another random cell, then continue with the click. The click is ignored if the cell was already clicked or flagged. Continue clicking around any cells that have no adjacent mines and are not themselves mined.
:: click-cell-at ( cells row col -- )
cells row col cell-at [
cells new-game? [
! first click shouldn't be a mine
dup mined?>> [
cells unmined-cell t >>mined? drop f >>mined?
cells update-counts drop
] when
] when
dup state>> { +clicked+ +flagged+ } member? [ drop ] [
+clicked+ >>state
{ [ mined?>> not ] [ #adjacent>> 0 = ] } 1&& [
cells row col click-cells-around
] when
] if
] when* ;
Handle marking a cell. First by flagging it as a likely mine, or marking with a question mark to come back to later. If the cell is not clicked, we just cycle through flagging, question, or not clicked.
:: mark-cell-at ( cells row col -- )
cells row col cell-at [
dup state>> {
{ +clicked+ [ +clicked+ ] }
{ +flagged+ [ +question+ ] }
{ +question+ [ f ] }
{ f [ +flagged+ ] }
} case >>state drop
] when* ;
Our graphical interface is going to consist of a gadget with an array of cells and a cache of OpenGL texture objects that can be easily drawn on the screen.
TUPLE: grid-gadget < gadget cells textures ;
When you make a new grid-gadget
, it initializes the game to a specified number of rows, columns, and number of mines:
:: <grid-gadget> ( rows cols mines -- gadget )
grid-gadget new
rows cols make-cells
mines place-mines update-counts >>cells
H{ } clone >>textures
COLOR: gray <solid> >>interior ;
When ungraft* is called to indicate the gadget is no longer visible on the screen, we clean up the cached textures:
M: grid-gadget ungraft*
dup find-gl-context
[ values dispose-each H{ } clone ] change-textures
call-next-method ;
Our images are going to be 32 x 32
squares, so the preferred dimension is number of rows and columns times 32 pixels for each square.
M: grid-gadget pref-dim*
cells>> cells-dim [ 32 * ] bi@ swap 2array ;
Some slightly complex logic to decide which image to display for each cell, taking into account whether the game is over so we can show the positions of all the mines and whether the player was correct in flagging a cell as mined, etc:
:: cell-image-path ( cell game-over? -- image-path )
game-over? cell mined?>> and [
cell state>> +clicked+ = "mineclicked.gif" "mine.gif" ?
] [
cell state>>
{
{ +question+ [ "question.gif" ] }
{ +flagged+ [ game-over? "misflagged.gif" "flagged.gif" ? ] }
{ +clicked+ [
cell mined?>> [
"mine.gif"
] [
cell #adjacent>> 0 or number>string
"open" ".gif" surround
] if ] }
{ f [ "blank.gif" ] }
} case
] if "vocab:minesweeper/_resources/" prepend ;
Drawing a cached texture is a matter of looking up the image in our texture cache and then rendering to the screen:
: draw-cached-texture ( path gadget -- )
textures>> [ load-image { 0 0 } <texture> ] cache
[ dim>> ] [ draw-scaled-texture ] bi ;
Drawing our gadget, is basically drawing all of the cells at their proper locations on the screen:
M:: grid-gadget draw-gadget* ( gadget -- )
gadget cells>> game-over? :> game-over?
gadget cells>> [| row col cell |
col row [ 32 * ] bi@ 2array [
cell game-over? cell-image-path
gadget draw-cached-texture
] with-translation
] each-cell ;
Basic handling for the gadget being left-clicked on:
:: on-click ( gadget -- )
gadget hand-rel first2 :> ( w h )
h w [ 32 /i ] bi@ :> ( row col )
gadget cells>> :> cells
cells game-over? [
cells row col click-cell-at
] unless gadget relayout-1 ;
Basic handling for the gadget being right-clicked on:
:: on-mark ( gadget -- )
gadget hand-rel first2 :> ( w h )
h w [ 32 /i ] bi@ :> ( row col )
gadget cells>> :> cells
cells game-over? [
cells row col mark-cell-at
] unless gadget relayout-1 ;
Logic for creating new games of varying difficulties: easy, medium, and hard:
: new-game ( gadget rows cols mines -- )
[ make-cells ] dip place-mines update-counts >>cells
relayout-window ;
: com-easy ( gadget -- ) 7 7 10 new-game ;
: com-medium ( gadget -- ) 15 15 40 new-game ;
: com-hard ( gadget -- ) 15 30 99 new-game ;
We set our gesture handlers for keyboard and mouse inputs:
grid-gadget {
{ T{ key-down { sym "1" } } [ com-easy ] }
{ T{ key-down { sym "2" } } [ com-medium ] }
{ T{ key-down { sym "3" } } [ com-hard ] }
{ T{ button-up { # 1 } } [ on-click ] }
{ T{ button-up { # 3 } } [ on-mark ] }
{ T{ key-down { sym " " } } [ on-mark ] }
} set-gestures
And a main word that creates an easy game in our grid-gadget
and opens it in a new window:
MAIN-WINDOW: run-minesweeper {
{ title "Minesweeper" }
{ window-controls
{ normal-title-bar close-button minimize-button } }
} 7 7 10 <grid-gadget> >>gadgets ;
The implementation above is about 200 lines of code and contains the full game logic. The final version is just under 300 lines of code, and adds:
2x
imagesI've been reading the book Building High Integrity Applications with Spark to learn more about the SPARK/Ada language for formal verification. It's a great book that goes through lots of examples of how to do proofs in Spark. I wrote a post on Spark/Ada earlier this year and tried some of the examples in the GNAT edition.
While working through the book I oftened compared how I'd implement similar examples in ATS. I'll go through one small example in this post and show how the dependent types of ATS allow capturing the invariants of a function and check them at type checking time to prove the absence of a particular class of runtime errors.
The example I'm looking at from the book is from the Loop Invariants
section, which aims to prove things about iterative loops in Ada. The procedure Copy_Into
copies characters from a String
into a Buffer
object that has a maximum capacity. If the source string is too short then the buffer is padded with spaces. The Spark/Ada code from the book is:
procedure Copy_Into(Buffer: out Buffer_Type; Source: in String) is
Characters_To_Copy : Buffer_Count_type := Maximum_Buffer_Size;
begin
Buffer := (others => ' ');
if Source'Length < Characters_To_Copy then
Characters_To_Copy := Source`Length;
end if;
for Index in Buffer_Count_Type range 1 .. Characters_To_Copy loop
pragma Loop_Invariant (Characters_To_Copy <= Source'Length and
Characters_To_Copy = Characters_To_Copy'Loop_Entry);
Buffer(Index) := Source(Source'First + (Index - 1));
end loop;
end Copy_Into;
This is quite readable for anyone familiar with imperative languages. The number of characters to copy is initially set to the maximum buffer size, then changed to the length of the string if it is less than that. The buffer is set to contain the initial characters ' '. The buffer is 1-indexed and during the loop the characters from the string are copied to it.
The Loop_Invariant
pragma is a Spark statement that tells the checker that certain invariants should be true. The invariant used here is that the number of characters to copy is always less than or equal to the length of the string and does not change within the loop. Given this loop invariant Spark can assert that the indexing into the Source
string cannot exceed the bounds of the string. Spark is able to reason itself that Buffer
does not get indexed out of bounds as the loop ranges up to Characters_To_Copy
which is capped at Maximum_Buffer_Size
. I'm not sure why this doesn't need a loop invariant but the book notes that the Spark tools improve over time at what invariants they can compute automatically. As an example, the second invariant check above for Characters_To_Copy'Loop_Entry
isn't needed for newer versions of Spark but is kept to enable checking on older toolchains.
For ATS I modeled the Buffer
type as an array of characters:
stadef s_max_buffer_size: int = 128
typedef Buffer0 = @[char?][s_max_buffer_size]
typedef Buffer1 = @[char][s_max_buffer_size]
val max_buffer_size: size_t s_max_buffer_size = i2sz(128)
In ATS, @[char][128]
represents an array of contiguous 'char' types in memory, where those char's are initialized to value. The @[char?][128]
represents an array of unitialized char's. It would be a type error to use an element of that array before initializing it. The '0' and '1' suffixes to the 'Buffer' name is an ATS idiom for uninitialized and initialized data respectively.
The stadef
keyword creates a constant in the 'statics' system of ATS. That is a constant in the language of types, vs a constant in the language of values where runtime level programming is done. For this post I have prefixed variables in the 'statics' system with s_
to make it clearer where they can be used.
The max_buffer_size
creates a constant in the 'dynamics' part of ATS, in the language of values, of type "size_t max_buffer_size
". size_t
is the type for indexes into arrays and size_t 128
is a dependent type representing a type where only a single value matches the type - 128
in this instance. The i2sz
function converts an integer to a size_t
. So in this case we've created a max_buffer_size
constant that can only ever be the same value as the s_max_buffer_size
type level constant.
The ATS equivalent of copy_into
looks like:
fun copy_into {n:nat}
(buffer: &Buffer0 >> Buffer1, source: string n): void = let
val () = array_initize_elt(buffer, max_buffer_size, ' ')
val len = string1_length(source)
stadef s_tocopy = min(s_max_buffer_size, n)
val tocopy: size_t s_tocopy = min(max_buffer_size, len)
fun loop {m:nat | m < s_tocopy } .<s_tocopy - m>.
(buffer: &Buffer1, m: size_t m): void = let
val () = buffer[m] := source[m]
in
if m < tocopy - 1 then loop(buffer, m+1)
end
in
if len > 0 then
loop(buffer, i2sz(0))
end
Starting with the function declaration:
fun copy_into {n:nat}
(buffer: &Buffer0 >> Buffer1, source: string n): void
The items between the curly brackets, {...}
, are universal variables used for setting constraints on the function arguments. Between the round brackets, (...)
, are the function arguments. The return type is void
. The function takes two arguments, buffer
and source
.
The buffer
is a reference type, represented by the &
in the type. This is similar to a reference argument in C++ or a pointer argument in C. It allows modification of the argument by the function. The Buffer0 >> Buffer1
means on entry to the function the type is Buffer0
, the uninitialized char
array described earlier, and on exit it will be a Buffer1
, an initialized char array. if the body of the function fails to initialize the elements of the array it will be a type error.
The source
argument is a string n
, where n
is a type index for the length of the string. By using a dependently typed string here we can use it later in the function body to set some invariants.
In the body of the function the call to array_initize_elt
sets each element of the array to the space character. This also has the effect of changing the type stored in the array from char?
to char
, and the array is now a valid Buffer1
. This matches the type change specified in the function declaration for the buffer
argument.
The next three lines compute the number of characters to copy:
val len = string1_length(source)
stadef s_tocopy = min(s_max_buffer_size, n)
val tocopy: size_t s_tocopy = min(max_buffer_size, len)
The length of the string is obtained. The string1_
prefix to function names is an idiom to show that they operate on dependently typed strings. string1_length
will return the string length. It returns a dependently typed size_t x
, where x
is the length of the string. This means that calling string_length
not only returns the length of the string but it sets a constraint such that the type index of the result is equal to the type index of the string passed in. Here is the declaration of string1_length
from the prelude (with some additional annotations removed):
fun string1_length {n:int} (x: string n): size_t n
The reuse of the n
in the argument and result type is what tells the compiler to set the constraint when it is called. This is important for the next two lines. These perform the same operation, once in the statics and once in the dynamics. That is, once at the type level and once at the runtime level. The stadef
sets a type level constant called s_tocopy
to be constrained to be the same as the minimum of the max buffer size and the type level string length, n
. The val
line sets the runtime variable to the same calculation but using the runtime length. These two lengths must much as a result of the call to string1_length
described earlier. The type of tocopy
ensures this by saying that it is the singleton type that can only be fulfilled by the value represented by s_tocopy
.
ATS has looping constructs but it's idiomatic to use tail recursion instead of loops. It is also easier to create types for tail recursive functions than to type iterative loops in ATS. For this reason I've converted the loop to a tail recursive function. When ATS compiles to C it converts tail recursive functions to a C loop so there is no danger of stack overflow. The looping function without dependent type annotations would be:
fun loop (buffer: &Buffer1, m: size_t): void = let
val () = buffer[m] := source[m]
in
if m < tocopy - 1 then loop(buffer, m+1)
end
It takes a buffer
and an index, m
, as arguments and assigns to buffer
at that index the equivalent entry from the source
string. If it hasn't yet copied the number of characters needed to copy it tail recursively calls itself, increasing the index. The initial call is:
loop(buffer, i2sz(0))
i2sz
is needed to convert the integer number zero from an int
type to a size_t
type.
The declaration for the loop
function contains the dependent type definitions that give invariants similar to the Spark example:
fun loop {m:nat | m < s_tocopy } .<s_tocopy - m>.
(buffer: &Buffer1, m: size_t m): void = let
Starting with the arguments, the buffer
is a Buffer
meaning it must be an initialized array. The index, m
is a dependently typed size_t m
where m
at the type level is constrained to be less than the number of characters to copy. This ensures that the indexing into the buffer and source string is never out of bounds due to the previous statements that set s_tocopy
to be the lesser of the maximum buffer size and the string size. s_tocopy
is needed here instead of tocopy
due to universal arguments being written in the language of the typesystem, not the runtime system.
The body of the loop does the copying of the indexed character from the source string to the buffer and recursively calls itself with an incremented index if it hasn't copied the required number of characters.
val () = buffer[m] := source[m]
in
if m < tocopy - 1 then loop(buffer, m+1)
Due to the constraints set in the function declaration the buffer and source string indexes are checked at compile time to ensure they aren't out of bounds, and the recursive call to loop will fail typechecking if an out of bounds index is passed as an argument.
One issue with recursive functions is that they could loop forever if the termination condition check is incorrect, or the variables being used in that check don't explicitly increase or decrease. In this case the index must increase to eventually reach the value for the termination check.
ATS resolves this by allowing termination metrics to be added to the function. This is the part of the function declaration that is bracketed by .< ... >.
markers. The expression inside these markers is expected to be in the 'statics' constraint language and evaluate to a tuple of natural numbers that the compiler needs to prove are lexicographically decreasing in value. The loop
index counts up so this needs to be converted to a decreasing value:
.<s_tocopy - m>.
This is done by taking the static constant of the number of characters to copy and subtracting the index value. The compiler proves that each recursive call in the body of the function results in something strictly less than the previous call. With the termination metric added it statically proves that the recursive function terminates.
The program can be run and tested with:
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"
stadef s_max_buffer_size: int = 128
typedef Buffer0 = @[char?][s_max_buffer_size]
typedef Buffer1 = @[char][s_max_buffer_size]
val max_buffer_size: size_t s_max_buffer_size = i2sz(128)
fun copy_into {n:nat}
(buffer: &Buffer0 >> Buffer1, source: string n): void = let
val () = array_initize_elt(buffer, max_buffer_size, ' ')
val len = string1_length(source)
stadef s_tocopy = min(s_max_buffer_size, n)
val tocopy: size_t s_tocopy = min(max_buffer_size, len)
fun loop {m:nat | m < s_tocopy } .<s_tocopy - m>.
(buffer: &Buffer1, m: size_t m): void = let
val () = buffer[m] := source[m]
in
if m < tocopy - 1 then loop(buffer, m+1)
end
in
if len > 0 then
loop(buffer, i2sz(0))
end
implement main0() = let
var b = @[char?][max_buffer_size]()
val () = copy_into(b, "hello world")
fun print_buffer {n:nat | n < s_max_buffer_size}
.<s_max_buffer_size - n>.
(buffer: &Buffer1, n: size_t n):void = let
val () = if n = 0 then print!("[")
val () = print!(buffer[n])
val () = if n = max_buffer_size - 1 then print!("]")
in
if n < 127 then print_buffer(buffer, n + 1)
end
val () = print_buffer(b, i2sz(0))
in
()
end
This example creates the array as a stack allocated object in the line:
var b = @[char?][max_buffer_size]()
Being stack allocated the memory will be deallocated on exit of the scope it was defined in. It's also possible to create a heap allocated buffer and pass that to copy_into
:
implement main0() = let
val (pf_b , pf_gc| b) = array_ptr_alloc<char>(max_buffer_size)
val () = copy_into(!b, "hello world")
fun print_buffer {n:nat | n < 128} .<128 - n>. (buffer: &(@[char][128]), n: int n):void = let
val () = if n = 0 then print!("[")
val () = print!(buffer[n])
val () = if n = 127 then print!("]")
in
if n < 127 then print_buffer(buffer, n + 1)
end
val () = print_buffer(!b, 0)
val () = array_ptr_free(pf_b, pf_gc | b)
in
()
end
This explicitly allocates the memory for the array using array_ptr_alloc
and dereferences it in the copy_into
call using the '!b
' syntax. Note that this array is later free'd using array_ptr_free
. Not calling that to free the memory would be a compile error.
Although this is a simple function it demonstrates a number of safety features:
The book Building High Integrity Applications with Spark is a great book for learning Spark and also for learning about the sorts of proofs used in production applications using Spark/Ada. Apart from learning a bit about Spark it's also a good exercise to think about how similar safety checks can be implemented in your language of choice.
planet-factor is an Atom/RSS aggregator that collects the contents of Factor-related blogs. It is inspired by Planet Lisp.