계약/제약을 기반으로 한 유형 시스템에 대한 좋은 정보?

Question

문제:

나는 좋은 소개를 찾고 있습니다 유형 시스템, 이는 기반입니다 계약/제약
(죄송합니다. 유형 시스템에 적합한 용어가 기억 나지 않습니다).

그러한 종류의 실험 유형 시스템을 구현할 수있는 정보가 필요합니다.

내가 아는 한, 그러한 유형 시스템은 XSD (XML 스키마 정의).

데이터 유형을 정의하는 대신 가능한 값 세트의 제약 조건을 정의합니다.

예시:

매개 변수로 일부 메소드를 정의합니다. "nothing", 또는 적분 범위와 일치합니다 [0..100].

이러한 방법은 다음 값을 수락합니다.

"nothing"
0
1
...
100

나는 내 자신을 분명하게 만들 수 있기를 바랍니다.

Answer 1

일반적인 LISP는 이러한 유형 테스트를 제공합니다 런타임. 정교한 유형 시스템이 있지만 정적으로 유형 된 언어로 익숙 할 수 있으므로 사용되지 않습니다. 매크로 check-type 수락 a typespec, 내장 사양이거나 매크로에 의해 정의 된 사양 일 수 있습니다. deftype. typespecs로 표현할 수있는 제약 조건은 호스트 언어로 작성된 술어 기능의 제약 조건입니다. 즉, 실행 시간을 검사 할 수있는 것은 새로운 유형을 구성하는 것에 대한 기준이 될 수 있습니다.

이 예를 고려하십시오 :

(defun is-nothing (val)
  (when (stringp val)
    (string= val "nothing")))

(deftype strange-range ()
  "A number between 0 and 100 inclusive, or the string \"nothing\"."
  '(or (integer 0 100)
       (satisfies is-nothing)))

"이상한 범위"라는 유형을 정의합니다. 이제 몇 가지 값을 테스트하십시오.

CL-USER> (let ((n 0))
           (check-type n strange-range))
NIL
CL-USER> (let ((n 100))
           (check-type n strange-range))
NIL
CL-USER> (let ((n "nothing"))
           (check-type n strange-range))
NIL
CL-USER> (let ((n 101))
           (check-type n strange-range))

마지막은 다음 메시지로 디버거를 트리거합니다.

The value of N should be of type STRANGE-RANGE.
The value is: 101
   [Condition of type SIMPLE-TYPE-ERROR]

이것은 동일한 결과를 유발합니다.

CL-USER> (let ((n "something"))
           (check-type n strange-range))

이런 식으로 부과 할 수있는 제약은 표현력이 있지만 Haskell이나 Scala와 같은 정교한 유형의 언어 시스템이하는 것과 동일한 목적을 제공하지 않습니다. 유형의 정의는 공통 LISP 컴파일러를 동축하여 피연산자의 유형에 더 맞고 효율적인 코드를 방출 할 수 있지만 위의 예는 런타임 유형 검사를 작성하는 간결한 방법입니다.

Answer 2

당신은 같은 언어를 볼 수 있습니다 Haskell, 또는 아고 다. 또한, 올레그 많은 훌륭한 자원이 있습니다.

Answer 3

이것은 내 전문 분야의 영역이 아니므로 주제가 될 수 있지만 Microsoft Research는 프로젝트가 있습니다. 코드 계약, ".NET 프로그램에서 코딩 가정을 표현하는 언어 공유 방법을 제공합니다. 계약은 전제 조건, 사후 조건 및 객체 불변의 형태를 취합니다."