АТС (язык программирования)

АТС

Парадигмы	мультипарадигмальность : функциональная , императивная , объектно-ориентированная , параллельная , модульная.
Семья	ML : Caml : OCaml : Зависимый ML
Разработано	Хунвэй Си
Разработчик	Бостонский университет
Впервые появился	2006 год ( 2006 )
Стабильная версия	АТС2-0.4.2 / 14 ноября 2020 г ( 14.11.2020 )
Дисциплина набора текста	статический , зависимый
Лицензия	лицензия GPLv3
Расширения имен файлов	.sats, .dats, .hats
Веб-сайт	www .все нормально .org
Под влиянием
Зависимое машинное обучение , машинное обучение , OCaml , C++

В вычислительной технике ( Applied Type System ) — это многопарадигмальный , общего назначения , высокоуровневый ATS функциональный язык программирования . Это диалект языка программирования ML , разработанный Хунвэй Си для объединения компьютерного программирования с формальной спецификацией . ATS поддерживает объединение доказательства теорем с практическим программированием за счет использования передовых систем типов . Предыдущая версия игры The Computer Language Benchmarks Game продемонстрировала, что производительность ATS сопоставима с производительностью языков C и C++ . Используя доказательство теорем и строгую проверку типов, компилятор может обнаружить и доказать, что реализованные им функции не подвержены таким ошибкам, как деление на ноль , утечки памяти , переполнение буфера и другие формы повреждения памяти , проверяя арифметику указателей и подсчет ссылок перед этим. программа компилируется. Кроме того, используя интегрированную систему доказательства теорем ATS (ATS/LF), программист может использовать статические конструкции, которые переплетаются с оперативным кодом, чтобы доказать, что функция соответствует своей спецификации.

ATS состоит из статического компонента и динамического компонента. Статический компонент используется для обработки типов, тогда как динамический компонент используется для программ. Хотя в своей основе ATS в первую очередь опирается на функциональный язык с вызовом по значению, он обладает способностью адаптировать различные парадигмы программирования , такие как функциональная , императивная , объектно-ориентированная , параллельная и модульная .

История

По словам автора, ATS был вдохновлен конструктивной теорией типов Мартина-Лёфа , которая изначально была разработана с целью заложить основы математики. Си разработал ATS «в попытке объединить спецификацию и реализацию в едином языке программирования».

ATS происходит главным образом от языков ML и OCaml . Более ранний язык Dependent ML того же автора был включен в ATS.

Первая реализация, ATS/Proto (ATS0), была написана на OCaml и выпущена в 2006 году. Это была предварительная версия ATS, и она больше не поддерживается. Год спустя была выпущена ATS/Geizella, первая реализация ATS1. Эта версия также была написана на OCaml и больше активно не используется.

Вторая версия ATS1, ATS/Anairiats, выпущенная в 2008 году, стала важной вехой в развитии языка, поскольку язык мог самозагружаться . Эта версия почти полностью написана на ATS1. Текущая версия ATS/Postiats (ATS2) была выпущена в 2013 году. Как и ее предшественница, эта версия также почти полностью написана на ATS1. Самая последняя выпущенная версия — ATS2-0.4.2.

Будущее

По состоянию на 2024 год , ATS используется в основном для исследований; менее 200 репозиториев GitHub содержат код, написанный на ATS. Это намного меньше, чем у других функциональных языков, таких как OCaml и Standard ML, которые имеют более 16 000 и 3 000 репозиториев соответственно. Вероятно, это связано с необходимостью сложного обучения, связанного с ATS, которое присутствует из-за использования в языке проверки зависимых типов и разрешения экземпляров шаблонов. Эти функции обычно требуют использования явных кванторов , что требует дальнейшего изучения.

По состоянию на 2024 год , ATS/Xanadu (ATS3) активно разрабатывается в ATS2 с надеждой сократить необходимое обучение за счет двух основных улучшений:

• Добавление дополнительного уровня в ATS2 для поддержки ML-подобной типов. алгебраической проверки
• на основе типов Метапрограммирование с использованием только алгебраических типов

Си Цзиньпин надеется, что благодаря этим улучшениям ATS станет намного более доступным и простым в освоении. Основная цель ATS3 — превратить ATS из языка, используемого в основном для исследований, в язык, достаточно мощный для крупномасштабной промышленной разработки программного обеспечения.

Доказательство теоремы

Основное внимание ATS уделяется поддержке формальной проверки посредством автоматического доказательства теорем в сочетании с практическим программированием. Доказательство теорем может, например, доказать, что реализованная функция не вызывает утечек памяти. Это также может предотвратить другие ошибки, которые в противном случае могли бы быть обнаружены только во время тестирования. Он включает в себя систему, аналогичную системам помощников по доказательству , которые обычно направлены только на проверку математических доказательств, за исключением того, что ATS использует эту способность, чтобы доказать, что реализации его функций работают правильно и дают ожидаемый результат.

