Newbee question: static functions

Google Group
1

I am just getting started with ATS. I have some familiarity with Coq and
Agda.

Suppose I have the following static ATS definition:

datasort intlist =
| intlist_nil of ()
| intlist_cons of (int, intlist)

How do I add a static “function” that produces a singleton intlist from an
int? Basically, I want to do this:

fn intlist1(i:int): intlist = intlist_cons(i, intlist_nil)

but that doesn’t work. Is there a way to do this? In general, is there a
way to define pure-functional forms in the statics, not just their
interfaces?

– Jonathan

2

In ATS, recursive functions cannot be defined directly in the statics.

To get something like ‘append’, one needs to declare a dataprop in the
dynamics of ATS that captures the relation induced by the ‘append’ function.
Following code may be useful for understanding this.

http://www.ats-lang.org/LIBRARY/libats/ilist_prf.html
http://www.ats-lang.org/LIBRARY/libats/gflist.html
http://www.ats-lang.org/LIBRARY/libats/gflist_vt.html

3

I got a little further:

stadef intlist1(i:int) = intlist_cons(i, intlist_nil)

The manual said nothing about stadef being used this way - it implied
stadef only aliased symbols, not defined functions. I just tried a
bunch of things until I stumbled on this.

However, this doesn’t work:

stadef intlist_append(xs:intlist, ys:intlist) =
scase+ xs of
| intlist_cons(x, xs) => x :: intlist_append(xs, ys)
| intlist_nil => ys

atscc says this has a syntax error right at scase+ (case+ doesn’t work
there, either). Is there some restriction on stadef? Is there some
other construct to use?

– Jonathan

4

“stadef” can be viewed as definition of macro in the statics. By “stadef”,
we can define some very simple functions in the statics. However we cannot
use “scase”, “if”, let alone recursive functions. So most of time it’s a
bad idea trying to define functions in the statics. I think that’s the
design of ATS, pushing the definition of complex relations out of statics
into dynamics. So that it’s the programmers’ responsibility to construct
proof for the validity of those relations.

I make up a simple example. The following code is similar to what you want
to do conceptually, but it won’t compile in ATS at all.

datasort foo =
| hello | bye

stadef encode (x: foo) =
scase x of
| hello () => 1
| bye () => 2

datatype Foo (foo) =
| Hello (hello)
| Bye (bye)

fun Encode {x: foo} (X: Foo x): int (encode (x)) =
case+ X of
| Hello () => 1
| Bye () => 2

A better practice in ATS would be something like the following.

datasort foo =
| hello | bye

dataprop encode (x:foo, n:int) =
| hello_rel (hello, 1)
| bye_rel (bye, 2)

datatype Foo (foo) =
| Hello (hello)
| Bye (bye)

fun Encode {x: foo} (X: Foo x): [n: int] (encode (x, n) | int n) =
case+ X of
| Hello () => (hello_rel () | 1)
| Bye () => (bye_rel () | 2)