ATS는 의존 타입과 정리 증명을 결합해 높은 성능과 형 안전성을 목표로 하는 ML 계열의 함수형·명령형·동시·모듈식 멀티 패러다임 프로그래밍 언어이다.
ATS (프로그래밍 언어)
위키백과, 우리 모두의 백과사전에서
컴퓨팅에서 ATS(Applied Type System)는 멀티 패러다임, 범용, 고수준, 함수형프로그래밍 언어이다. 프로그래밍 언어 ML의 방언으로, Hongwei Xi가 컴퓨터 프로그래밍과 형식 명세를 통합하기 위해 설계했다. ATS는 고급 타입 시스템을 이용해 정리 증명과 실용 프로그래밍을 결합하는 것을 지원한다.[2] 과거 버전의 The Computer Language Benchmarks Game은 ATS의 성능이 C와 C++에 필적함을 보여 주었다.[3] ATS는 정리 증명과 엄격한 타입 체크를 사용함으로써, 컴파일러가 구현된 함수가 0으로 나누기, 메모리 누수, 버퍼 오버플로 및 기타 형태의 메모리 손상과 같은 버그에 취약하지 않음을, 포인터 산술과 참조 카운팅을 프로그램 실행 전에 검증함으로써 감지하고 증명할 수 있다. 또한 ATS의 통합 정리 증명 시스템(ATS/LF)을 사용하면, 프로그래머는 동작 코드와 뒤섞인 정적 구성 요소를 이용해 함수가 그 명세를 만족함을 증명할 수 있다.
ATS는 정적 구성 요소와 동적 구성 요소로 이루어져 있다. 정적 구성 요소는 타입을 다루는 데 사용되고, 동적 구성 요소는 프로그램을 다루는 데 사용된다. ATS는 핵심에서 주로 값 호출(call-by-value) 함수형 언어에 의존하지만, 함수형, 명령형, 객체 지향, 동시성, 모듈식 등 다양한 프로그래밍 패러다임을 수용할 수 있다.
저자에 따르면 ATS는 본래 수학의 기초를 확립하기 위해 개발된 Per Martin-Löf의 구성적 타입 이론에서 영감을 받았다. Xi는 ATS를 “명세와 구현을 하나의 프로그래밍 언어로 결합하려는 시도”로 설계했다.[4]
ATS는 주로 ML과 OCaml에서 파생되었다. 같은 저자가 설계한 이전 언어인 Dependent ML은 ATS에 통합되었다.
첫 구현인 ATS/Proto(ATS0)는 OCaml로 작성되었고 2006년에 공개되었다. 이는 ATS의 예비 1판으로, 더 이상 유지보수되지 않는다. 1년 뒤 ATS1의 첫 구현인 ATS/Geizella가 공개되었다. 이 버전 역시 OCaml로 작성되었고 현재는 더 이상 적극적으로 사용되지 않는다.[5]
ATS1의 두 번째 버전인 ATS/Anairiats는 2008년에 공개되었으며, 언어가 스스로를 부트스트랩할 수 있게 된 점에서 언어 개발의 주요 이정표였다. 이 버전은 거의 전부 ATS1로 작성되었다. 현재 버전인 ATS/Postiats(ATS2)는 2013년에 공개되었다. 전임자와 마찬가지로 이 버전 또한 거의 전적으로 ATS1로 작성되었다. 가장 최근에 공개된 버전은 ATS2-0.4.2이다.[5]
2024년 기준으로 ATS는 주로 연구 목적으로 사용되며, ATS 코드가 포함된 GitHub 저장소는 200개 미만이다. 이는 OCaml과 Standard ML처럼 16,000개, 3,000개 이상의 저장소를 보유한 다른 함수형 언어에 비해 훨씬 적다. 이는 ATS의 학습 곡선이 가파르기 때문일 가능성이 크며, 그 원인은 언어가 의존 타입 검사와 템플릿 인스턴스 해석을 사용하기 때문이다. 이러한 기능은 보통 명시적인 양화사 사용을 요구하며, 이는 추가 학습을 필요로 한다.[6]
2024년 현재 ATS/Xanadu(ATS3)는 ATS2로 적극적으로 개발되고 있으며, 다음 두 가지 주요 개선을 통해 학습 부담을 줄이는 것을 목표로 한다.
이러한 개선을 통해 Xi는 ATS가 훨씬 더 접근 가능하고 배우기 쉬운 언어가 되기를 기대한다. ATS3의 주요 목표는 ATS를 주로 연구에 사용되는 언어에서, 대규모 산업용 소프트웨어 개발에 충분히 강력한 언어로 전환하는 것이다.[5]
ATS의 주요 초점은 자동 정리 증명을 통한 형식 검증을 실용적인 프로그래밍과 결합해 지원하는 것이다.[2] 정리 증명은 예를 들어, 구현된 함수가 메모리 누수를 일으키지 않음을 증명할 수 있다. 또한 그렇지 않다면 테스트 과정에서만 발견될 수 있는 다른 버그들을 예방할 수 있다. ATS는 보통 수학적 증명만을 검증하는 데 목표를 두는 증명 보조기와 유사한 시스템을 통합하지만, ATS는 이 능력을 함수 구현이 올바르게 동작하고 예상되는 출력을 생성함을 증명하는 데 사용한다.
간단한 예로, 나눗셈을 사용하는 함수에서 프로그래머는 나누는 수가 결코 0이 되지 않음을 증명함으로써 0으로 나누기 오류를 방지할 수 있다. 예를 들어, 나누는 수 X가 리스트 A의 길이에 5를 곱해 계산되었다고 하자. 비어 있지 않은 리스트의 경우, X는 두 개의 0이 아닌 수(5와 A의 길이)의 곱이므로 0이 아님을 증명할 수 있다. 더 실용적인 예로는 참조 카운팅을 통해, 할당된 메모리 블록에 대한 보유 카운트가 각 포인터에 대해 올바르게 계산되고 있음을 증명하는 것이다. 그러면 객체가 조기에 해제되지 않으며, 메모리 누수가 발생하지 않을 것임을 알고, 문자 그대로 증명할 수 있다.
ATS 시스템의 이점은 모든 정리 증명이 엄격히 컴파일러 내부에서 수행되므로, 실행 파일의 속도에 아무런 영향을 미치지 않는다는 점이다. ATS 코드는 일반적인 C 코드보다 컴파일하기 어려운 경우가 많지만, 일단 컴파일되면 (컴파일러와 런타임 시스템이 올바르다고 가정할 때) 증명으로 지정된 정도까지 올바르게 동작함이 보장된다.
ATS에서 증명은 구현과 분리되어 있으므로, 원한다면 증명 없이 함수를 구현하는 것도 가능하다.
[편집]
저자에 따르면 ATS의 효율성[7]은 주로 언어에서 데이터가 표현되는 방식과 꼬리 호출 최적화(이는 일반적으로 함수형 언어의 효율성에 중요하다) 덕분이다. 데이터는 박스드(boxed) 표현이 아니라 평탄(flat) 또는 언박스드(unboxed) 표현으로 저장될 수 있다.
[편집]
dataprop은 _술어_를 대수적 타입으로 표현한다.
ATS 소스와 다소 유사한 의사 코드에서의 술어(아래에 실제 ATS 소스 참조):
FACT(n, r) [iff](https://en.wikipedia.org/wiki/If_and_only_if "If and only if") fact(n) = r
MUL(n, m, prod) [iff](https://en.wikipedia.org/wiki/If_and_only_if "If and only if") 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](https://en.wikipedia.org/wiki/If_and_only_if "If and only if") r = n * r1 and r1 = fact(n-1)
ATS 코드에서는 다음과 같다.
atsdataprop 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)의 계산에 사용된다. 이 증명들은 명제의 술어를 표현한다.
[편집]
[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)@(...) 평탄 튜플 또는 가변 인자 함수의 매개변수 튜플.<...>. 종료 메트릭[8]ats#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) )
[편집]
atsimplement 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) }
이는 모두 하나의 파일에 넣어 다음과 같이 컴파일할 수 있다. 컴파일은 GNU 컴파일러 컬렉션(gcc) 등 다양한 C 백엔드 컴파일러로 동작해야 한다. 가비지 컬렉션은 -D_ATS_GCATS로 명시적으로 지정하지 않는 한 사용되지 않는다.[9]
bash$ patscc fact1.dats -o fact1 $ ./fact1 4
위 명령은 컴파일 후 예상한 결과를 출력한다.
bool (true, false)int (리터럴: 255, 0377, 0xFF), 단항 음수는 ML과 같이 ~ 사용doublechar 'a'"abc"접두사 @ 또는 없음: 직접, 평탄(flat) 또는 언박스드 할당
atsval 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'
접두사 ': 간접 또는 박스드 할당
atsval 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'
특수 구문: |를 구분자로 사용하여, 일부 함수는 결과 값을 술어 평가와 함께 래핑해서 반환한다.
atsval ( predicate_proofs | values) = myfunct params
{...} 전칭 양화[...] 존재 양화(...) 괄호식 또는 튜플(... | ...) (proofs | values).<...>. 종료 메트릭@(...) 평탄 튜플 또는 가변 인자 함수 매개변수 튜플 (예제의 printf 참조)@[byte][BUFLEN] 타입 byte 값 BUFLEN개로 이루어진 배열의 타입[10]@[byte][BUFLEN]() 배열 인스턴스@[byte][BUFLEN](0) 0으로 초기화된 배열atssortdef nat = {a: int | a >= 0 } // prelude에서: ∀ ''a'' ∈ int ... typedef String = [a:nat] string(a) // [..]: ∃ ''a'' ∈ nat ...
type (정렬로서)는 포인터 워드 길이의 요소를 위한 일반적인 _sort_로, 타입 매개변수화된 다형 함수에서 사용된다. 또한 “박스드 타입”을 의미한다.[11]
ats// {..}: ∀ a,b ∈ type ... fun {a,b:type} swap_type_type (xy: @(a, b)): @(b, a) = (xy.1, xy.0)
t@ype는 위의 type의 선형(linear) 버전으로, 길이가 추상화되어 있다. 또한 언박스드 타입이다.[11]
viewtype은 메모리 연관성(view)을 가지는, type과 같은 도메인 클래스이다.
viewt@ype는 길이가 추상화된 viewtype의 선형 버전이다. 이는 viewtype을 상위 개념으로 포함하며, 타입과 메모리 위치 간의 뷰 관계를 표현한다. 중위 연산자 @는 가장 일반적인 생성자이며, T @ L은 위치 L에 타입 T의 뷰가 존재함을 주장(assert)한다.
atsfun {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)자세한 내용은 매뉴얼 7.1절 "포인터를 통한 안전한 메모리 접근" 참조[12]
atsviewdef array_v (a:viewt@ype, n:int, l: addr) = @[a][n] @ l
T?는 초기화되지 않았을 수도 있는 타입을 나타낸다.
[편집]
case+, val+, type+, viewtype+ 등에서 사용된다.
+가 있으면, 분기가 완전하지 않을 경우 컴파일러가 오류를 발생시킨다.-를 사용하면, 완전성 검사를 피할 수 있다.atsstaload "foo.sats" // foo.sats를 로드하고 현재 네임스페이스에 연다 staload F = "foo.sats" // 식별자를 $F.bar와 같이 한정해서 사용 dynload "foo.dats" // 실행 시점에 동적으로 로드
Dataview는 종종 선형 자원에 대한 재귀적으로 정의된 관계를 인코딩하기 위해 선언된다.[13]
atsdataview 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))
[편집]
데이터타입[14]
atsdatatype workday = Mon | Tue | Wed | Thu | Fri
리스트
atsdatatype list0 (a:t@ype) = | list0_cons (a) of (a, list0 a) | list0_nil (a)
dataviewtype은 datatype과 유사하지만 선형이다. dataviewtype을 사용하면, 프로그래머는 그 dataviewtype에 연관된 생성자를 저장하는 데 사용된 메모리를 안전한 방식으로 명시적으로 해제(또는 할당 해제)할 수 있다.[15]
atsvar res: int with pf_res = 1 // pf_res를 _view @ (res)_의 별칭으로 도입
스택 상의 배열 할당 예:
ats#define BUFLEN 10 var !p_buf with pf_buf = @[byte][BUFLEN](0) // pf_buf = @[byte][BUFLEN](0) @ p_buf
자세한 내용은 val 및 var 선언을 참조.[17]
@[T][I] 형태의 타입.strbuf에 대한 print 오버로드, 및 배열 예제를 그대로 사용하면 "use of array subscription is not supported"와 같은 오류 메시지가 발생).