В качестве простого примера: в функции, использующей деление, программист может доказать, что делитель никогда не будет равен нулю, предотвращая ошибку деления на ноль . Допустим, делитель «X» был вычислен как 5-кратная длина списка «А». Можно доказать, что в случае непустого списка «X» не равно нулю, поскольку «X» является произведением двух ненулевых чисел (5 и длины «A»). Более практичным примером было бы доказать с помощью подсчета ссылок , что счетчик сохранения в выделенном блоке памяти подсчитывается правильно для каждого указателя. Тогда можно будет знать и буквально доказать, что объект не будет освобожден преждевременно и что утечек памяти не произойдет.

Преимущество системы ATS в том, что, поскольку все доказательства теорем происходят строго внутри компилятора, это не влияет на скорость исполняемой программы. Код ATS часто сложнее компилировать, чем стандартный код C , но как только он компилируется, можно быть уверенным, что он работает правильно в той степени, которая указана в доказательствах (при условии, что компилятор и система времени выполнения корректны).

В ATS доказательства отделены от реализации, поэтому при желании можно реализовать функцию без ее доказательства.

Представление данных

По мнению автора, эффективность АТС во многом связано со способом представления данных на языке и оптимизацией хвостовых вызовов (которые обычно важны для эффективности функциональных языков). Данные могут храниться в плоском или неупакованном представлении, а не в коробочном представлении.

случай

Предложения

dataprop выражает предикаты как алгебраические типы .

Предикаты в псевдокоде чем-то похожи на источник ATS (действительный источник ATS см. ниже):

 FACT(n, r)         iff    fact(n) = r
 MUL(n, m, prod)    iff    n * m = prod
  
 FACT(n, r) = 
       FACT(0, 1) 
     | FACT(n, r) iff FACT(n-1, r1) and MUL(n, r1, r)   // for n > 0
 
 // expresses fact(n) = r  iff  r = n * r1  and  r1 = fact(n-1)

В коде АТС:

 dataprop FACT (int, int) =
   | FACTbas (0, 1)             // basic case: FACT(0, 1)
   | {n:int | n > 0} {r,r1:int} // inductive case
     FACTind (n, r) of (FACT (n-1, r1), MUL (n, r1, r))

где FACT (int, int) — тип доказательства

Пример

Нехвостовой рекурсивный факториал с утверждением или « теоремой », доказывающий посредством конструкции dataprop .

Оценка fact1(n-1) возвращает пару (proof_n_minus_1 | result_of_n_minus_1) который используется при расчете fact1(n). Доказательства выражают предикаты предложения.

Часть 1 (алгоритм и предложения)

 [FACT (n, r)] implies [fact (n) = r]
 [MUL (n, m, prod)] implies [n * m = prod]

 FACT (0, 1)
 FACT (n, r) iff FACT (n-1, r1) and MUL (n, r1, r) forall n > 0

Чтобы помнить:

{...} universal quantification
[...] existential quantification
(... | ...)   (proof | value)
@(...) flat tuple or variadic function parameters tuple
.<...>. termination metric

#include "share/atspre_staload.hats"

dataprop FACT (int, int) =
  | FACTbas (0, 1) of () // basic case
  | {n:nat}{r:int}       // inductive case
    FACTind (n+1, (n+1)*r) of (FACT (n, r))

(* note that int(x) , also int x, is the monovalued type of the int x value.

 The function signature below says:
 forall n:nat, exists r:int where fact( num: int(n)) returns (FACT (n, r) | int(r)) *)

fun fact{n:nat} .<n>. (n: int (n)) : [r:int] (FACT (n, r) | int(r)) =
(
  ifcase
  | n > 0 => ((FACTind(pf1) | n * r1)) where 
  { 
    val (pf1 | r1) = fact (n-1)
  }
  | _(*else*) => (FACTbas() | 1)
)

Часть 2 (программы и тест)

implement main0 (argc, argv) =
{
  val () = if (argc != 2) then prerrln! ("Usage: ", argv[0], " <integer>")

  val () = assert (argc >= 2)
  val n0 = g0string2int (argv[1])
  val n0 = g1ofg0 (n0)
  val () = assert (n0 >= 0)
  val (_(*pf*) | res) = fact (n0)

  val ((*void*)) = println! ("fact(", n0, ") = ", res)
}

Все это можно добавить в один файл и скомпилировать следующим образом. Компиляция должна работать с различными серверными компиляторами C, например, GNU Compiler Collection (gcc). Сбор мусора не используется, если это явно не указано в -D_ATS_GCATS )

$ patscc fact1.dats -o fact1
$ ./fact1 4

компилирует и выдает ожидаемый результат

Особенности

Основные типы

• bool (истина, ложь)
• int (литералы: 255, 0377, 0xFF), унарный минус как ~ (как в ML )
• двойной
• символ 'а'
• строка «абв»

Кортежи и записи

