Log of Changes for ATS/Anairiats

The sorts for boxed types and viewtypes are introduced. We now use type and viewtype as the sorts for boxed types and viewtypes, respectively. For unboxed types and viewtypes, the sorts are t@ype and viewt@ype, respectively.

Here are two type definitions for boxed and unboxed pairs of integers:

stadef int2_box: type = '(int, int) // boxed tuple
stadef int2_flt: t@ype = @(int, int) // flat tuple

For a function declaration, the default function kind is now function (FUNCLOfun) instead of closure (FINCLOclo). For example, The following function declaration assigns foo the type T1 -<fun1> T2:

fun foo (x: T1): T2 = ...

In order to assign a closure type to foo, the function kind annoation needs to be supplied as follows:

fun foo (x: T1):<clo1> T2 = ...

It is now allowed for a constructor associtated with a datatype to carry an argument of a linear type. For instance, the datatype for (persistent) lists is now defined as follows:

datatype list (a:viewt@ype+, int) =
  | {n:nat} cons (a, n+1) of (a, list (a, n)) | nil (a, 0)

fun{a:viewt@ype} length {n:nat} (xs: list (a, n)): int n =
  case+ xs of cons (!x, xs) = 1 + length (xs) | nil () => 0