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

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

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

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

История [ править ]

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

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

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

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

Будущее [ править ]

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

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

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

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

Доказательство теоремы [ править ]

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

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

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

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

Представление данных [ править ]

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

вводный случай Доказательство теоремы :

Предложения [ править ]

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

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

FACT(n, r)  тогда и только тогда, когда  fact(n) = r 
   MUL(n, m, prod)  тогда и только тогда, когда  n * m = prod 
  
   ФАКТ(n, r) =  
         ФАКТ(0, 1)  
       |   FACT(n, r) тогда и только тогда, когда FACT(n-1, r1) и MUL(n, r1, r) // для n > 0 
 
   // выражает fact(n) = r  тогда и только тогда, когда  r = n * r1 и r1 = fact(n-1)

В коде АТС:

 dataprop   ФАКТ   (  int  ,   int  )   = 
    |    FACTbas   (  0,1     )               //   базовый   случай  :   FACT  (  0,1     ) 
    |    {  п  :  целое   |    n   >   0  }   {  r  ,  r1  :  int  }   //   индуктивный   случай 
      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 (алгоритм и предложения) [ править ]

[ФАКТ (n, r)] подразумевает [факт (n) = r]
  [MUL(n, m, prod)] подразумевает [n * m = prod]

ФАКТ (0, 1)
  FACT (n, r) тогда и только тогда, когда FACT (n-1, r1) и MUL (n, r1, r) для всех n > 0

Запомнить:

{...} универсальная количественная оценка
 [...] экзистенциальная количественная оценка
 (... | ...) (доказательство | значение)
 @(...) плоский кортеж или кортеж параметров переменной функции
 .<...>.  метрика завершения ^[8]

#  включаем   "share/atspre_staload.hats" 

 dataprop   FACT   (  int  ,   int  )   = 
   |    FACTbas   (  0  ,   1  )   of   ()   //   базовый   случай 
   |    {  n  :  nat  }{  r  :  int  }         //   индуктивный   случай 
     FACTind   (  n  +  1  ,   (  n  +  1  )*  r  )   of   (  FACT   (  n  ,   r  )) 

 (* обратите внимание, что int(x) , также int x, — это однозначный тип значения int x. 

 Сигнатура функции ниже гласит: 
 forall n:nat, существует r:int где fact( num: int(n)) возвращает (FACT (n, r) | int(r)) * ) 

 забавный   факт  {  n  :  nat  }   .<  n  >.    (  n  :   int   (  n  ))   :   [  r  :  int  ]   (  FACT   (  n  ,   r  )   |   int  (  r  ))   = 
 ( 
   ifcase 
   |   n   >   0   =>   ((  FACTind  (  pf1  )   |   n   *   r1  ))   где  
   {  
     val   (  pf1   |   r1  )   =   факт   (  n  -  1  ) 
   } 
   _   =  (*else*)   >   (  FACTbas  ()   |   1  ) 
 )

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

реализовать   main0   (  argc  ,   argv  )   = 
 { 
   val   ()   =   if   (  argc   !=   2  )   , то   prerrln  !    (  "Использование: "  ,   argv  [  0  ],   " <integer>"  ) 

   val   ()   =   утверждать   (  argc   >=   2  ) 
   val   n0   =   g0string2int   (  argv  [  1  ]) 
   val   n0   =   g1ofg0   (  n0  ) 
   val   ()   =   утверждать   (  n0   >=   0  ) 
   val   (_  (*pf*)   |   res  )   =   факт   (  n0  ) 

   val   (  (*void*)  )   =   println  !    (  "факт("  ,   n0  ,   ") = "  ,   рез  ) 
 }

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

$  patscc   fact1.dats   -o   факт1 
  $  ./факт1   4

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

Особенности [ править ]

Основные типы [ править ]

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

Кортежи и записи [ править ]

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

  val   x   :   @(  int  ,   char  )   =   @(  15  ,   'c'  )    //   x  .   0   =   15   ;    Икс  .   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   x   :   '  (  int  ,   char  )   =   '  (  15  ,   'c'  )    //   x  .   0   =   15   ;    Икс  .   1   =   'c' 
   val   '  (  a  ,   b  )   =   x                      //   a  =   15  ,   b  =  'c' 
   val   x   =   '  {  first  =  15  ,   второй  =  'c'  }      //   x  .   первый   =   15 
   val   '  {  первый  =  a  ,   второй  =  b  }   =   x         //   a  =   15  ,   b  =  'c' 
   val   '  {  второй  =  b  ,   ...}   =   x             //   b  =  'c'

особенный

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

val  (predicate_proofs | значения) = параметры myfunct

Общий [ править ]

{...} универсальная количественная оценка
 [...] экзистенциальная количественная оценка
 (...) выражение в скобках или кортеж

 (... | ...) (доказательства | значения)

.<...>.   метрика завершения 

  @(...) плоский кортеж или  кортеж параметров переменной функции  (см. пример  printf  ) 

  @[byte][BUFLEN] тип массива значений BUFLEN типа  byte ^[10]Экземпляр массива @[byte][BUFLEN]()
 @[byte][BUFLEN](0) массив инициализирован значением 0

Словарь [ править ]

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

sortdef nat = {a: int |   a >= 0 } // из прелюдии: ∀  a  ∈ int ...

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

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

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

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

тип

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

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

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

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

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

