표준 ML
Standard ML| 패러다임 | 멀티패러다임: 기능, 필수, 모듈러[1] |
|---|---|
| 가족 | ML |
| 처음 등장한 | 전[2] |
| 안정된 릴리스 | 표준 ML '97[2]/전( |
| 타이핑 분야 | 추정, 정적, 강력 |
| 파일 이름 확장자 | .sml |
| 웹 사이트 | smlfamily |
| 주요 구현 | |
| SML/NJ, MLton | |
| 사투리 | |
| Alice, 동시 ML, 종속 ML | |
| 영향을 받다 | |
| ML, Hope, Pascal | |
| 영향받은 | |
| Elm, F#, F*, Haskell, OCaml, Python,[3] Rust, Scala | |
표준 ML(SML)은 컴파일 시간 유형 검사 및 유형 추론을 사용하는 범용 모듈러 기능 프로그래밍 언어입니다.컴파일러 라이터와 프로그래밍 언어 연구자들 사이에서는 물론 정리 프로버의 개발에서도 인기가 있습니다.
표준 ML은 LCF(Logic for Computable Functions) 정리 증명 프로젝트에서 사용되는 언어인 ML의 현대 방언입니다.이것은 표준 [4]ML의 정의에서 타이핑 규칙과 운영 의미론으로서 주어진 공식적인 사양을 가지고 있다는 점에서 널리 사용되는 언어들 사이에서 구별된다.
언어
 |