префикс @ или none означает прямое, фиксированное или неупакованное распределение.

  val x : @(int, char) = @(15, 'c')  // x.0 = 15 ; x.1 = 'c'
  val @(a, b) = x                    // pattern matching binding, a= 15, b='c'
  val x = @{first=15, second='c'}    // x.first = 15
  val @{first=a, second=b} = x       // a= 15, b='c'
  val @{second=b, ...} = x           // with omission, b='c'

префикс ' означает косвенное или коробочное выделение

  val x : '(int, char) = '(15, 'c')  // x.0 = 15 ; x.1 = 'c'
  val '(a, b) = x                    // a= 15, b='c'
  val x = '{first=15, second='c'}    // x.first = 15
  val '{first=a, second=b} = x       // a= 15, b='c'
  val '{second=b, ...} = x           // b='c'

особенный

С '|' в качестве разделителя некоторые функции возвращают значение результата с оценкой предикатов

val ( predicate_proofs | values) = myfunct params

Общий

{...} universal quantification
[...] existential quantification
(...) parenthetical expression or tuple

(... | ...)     (proofs | values)

.<...>. termination metric

@(...)          flat tuple or variadic function parameters tuple (see example's printf)

@[byte][BUFLEN]     type of an array of BUFLEN values of type byte
@[byte][BUFLEN]()   array instance
@[byte][BUFLEN](0)  array initialized to 0

Словарь

сортировка:домен

sortdef nat = {a: int | a >= 0 }     // from prelude: ∀ a ∈ int ...

typedef String = [a:nat] string(a)   // [..]: ∃ a ∈ nat ...

тип (как сортировка)

универсальная сортировка для элементов с длиной слова-указателя, которая будет использоваться в параметризованных типом полиморфных функциях. Также «коробочные типы»

// {..}: ∀ a,b ∈ type ...
fun {a,b:type} swap_type_type (xy: @(a, b)): @(b, a) = (xy.1, xy.0)

тип

линейная версия предыдущего типа с абстрактной длиной. Также распакованные типы.

тип представления

класс домена типа типа с представлением (ассоциация памяти)

просмотр@тип

линейная версия типа представления с абстрактной длиной. Он заменяет тип просмотра

вид

связь Типа и ячейки памяти. Инфикс @ — его самый распространенный конструктор.

T @ L утверждает, что в позиции L существует представление типа T

 fun {a:t@ype} ptr_get0 {l:addr} (pf: a @ l | p: ptr l): @(a @ l | a)
 
 fun {a:t@ype} ptr_set0 {l:addr} (pf: a? @ l | p: ptr l, x: a): @(a @ l | void)

тип ptr_get0 (T) является ∀ l : addr . ( T @ l | ptr( l ) ) -> ( T @ l | T) // see manual, section 7.1. Safe Memory Access through Pointers

viewdef array_v (a:viewt@ype, n:int, l: addr) = @[a][n] @ l

Т?

возможно неинициализированный тип

полнота сопоставления с образцом

как в случае+ , val+ , type+ , viewtype+ , ...

• с суффиксом '+' компилятор выдает ошибку в случае неполных альтернатив
• без суффикса компилятор выдает предупреждение
• с суффиксом «-» позволяет избежать контроля полноты

модули

 staload "foo.sats" // foo.sats is loaded and then opened into the current namespace

 staload F = "foo.sats" // to use identifiers qualified as $F.bar

 dynload "foo.dats" // loaded dynamically at run-time

просмотр данных

Представления данных часто объявляются для кодирования рекурсивно определенных отношений на линейных ресурсах.

dataview array_v (a: viewt@ype+, int, addr) =
  | {l: addr} array_v_none (a, 0, l)
  | {n: nat} {l: addr}
    array_v_some (a, n+1, l)
    of (a @ l, array_v (a, n, l+sizeof a))

тип данных/тип представления данных

Типы данных

datatype workday = Mon | Tue | Wed | Thu | Fri

списки

datatype list0 (a:t@ype) = list0_cons (a) of (a, list0 a) | list0_nil (a)

тип представления данных

Тип представления данных похож на тип данных, но он линейный. При использовании типа представления данных программисту разрешено явно освободить (или освободить) безопасным способом память, используемую для хранения конструкторов, связанных с типом представления данных.

переменные

локальные переменные

var res: int with pf_res = 1   // introduces pf_res as an alias of view @ (res)

при выделении массива стека :

#define BUFLEN 10
var !p_buf with pf_buf = @[byte][BUFLEN](0)    // pf_buf = @[byte][BUFLEN](0) @ p_buf

См. val и var. объявления

Внешние ссылки

• Официальный сайт
• Язык программирования ATS. Архивировано 5 декабря 2014 г. в документации Wayback Machine для ATS2.
• Язык программирования ATS Старая документация для ATS1
• Черновик руководства (устарело). Некоторые примеры относятся к функциям или процедурам, отсутствующим в выпуске (Anairiats-0.1.6) (например: перегрузка печати для strbuf и использование его примеров массива выдает сообщения об ошибках типа «использование подписки на массив не поддерживается».)
• ATS для ML-программистов
• Обучающие примеры и краткие примеры использования ATS