вид

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

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  }   (  пф  :   а  л   @   |   |   р  :   птр   л  ,   х  :   а  ):   @  а   @   л   )   пустота  (

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

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

Т?

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

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

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

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

модули [ править ]

staload "foo.sats" // foo.sats загружается, а затем открывается в текущем пространстве имен

  staload F = "foo.sats" // для использования идентификаторов, квалифицированных как $F.bar

  dynload "foo.dats" // загружается динамически во время выполнения

просмотр данных [ править ]

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

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

тип данных / тип представления данных [ изменить ]

Типы данных ^[14]

тип данных рабочий день = Пн |  Вт |  Ср |  Чт |  Пт

списки

тип данных list0 (a:t@ype) = list0_cons (a) of (a, list0 a) |  list0_nil (а)

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

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

переменные [ править ]

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

var res: int with pf_res = 1 // представляет pf_res как псевдоним представления  @ (res)

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

#define БУФЛЕН 10
 var !p_buf с pf_buf = @[byte][BUFLEN](0) // pf_buf = @[byte][BUFLEN](0) @ p_buf ^[16]

См val и var. . объявления ^[17]

Ссылки [ править ]

^ Си Цзиньпин, Хунвэй (14 ноября 2020 г.). «[ats-lang-users] Выпущен ATS2-0.4.2» . ats-lang-пользователи . Проверено 17 ноября 2020 г. .
^ Перейти обратно: ^а ^б «Сочетание программирования с доказательством теорем» (PDF) . Архивировано из оригинала (PDF) 29 ноября 2014 г. Проверено 18 ноября 2014 г.
^ Тесты ATS | Игра Computer Language Benchmarks (веб-архив)
^ «Введение в программирование в АТС» . ats-lang.github.io . Проверено 23 февраля 2024 г.
^ Перейти обратно: ^а ^б ^с «АТС-ПЛ-СИС» . www.cs.bu.edu . Проверено 23 февраля 2024 г.
^ Перейти обратно: ^а ^б Си, Хунвэй (17 февраля 2024 г.). "githwxi/ATS-Занаду" . Гитхаб . Проверено 23 февраля 2024 г.
^ Обсуждение эффективности языка (Language Shootout: ATS — новый лучший стрелок. Превосходит C++.)
^ «Метрики завершения» . Архивировано из оригинала 18 октября 2016 г. Проверено 20 мая 2017 г.
↑ Сборник — Сбор мусора. Архивировано 4 августа 2009 г., в Wayback Machine.
^ тип массива. Архивировано 4 сентября 2011 г., в типах Wayback Machine , таких как @[T][I]
^ Перейти обратно: ^а ^б «Введение в зависимые типы» . Архивировано из оригинала 12 марта 2016 г. Проверено 13 февраля 2016 г.
^ Руководство, раздел 7.1. Безопасный доступ к памяти через указатели ^{[ постоянная мертвая ссылка ]} (устарело)
^ Конструкция Dataview. Архивировано 13 апреля 2010 г. в Wayback Machine .
↑ Конструкция типа данных. Архивировано 14 апреля 2010 г., в Wayback Machine.
^ Конструкция типа представления данных
↑ Руководство — 7.3 Распределение памяти в стеке. Архивировано 9 августа 2014 г. на Wayback Machine (устарело).
^ Декларации Val и Var. Архивировано 9 августа 2014 г. в Wayback Machine (устарело).

Внешние ссылки [ править ]

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

[1] Си Цзиньпин, Хунвэй (14 ноября 2020 г.). «[ats-lang-users] Выпущен ATS2-0.4.2» . ats-lang-пользователи . Проверено 17 ноября 2020 г. .

[ats-lang.org-2] Перейти обратно: ^а ^б «Сочетание программирования с доказательством теорем» (PDF) . Архивировано из оригинала (PDF) 29 ноября 2014 г. Проверено 18 ноября 2014 г.

[3] Тесты ATS | Игра Computer Language Benchmarks (веб-архив)

[4] «Введение в программирование в АТС» . ats-lang.github.io . Проверено 23 февраля 2024 г.

[:0-5] Перейти обратно: ^а ^б ^с «АТС-ПЛ-СИС» . www.cs.bu.edu . Проверено 23 февраля 2024 г.

[:1-6] Перейти обратно: ^а ^б Си, Хунвэй (17 февраля 2024 г.). "githwxi/ATS-Занаду" . Гитхаб . Проверено 23 февраля 2024 г.

[7] Обсуждение эффективности языка (Language Shootout: ATS — новый лучший стрелок. Превосходит C++.)

[8] «Метрики завершения» . Архивировано из оригинала 18 октября 2016 г. Проверено 20 мая 2017 г.

[9] Сборник — Сбор мусора. Архивировано 4 августа 2009 г., в Wayback Machine.

[10] тип массива. Архивировано 4 сентября 2011 г., в типах Wayback Machine , таких как @[T][I]

[introdep-11] Перейти обратно: ^а ^б «Введение в зависимые типы» . Архивировано из оригинала 12 марта 2016 г. Проверено 13 февраля 2016 г.

[12] Руководство, раздел 7.1. Безопасный доступ к памяти через указатели ^{[ постоянная мертвая ссылка ]} (устарело)

[13] Конструкция Dataview. Архивировано 13 апреля 2010 г. в Wayback Machine .

[14] Конструкция типа данных. Архивировано 14 апреля 2010 г., в Wayback Machine.

[15] Конструкция типа представления данных

[16] Руководство — 7.3 Распределение памяти в стеке. Архивировано 9 августа 2014 г. на Wayback Machine (устарело).

[17] Декларации Val и Var. Архивировано 9 августа 2014 г. в Wayback Machine (устарело).

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]