ATS

ATS (Applied Type System) is a programming language designed to unify programming with formal specification. It combines features from functional and imperative programming paradigms and places a strong emphasis on static verification through its advanced type system, which includes dependent types and linear types. This allows for the prevention of common programming errors, such as null pointer dereferences and buffer overflows, at compile time.

A key feature of ATS is its ability to interoperate seamlessly with C. ATS code can be compiled to C code, which is then compiled by a standard C compiler like GCC. This makes it highly efficient and allows for easy integration with existing C libraries and systems.

Its focus on safety and performance makes it suitable for systems programming, including embedded and low-level development, where reliability and efficiency are critical.

Hello World

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

// A perfunctory check of species. Assumed to be true for the operator.
fun is_human (): bool = true

// A check of planetary origin. The alternative is too complex to contemplate.
fun is_on_earth (): bool = true

// All preconditions must be satisfied before proceeding.
fun conditions_are_met (): bool = is_human () && is_on_earth ()

// A function that, upon confirmation of satisfactory preconditions,
// produces the contractually obligated greeting.
fun produce_utterance (): string = "Hello World!\n"

// BEGIN_FRAGLET
implement main0 () =
  if conditions_are_met () then
    print (produce_utterance ())
  else
    // A state of affairs so unlikely as to be considered impossible.
    // In such a case, silence is the only option.
    ()
// END_FRAGLET

Coding Guide

Language Version

ATS2-Postiats 0.4.2

Execution Model

• Compiled language using patscc (ATS compiler)
• Code is compiled to a binary, then executed
• Standard ATS execution model with main0() function

Key Characteristics

• Statically typed with advanced type system (dependent types, linear types)
• Functional and imperative programming paradigms
• Case-sensitive
• Requires explicit compilation step
• Strong emphasis on formal specification and static verification
• Seamless C interoperation (compiles to C)

Fragment Authoring

Write valid ATS code that implements main0(). Your fragment will be compiled and executed.

Fragments can include:

• #include directives — You can put #include lines at the top of your fragment. They are injected into the compiled file and processed by the preprocessor, so extra libraries are available for that fragment only.
• Function definitions
• Variable declarations
• Control flow (if/else, loops)
• Print statements
• Type annotations

Includes and libraries

The container template already has at the top of the file:

• #include "share/atspre_staload.hats"
• #include "share/atspre_staload_libats_ML.hats"

So most fragments do not need to add includes. When you need another library, add the corresponding #include at the top of your fragment (e.g. #include "share/HATS/atspre_staload_libats_ML.hats" or a libc SATS path). Paths are resolved relative to the compiler’s search path (e.g. PATSHOME).

Available Libraries

With the default template includes you can use:

• Standard I/O: print, println!, print_string
• Command-line args: main0{n}(argc, argv) and listize_argc_argv(argc, argv) (from ML lib)
• Stdin: stdin_ref and streamize_fileref_line(stdin_ref) (from ML lib)
• C interoperation

Command-line arguments

Use the overloaded entry point main0{n}(argc, argv) and convert to a list with listize_argc_argv:

implement main0{n}(argc, argv): void =
  let
    val args = listize_argc_argv(argc, argv)
  in
    list0_foreach(args, lam(arg) => println!(arg))
  end

The execution script runs the binary with "$@", so arguments passed to the container appear as argv.

Stdin

Read lines from standard input with streamize_fileref_line(stdin_ref):

implement main0() =
  let
    val lines = streamize_fileref_line(stdin_ref)
    val () = lines.foreach()(lam x => println!(x))
  in () end

For a single line you can use the stream’s head() or iterate as above.

Common Patterns

• Print: print ("message\n") or println!(x)
• Variables: val x = 10
• Functions: fun add (a: int, b: int): int = a + b
• Conditionals: if condition then expr1 else expr2
• Loops: for* {i:nat | i <= n} .<n-i>. (i: int i) => ...

Examples

// Simple output
implement main0 () =
  print ("Hello from fragment!\n")

// Variables
implement main0 () =
  let
    val message = "Variables work\n"
  in
    print (message)
  end

// Conditional output
implement main0 () =
  if true then
    print ("Condition is true\n")
  else
    print ("Condition is false\n")

// Multiple print statements (using parentheses and semicolons)
implement main0 () =
  (print ("First line\n"); print ("Second line\n"); print ("Third line\n"))

Caveats

• Fragments must be valid ATS code that compiles
• Remember to include \n in print statements for newlines
• Use main0() for no-arg entry or main0{n}(argc, argv) for command-line arguments (only one entry point per fragment)
• ATS has strict type checking - type errors will prevent compilation
• Code is compiled fresh each time, so compilation errors will fail execution
• Use print or println! for output. For formatted output with numbers, convert to strings or use C interoperation

Fraglet Scripts

Echo Args

#!/usr/bin/env -S fragletc --vein=ats
implement main0{n}(argc, argv): void =
  let
    val args = listize_argc_argv(argc, argv)
  in
    list0_foreach(args, lam(arg) => println!(arg))
  end

Stdin Echo

#!/usr/bin/env -S fragletc --vein=ats
implement main0() =
  let
    val lines = streamize_fileref_line(stdin_ref)
    val () = lines.foreach()(lam x => println!(x))
  in () end

Stdin Upper

#!/usr/bin/env -S fragletc --vein=ats
implement main0() =
  let
    val lines = streamize_fileref_line(stdin_ref)
    val () = lines.foreach()(lam x => println!(x))
  in () end

Test

#!/usr/bin/env -S fragletc --vein=ats
implement main0 () =
  if conditions_are_met () then
    print (produce_utterance ())
  else
    // A state of affairs so unlikely as to be considered impossible.
    // In such a case, silence is the only option.
    ()

Connections

Container Info