표준 ML은 일부 불순한 기능을 가진 기능적 프로그래밍 언어입니다.표준 ML로 작성된 프로그램은 문장이나 명령어가 아닌 표현식으로 구성되지만 일부 형식 단위의 표현식은 부작용으로만 평가됩니다.
기능들
모든 기능 언어와 마찬가지로 표준 ML의 주요 특징은 추상화에 사용되는 기능입니다.요인 함수는 다음과 같이 표현될 수 있습니다.
재밌어요 요인 n = 한다면 n = 0 그리고나서 1 또 다른 n * 요인 (n - 1) 유형 추론
SML 컴파일러는 정적 유형을 추론해야 합니다.val factorial : int -> int사용자 제공 유형 주석 없음.을 추론해야 한다.n는 정수식에서만 사용되므로 그 자체가 정수여야 하며 모든 단말식이 정수식이어야 합니다.
선언적 정의
if-then-else 조건이 특정 값에 대해 평가된 요인 함수의 템플릿으로 대체되는 Clausal 함수 정의로 동일한 함수를 표현할 수 있다.
재밌어요 요인 0 = 1 요인 n = n * 요인 (n - 1) 명령어 정의
또는 반복:
재밌어요 요인 n = 허락하다 값 i = 레퍼런스 n 그리고. 액세스 = 레퍼런스 1 에 하는 동안에 !i > 0 하다 (액세스 := !acc * !i; i := !i - 1); !acc 끝. 람다 함수
또는 람다 함수로 사용할 수 있습니다.
값 인식하다 요인 = fn 0 => 1 n => n * 요인 (n - 1) 여기서 키워드는val는 ID와 값의 바인딩을 도입하고 있습니다.fn는 어나니머스 기능을 도입하고 있습니다.rec그럼 정의가 자기비대조적이 되도록 할 수 있습니다.
로컬 정의
여기서 보듯이 불변성이 없는 외부 함수 내에서 1개 이상의 어큐뮬레이터 파라미터를 사용하여 불변성을 유지하는 테일재귀적인 타이트루프를 캡슐화하는 것은 표준 ML의 일반적인 관용어입니다.
로컬 기능을 사용하면 보다 효율적인 테일 반복 스타일로 다시 작성할 수 있습니다.
현지의 재밌어요 고리 (0, 액세스) = 액세스 고리 (m, 액세스) = 고리 (m - 1, m * 액세스) 에 재밌어요 요인 n = 고리 (n, 1) 끝. 동의어를 입력하다
type symony는 키워드로 정의됩니다.type평면상의 점의 유형 동의어로, 헤론의 공식에 따라 두 점 사이의 거리 및 주어진 모서리를 가진 삼각형의 면적을 계산하는 함수입니다.(이러한 정의는 다음 예에서 사용됩니다.)
유형 위치 = 진짜 * 진짜 재밌어요 광장 (x : 진짜) = x * x 재밌어요 일그러뜨리다 (x, y) (x', y') = 수학.sqrt (광장 (x' - x) + 광장 (y' - y)) 재밌어요 왜가리 (a, b, c) = 허락하다 값 x = 일그러뜨리다 a b 값 y = 일그러뜨리다 b c 값 z = 일그러뜨리다 a c 값 s = (x + y + z) / 2.0 에 수학.sqrt (s * (s - x) * (s - y) * (s - z)) 끝. 대수 데이터형
표준 ML은 ADT(대수 데이터 유형)를 강력하게 지원합니다.데이터 유형은 튜플의 분리된 결합(또는 "제품의 합")으로 간주할 수 있습니다.대부분의 Standard ML 구현의 패턴-유출성 검사 및 패턴 용장성 검사뿐만 아니라 패턴 매칭에 의해 정의 및 사용이 용이합니다.
오브젝트 지향 프로그래밍 언어에서는 클래스 계층으로서 불연속 결합을 표현할 수 있다.단, 클래스 계층과는 달리 ADT는 닫혀 있습니다.따라서 ADT의 확장성은 클래스 계층의 확장성과 직교한다.클래스 계층은 동일한 인터페이스를 구현하는 새로운 서브클래스로 확장할 수 있으며 ADT의 기능은 고정된 컨스트럭터 세트에 대해 확장할 수 있습니다.표현식 문제를 참조하십시오.
데이터 유형은 키워드로 정의됩니다.datatype예를 들어 다음과 같습니다.
데이터형 모양. = 원형 의 위치 * 진짜 (* 중심 및 반지름 *) 광장 의 위치 * 진짜 (* 왼쪽 상단 모서리 및 측면 길이, 축 정렬 *) 삼각형 의 위치 * 위치 * 위치 (* 모서리 *) 형식 동의어는 재귀적일 수 없습니다. 데이터 유형은 재귀 생성자를 정의하는 데 필요합니다(이 예에서는 문제가 되지 않습니다).
패턴 매칭
패턴은 정의된 순서대로 대조됩니다.C 프로그래머는 태그가 달린 유니언(태그 값에 따라 디스패치)을 사용하여 ML이 데이터 타입과 패턴 매칭을 통해 달성한 것을 달성할 수 있습니다.그럼에도 불구하고, 적절한 체크로 장식된 C 프로그램은 대응하는 ML 프로그램만큼 강력하지만, 이러한 체크는 필연적으로 동적입니다.ML의 정적 체크는 컴파일 시 프로그램의 정확성에 대한 강력한 보증을 제공합니다.
함수 인수는 다음과 같이 패턴으로 정의할 수 있습니다.
재밌어요 지역 (원형 (_, r)) = 수학.파이 * 광장 r 지역 (광장 (_, s)) = 광장 s 지역 (삼각형 p) = 왜가리 p (* 위 참조 *) 인수가 패턴으로 정의되는 함수 정의의 이른바 "절단 형식"은 사례 표현에 대한 통사적 설탕에 불과하다.
재밌어요 지역 모양. = 사례. 모양. 의 원형 (_, r) => 수학.파이 * 광장 r 광장 (_, s) => 광장 s 삼각형 p => 왜가리 p 완전성 체크
패턴-유출성 검사를 통해 데이터 유형의 각 생성자가 하나 이상의 패턴과 일치하는지 확인합니다.
다음 패턴은 완전하지 않습니다.
재밌어요 중심 (원형 (c, _)) = c 중심 (광장 ((x, y), s)) = (x + s / 2.0, y + s / 2.0) 의 패턴은 없습니다.Triangle의 케이스center기능.컴파일러는 대소문자의 표현이 완전하지 않다는 경고를 보냅니다.Triangle실행 시 이 함수에 전달됩니다.exception Match상승합니다.
용장성 체크
다음(의미 없음) 함수의 두 번째 구에 있는 패턴은 다중입니다.
재밌어요 f (원형 ((x, y), r)) = x + y f (원형 _) = 1.0 f _ = 0.0 두 번째 절의 패턴과 일치하는 값은 첫 번째 절의 패턴과도 일치하므로 두 번째 절에는 도달할 수 없습니다.따라서 이 정의는 전체적으로 용장성을 나타내며 컴파일 시 경고가 발생합니다.
다음 함수의 정의는 완전하며 중복되지 않습니다.
값 하드코너 = fn (원형 _) => 거짓의 _ => 진실의 컨트롤이 첫 번째 패턴을 통과한 경우(Circle)의 모양은 다음 중 하나여야 한다는 것을 알고 있습니다.Square또는Triangle어느 경우든 모양에 모서리가 있다는 것을 알 수 있기 때문에 다시 돌아올 수 있습니다.true실제 형태를 구별하지 않고.
고차 함수
함수는 함수를 인수로 사용할 수 있습니다.
재밌어요 지도 f (x, y) = (f x, f y) 함수는 함수를 반환값으로 생성할 수 있습니다.
재밌어요 일정한 k = (fn _ => k) 함수는 또한 다음과 같은 기능을 소비하고 생성할 수 있습니다.
재밌어요 작곡하다 (f, g) = (fn x => f (g x)) 함수List.mapfrom basis library는 표준 ML에서 가장 일반적으로 사용되는 고차 함수 중 하나입니다.
재밌어요 지도 _ [] = [] 지도 f (x :: xs) = f x :: 지도 f xs 테일 리커버티브를 통한 보다 효율적인 구현List.foldl:
재밌어요 지도 f = 목록..리비전 o 목록..접다 (fn (x, 액세스) => f x :: 액세스) [] 예외
예외는 키워드와 함께 발생합니다.raise패턴 매칭으로 처리됩니다.handle건설하다.예외 시스템은 비 로컬 종료를 구현할 수 있습니다. 이 최적화 기술은 다음과 같은 기능에 적합합니다.
현지의 예외. 영; 값 p = fn (0, _) => 올리다 영 (a, b) => a * b 에 재밌어요 자극하다 xs = 목록..접다 p 1 xs 다루다 영 => 0 끝. 언제exception Zero상승하면 제어가 기능을 종료합니다.List.foldl다같이.대신 값 0이 반환되고 목록의 다음 정수가 곱되며 결과 값(불가피하게 0)이 반환되는 등의 방법을 생각해 보십시오.예외가 발생하면 제어가 프레임 체인 전체를 건너뛰고 관련 계산을 피할 수 있습니다.밑줄 사용법에 주의해 주세요._)를 와일드카드 패턴으로 사용합니다.
테일 콜에서도 같은 최적화를 얻을 수 있습니다.
현지의 재밌어요 p a (0 :: _) = 0 p a (x :: xs) = p (a * x) xs p a [] = a 에 값 자극하다 = p 1 끝. 모듈 시스템
표준 ML의 고급 모듈 시스템은 프로그램을 논리적으로 관련된 유형 및 값 정의의 계층 구조로 분해할 수 있습니다.모듈은 네임스페이스 제어뿐만 아니라 추상 데이터 유형을 정의할 수 있다는 점에서 추상화도 제공합니다.모듈 시스템에는 시그니처, 구조 및 펑터의 3가지 주요 구문 구조가 있습니다.
시그니처
시그니처는 보통 구조체의 유형으로 간주되는 인터페이스입니다.구조에 의해 제공되는 모든 엔티티의 이름, 각 유형 컴포넌트의 특성, 각 값 컴포넌트의 유형 및 각 하위 구조의 시그니처를 지정합니다.유형 구성 요소의 정의는 선택 사항입니다. 정의가 숨겨져 있는 유형 구성 요소는 추상 유형입니다.
예를 들어 큐의 시그니처는 다음과 같습니다.
서명 큐잉 = 시그니처 유형 'a' 큐잉 예외. 큐에러; 값 빈 : 'a' 큐잉 값 비어 있다 : 'a' 큐잉 -> 부울 값 싱글톤 : 'a' -> 'a' 큐잉 값 리스트에서 : 'a' 목록. -> 'a' 큐잉 값 삽입하다 : 'a' * 'a' 큐잉 -> 'a' 큐잉 값 훔쳐보다 : 'a' 큐잉 -> 'a' 값 제거한다. : 'a' 큐잉 -> 'a' * 'a' 큐잉 끝. 이 시그니처는 폴리모픽 타입을 제공하는 모듈을 나타냅니다.'a queue,exception QueueError및 큐의 기본 동작을 정의하는 값.
구조물들
구조는 모듈로, 유형, 예외, 값 및 구조(서브구조라고 함)의 집합으로 구성되어 논리 유닛으로 통합됩니다.
큐 구조는 다음과 같이 구현할 수 있습니다.
구조. Two List Queue(투 리스트 큐) :> 큐잉 = 구조 유형 'a' 큐잉 = 'a' 목록. * 'a' 목록. 예외. 큐에러; 값 빈 = ([], []) 재밌어요 비어 있다 ([], []) = 진실의 비어 있다 _ = 거짓의 재밌어요 싱글톤 a = ([], [a]) 재밌어요 리스트에서 a = ([], a) 재밌어요 삽입하다 (a, ([], [])) = 싱글톤 a 삽입하다 (a, (인스톨, 아웃)) = (a :: 인스톨, 아웃) 재밌어요 훔쳐보다 (_, []) = 올리다 큐에러 훔쳐보다 (인스톨, 아웃) = 목록..HD 아웃 재밌어요 제거한다. (_, []) = 올리다 큐에러 제거한다. (인스톨, [a]) = (a, ([], 목록..리비전 인스톨)) 제거한다. (인스톨, a :: 아웃) = (a, (인스톨, 아웃)) 끝. 이 정의는 다음과 같이 선언합니다.structure TwoListQueue용구signature QUEUE또, 다음에 나타내는 불투명한 기술.:>는 시그니처에 정의되어 있지 않은 타입(즉,type 'a queue)는 추상적이어야 합니다.즉, 목록 쌍으로서의 큐의 정의는 모듈 외부에서는 표시되지 않습니다.구조체는 시그니처의 모든 정의를 구현합니다.
구조체의 유형과 값은 "도트 표기법"을 사용하여 액세스할 수 있습니다.
값 q : 스트링 Two List Queue(투 리스트 큐).큐잉 = Two List Queue(투 리스트 큐).빈 값 q' = Two List Queue(투 리스트 큐).삽입하다 (진짜.문자열 수학.파이, q) 기능자
펑터는 구조에서 구조로의 함수입니다.즉, 펑터는 하나 이상의 인수를 받아들입니다.이것은 보통 주어진 시그니처의 구조이며, 그 결과로서 구조를 생성합니다.펑터는 범용 데이터 구조 및 알고리즘을 구현하기 위해 사용됩니다.
트리의[5] 너비 우선 검색을 위해 널리 사용되는 알고리즘 중 하나는 큐를 사용합니다.여기서는 추상 큐 구조에 대해 파라미터화된 알고리즘의 버전을 나타냅니다.
(*오카사키 이후, ICFP, 2000*) 기능자 BFS (Q: 큐잉) = 구조 데이터형 'a' 트리 = E T 의 'a' * 'a' 트리 * 'a' 트리 현지의 재밌어요 bfsQ q = 한다면 Q.비어 있다 q 그리고나서 [] 또 다른 서치 (Q.제거한다. q) 그리고. 서치 (E, q) = bfsQ q 서치 (T (x, l, r), q) = x :: bfsQ (삽입하다 (삽입하다 q l) r) 그리고. 삽입하다 q a = Q.삽입하다 (a, q) 에 재밌어요 bfs t = bfsQ (Q.싱글톤 t) 끝. 끝. 구조. 큐BFS = BFS (Two List Queue(투 리스트 큐)) 이내에functor BFS큐의 표시는 표시되지 않습니다.구체적으로는 2개의 리스트큐의 첫 번째 리스트가 실제로 사용되고 있는 경우 선택할 방법이 없습니다.이 데이터 추상화 메커니즘은 폭 우선 검색을 큐의 구현과 완전히 무관하게 만듭니다.이것은 일반적으로 바람직합니다.이 경우 큐 구조는 추상화의 방탄벽 뒤에 있는 정확성에 따라 달라지는 논리 불변량을 안전하게 유지할 수 있습니다.
코드 예시
 | 이 섹션은 어떠한 출처도 인용하지 않습니다.(2013년 6월 (이 및 ) |
SML 코드의 스니펫은, 인터랙티브한 톱 레벨에 입력하는 것으로, 가장 간단하게 학습할 수 있습니다.
안녕 세계
| hello.sml |
|---|
인쇄물 안녕, 세상아!\n" |
| 때리다 |
$ mlton hello.sml $./안녕하세요, 세상아! |
알고리즘
삽입 정렬
삽입 정렬int list(7)은 다음과 같이 간결하게 표현할 수 있다.
재밌어요 삽입하다 (x, []) = [x] 삽입하다 (x, h :: t) = 종류 x (h, t) 그리고. 종류 x (h, t) = 한다면 x < > h 그리고나서 [x, h] @ t 또 다른 h :: 삽입하다 (x, t) 값 삽입소트 = 목록..접다 삽입하다 [] 머지소트
여기서 기존의 머지소트 알고리즘은 스플릿, 머지 및 머지소트의 3가지 기능으로 구현됩니다.또한 구문을 제외하고 유형이 없습니다.op ::그리고.[]목록을 나타냅니다.이 코드는 일관된 주문 기능이 있는 한 모든 유형의 목록을 정렬합니다.cmp정의되어 있습니다.힌들리-밀러 유형 추론을 사용하여 모든 변수의 유형을 추론할 수 있으며, 함수의 유형과 같은 복잡한 유형도 추론할 수 있다.cmp.
분열되다
fun split를 번갈아 가며 스테이트풀 클로징으로 구현한다.true그리고.false, 입력을 무시합니다.
재밌어요 교류 발전기 {} = 허락하다 값 주 = 레퍼런스 진실의 에 fn a => !스테이트 전에 주 := 것은 아니다. (!스테이트) 끝. (*목록을 같은 길이의 거의 절반으로 분할합니다. * 그렇지 않으면 첫 번째 요소가 다른 요소보다 하나 더 많아집니다. * O(n) 시간 내에 실행됩니다. 여기서 n = xs. *) 재밌어요 분열되다 xs = 목록..칸막이 (교류 발전기 {}) xs 머지
Marge는 효율을 위해 로컬 기능 루프를 사용합니다.내부loop는, 양쪽의 리스트가 공백이 아닌 경우에 정의됩니다.x :: xs1개의 리스트가 비어 있는 경우([]).
이 함수는 정렬된 두 목록을 하나의 정렬된 목록으로 병합합니다.어큐뮬레이터가 어떻게acc거꾸로 빌드된 후 반환되기 전에 반전됩니다.이것은 일반적인 기술입니다.'a list는 링크 리스트로 표시됩니다.이 테크놀로지에서는 더 많은 클럭타임이 필요하지만 점근점수가 더 나쁘지는 않습니다.
(* 순서 cmp를 사용하여 2개의 순서 리스트를 Marge합니다). * 사전: 각 목록은 이미 cmp별로 주문되어 있어야 합니다. * O(n) 시간 내에 실행됩니다(n = xs + ys). *) 재밌어요 합병하다 cmp (xs, []) = xs 합병하다 cmp (xs, y :: ys) = 허락하다 재밌어요 고리 (a, 액세스) (xs, []) = 목록..재첨부여 (a :: 액세스, xs) 고리 (a, 액세스) (xs, y :: ys) = 한다면 cmp (a, y) 그리고나서 고리 (y, a :: 액세스) (ys, xs) 또 다른 고리 (a, y :: 액세스) (xs, ys) 에 고리 (y, []) (ys, xs) 끝. 머지소트
주요 기능:
재밌어요 ap f (x, y) = (f x, f y) (* 지정된 주문 조작 cmp에 따라 목록을 정렬합니다). * O(n log n) 시간 내에 실행됩니다. 여기서 n = xs. *) 재밌어요 머지소트 cmp [] = [] 머지소트 cmp [x] = [x] 머지소트 cmp xs = (합병하다 cmp o ap (머지소트 cmp) o 분열되다) xs 퀵소트
QuickSort는 다음과 같이 표현할 수 있습니다. fun part주문 연산자를 소비하는 폐쇄입니다.op <<.
혼재하다 << > 재밌어요 퀵소트 (동작 << >) = 허락하다 재밌어요 일부 p = 목록..칸막이 (fn x => x << > p) 재밌어요 종류 [] = [] 종류 (p :: xs) = 합류하다 p (일부 p xs) 그리고. 합류하다 p (l, r) = 종류 l @ p :: 종류 r 에 종류 끝. 표현식 인터프리터
작은 표현 언어를 정의 및 처리할 수 있는 비교적 쉬운 점에 유의하십시오.
예외. 타이에러; 데이터형 ty = 인티 불티 재밌어요 통합하다 (인티, 인티) = 인티 통합하다 (불티, 불티) = 불티 통합하다 (_, _) = 올리다 타이에러 데이터형 exp = 진실의 거짓의 내부 의 인트 것은 아니다. 의 exp 더하다 의 exp * exp 한다면 의 exp * exp * exp 재밌어요 추론하다 진실의 = 불티 추론하다 거짓의 = 불티 추론하다 (내부 _) = 인티 추론하다 (것은 아니다. e) = (주장하다 e 불티; 불티) 추론하다 (더하다 (a, b)) = (주장하다 a 인티; 주장하다 b 인티; 인티) 추론하다 (한다면 (e, t, f)) = (주장하다 e 불티; 통합하다 (추론하다 t, 추론하다 f)) 그리고. 주장하다 e t = 통합하다 (추론하다 e, t) 재밌어요 평가하다 진실의 = 진실의 평가하다 거짓의 = 거짓의 평가하다 (내부 n) = 내부 n 평가하다 (것은 아니다. e) = 한다면 평가하다 e = 진실의 그리고나서 거짓의 또 다른 진실의 평가하다 (더하다 (a, b)) = (사례. (평가하다 a, 평가하다 b) 의 (내부 x, 내부 y) => 내부 (x + y)) 평가하다 (한다면 (e, t, f)) = 평가하다 (한다면 평가하다 e = 진실의 그리고나서 t 또 다른 f) 재밌어요 달려. e = (추론하다 e; 몇개 (평가하다 e)) 다루다 타이에러 => 없음. well-type 표현과 well-type 표현에서의 사용 예:
값 몇개 (내부 3) = 달려. (더하다 (내부 1, 내부 2)) (*정확하게 *) 값 없음. = 달려. (한다면 (것은 아니다. (내부 1), 진실의, 거짓의)) (* 부적절한 대응*) 임의 정밀도 정수
그IntInfmodule은 임의의 정수 연산을 제공합니다.게다가 정수 리터럴은 프로그래머가 아무것도 하지 않아도 임의의 정밀도의 정수로 사용할 수 있다.
다음 프로그램은 임의 정밀도 요인 함수를 구현합니다.
| fact.sml |
|---|
재밌어요 사실 n : IntInf.인트 = 한다면 n = 0 그리고나서 1 또 다른 n * 사실 (n - 1); 재밌어요 프린트 라인 스트레이트 = 허락하다 에 텍스트IO.산출량 (텍스트IO.출력, 스트레이트); 텍스트IO.산출량 (텍스트IO.출력, "\n") 끝.; 값 () = 프린트 라인 (IntInf.문자열 (사실 120)); |
| 때리다 |
$mlton fact.sml $./fact 6689502913449127051805403786753802982971352301 6335572449636687416527849813081576378914055408115205405205956605956605659605959605959000 |
부분적용
큐레이티드 함수는 중복 코드 제거와 같은 매우 많은 응용 프로그램을 가지고 있습니다.예를 들어, 모듈에는 유형의 기능이 필요할 수 있습니다.a -> b, 그러나 타입의 함수를 쓰는 것이 더 편리하다.a * c -> b활자의 물체 사이에 고정된 관계가 있는 곳a그리고.c. 타입의 함수c -> (a * c -> b) -> a -> b이 공통점을 배제할 수 있습니다.어댑터 [citation needed]패턴의 예를 다음에 나타냅니다.
이 예에서는,fun d주어진 함수의 도함수를 계산하다f요점에서x:
- 재밌어요 d 델타 f x = (f (x + 델타) - f (x - 델타)) / (2.0 * 델타) 값 d = fn : 진짜 -> (진짜 -> 진짜) -> 진짜 -> 진짜 의 종류fun d타입을 가지는 함수에 「스위치」를 매핑하는 것을 나타냅니다.(real -> real) -> real -> real이를 통해 카레링이라고 하는 주장을 부분적으로 적용할 수 있습니다.이 경우 기능d인수에 부분적으로 적용함으로써 전문화할 수 있다delta에 적합한 선택delta이 알고리즘을 사용할 경우 기계 엡실론의 [citation needed]세제곱근입니다.
- 값 d' = d 1E~8; 값 d' = fn : (진짜 -> 진짜) -> 진짜 -> 진짜 유추된 유형은 다음을 나타냅니다.d'유형을 가진 함수를 기대하다real -> real그 첫 번째 논쟁으로x 에서 f( ) 3 - - ({ f)=의 도함수에 대한 근사치를 계산할 수 있습니다.정답은 f ( ) {\ f' (3) = - 1 =} 입니다.
도함수에 대한 근사치를 계산할 수 있습니다.정답은 f 
- d' (fn x => x * x * x - x - 1.0) 3.0; 값 그것 = 25.9999996644 : 진짜 라이브러리
표준.
기본[6] 라이브러리는 표준화되어 있으며 대부분의 구현이 포함되어 있습니다.트리, 어레이 및 기타 데이터 구조용 모듈뿐만 아니라 입출력 및 시스템 인터페이스용 모듈도 제공합니다.
서드파티
수치 컴퓨팅의 경우 매트릭스 모듈(단, 현재 파손되어 있음)이 있습니다.https://www.cs.cmu.edu/afs/cs/project/pscico/pscico/src/matrix/README.html
그래픽스의 경우 카이로-sml은 카이로 그래픽 라이브러리에 대한 오픈소스 인터페이스입니다.기계 학습의 경우 그래픽 모델을 위한 라이브러리가 존재합니다.
실장
표준 ML의 실장은 다음과 같습니다.
표준.
- HaMLet: 표준 ML 인터프리터.표준의 정확하고 접근하기 쉬운 참조 구현을 목표로 합니다.
- MLton(mlton.org): 정의에 엄밀하게 준거하여 LLVM 및 C용 백엔드 등 다른 ML 구현과 비교하여 매우 빠른 코드를 생성하는 전체
- Moscow ML: 모듈 및 많은 기본 라이브러리를 포함한 완전한 표준 ML 언어를 구현하는 CAML Light 런타임 엔진을 기반으로 한 경량 구현
- Poly/ML: 고속 코드를 생성하고 (Posix 스레드를 통해) 멀티코어 하드웨어를 지원하는 Standard ML의 완전한 구현. 런타임 시스템은 병렬 가비지 수집과 불변의 하위 구조의 온라인 공유를 수행합니다.
- 뉴저지 표준 ML(smlnj.org): 관련된 라이브러리, 도구, 인터랙티브 셸 및 Concurrent ML을 지원하는 문서를 포함한 풀 컴파일러
- SML.NET: 다른 언어와의 링크용 확장 기능을 가진 공통 언어 런타임용 표준 ML 컴파일러입니다.NET 코드
- Wayback Machine에서 아카이브된 ML 키트 2016-01-07: 정의에 매우 밀접하게 기반한 구현으로, 가비지 콜렉터(비활성화 가능)와 지역 기반 메모리 관리를 통합하여 실시간 애플리케이션 지원을 목표로 합니다.
파생상품
- Alice: Saarland University의 Standard ML 인터프리터.미래를 사용한 병렬 프로그래밍, 느린 평가, 원격 프로시저 호출 및 제약 프로그래밍을 통한 분산 컴퓨팅을 지원합니다.
- SML 번호: 레코드 다형성과 C 언어 상호 운용성을 제공하는 SML의 확장입니다.이것은 기존의 네이티브컴파일러이며, 그 이름은 위에서 동작하는 것을 암시하는 것이 아닙니다.NET 프레임워크
- SOSML: TypeScript로 작성된 구현으로 대부분의 SML 언어와 일부 기본 라이브러리를 지원합니다.
조사.
- CakeML은 정식 검증된 런타임과 어셈블러로의 변환을 포함한 ML의 리플리케이션 버전입니다.
- Isabelle(Isabelle/ML)은 parallel Poly/ML을 대화형 정리 프로버에 통합하고 공식 Standard ML(SML'97), Isabel/ML 방언 및 증명 언어를 위한 정교한 IDE(jEdit 기반)를 제공합니다.Isabelle2016부터는 ML용 소스 레벨 디버거도 있습니다.
- Poplog는 Common Lisp 및 Prolog와 함께 표준 ML 버전을 구현하여 혼합 언어 프로그래밍을 가능하게 합니다.모두 POP-11로 구현되어 증분 컴파일 됩니다.
- TILT는 입력된 중간 언어를 사용하여 코드를 최적화하고 정확성을 보증하는 Standard ML용 완전 인증 컴파일러입니다.또, 입력된 어셈블리 언어로 컴파일 할 수 있습니다.
이러한 구현은 모두 오픈 소스이며 자유롭게 사용할 수 있습니다.대부분은 Standard ML에 실장되어 있습니다.현재 상용 실장은 없습니다.할리킨은 한때 MLWorks라는 상용 IDE와 컴파일러를 생산해 Xanalys에 넘겼으며, 2013년 4월 26일 Ravenbrook Limited에 인수된 후 오픈소싱되었습니다.
SML을 이용한 주요 프로젝트
코펜하겐 IT대학의 전체 엔터프라이즈 아키텍처는 직원 기록, 급여, 코스 관리 및 피드백, 학생 프로젝트 관리, 웹 기반 셀프 서비스 [7]인터페이스 등 약 100,000개의 SML 라인에서 구현됩니다.
Proof Assistant HOL4, Isabelle, LEGO, Twelf는 Standard ML로 작성되어 있으며 컴파일러 라이터 및 [8]ARM 등의 집적회로 설계자가 사용하고 있습니다.
「 」를 참조해 주세요.
레퍼런스
- ^ a b "Programming in Standard ML: Hierarchies and Parameterization". Retrieved 2020-02-22.
- ^ a b c "SML '97". www.smlnj.org.
- ^ a b "itertools — Functions creating iterators for efficient looping — Python 3.7.1rc1 documentation". docs.python.org.
- ^ a b Robin Milner; Mads Tofte; Robert Harper; David MacQueen (1997). The Definition of Standard ML (Revised). MIT Press. ISBN 0-262-63181-4.
- ^ a b Chris Okasaki (2000). "Breadth-First Numbering: Lessons from a Small Exercise in Algorithm Design". International Conference on Functional Programming 2000. ACM.
- ^ "Standard ML Basis Library". smlfamily.github.io. Retrieved 2022-01-10.
- ^ a b Mads Tofte (2009). "Standard ML language". Scholarpedia. 4 (2): 7515. Bibcode:2009SchpJ...4.7515T. doi:10.4249/scholarpedia.7515. Retrieved 2020-01-08.
- ^ a b Jade Alglave; Anthony C. J. Fox; Samin Ishtiaq; Magnus O. Myreen; Susmit Sarkar; Peter Sewell; Francesco Zappa Nardelli. The Semantics of Power and ARM Multiprocessor Machine Code (PDF). DAMP 2009. pp. 13–24.
외부 링크
표준 ML에 대해서
후계 ML에 대해서
실용적인.
학업의
리스트: 
