OCaml 펑터 :: 반 직관적 인 행동

Question

OCaml (3.12.1)의 모듈 언어를 실험 중이며, 모듈에 대한 펑터와 서명을 정의하고 있습니다. 대부분 Chapter 2 of the OCaml manual의 예제를 따르면 우연히 발견하게됩니다. , 펑터와 모듈 서명이 어떻게 작동하는지에 대한 나의 정신 모델이 결함이있는 상황에서. 나는 가능한 한 가장 짧은 양의 코드로 인해 발생하는 상황을 좁히려고 노력했다. 그래서 내가 성취하려는 것을 묻지 않는다. 이것은 OCaml 기능을 시연하는 완전히 모범적 인 예이다.

그래서 우리는 단순히 신원 함수 'f'를 제공하고 해당 함수의 입력 매개 변수의 유형을 제공하는 모듈에 의해 매개 변수화 된 기능을 제공합니다. 내가 말한 것처럼 완전히 고안된 예. ..

module IntType = struct type t = int end ;; 

그리고, 우리는 INT 식별 기능 모듈을 생성하기 위해 펑를 사용 :

module type SOMETYPE = sig type t end ;; 
module Identity = functor (Type: SOMETYPE) -> struct let f (x: Type.t) = x end ;; 

, 우리는 정수형 공급 모듈을 정의하는 상기 진행 감안할

module IdentityInt = Identity(IntType) ;;      

물론 예상대로 충분히 생성 모듈과 F 기능 깊으

#IdentityInt.f(3) + 10 ;; 
- : int = 13 

모듈을 입력 모듈로 사용하는 함수 인 펑터의 정신 모델은 지금까지 우리에게 도움이되고있는 것 같습니다. Identity functor는 시그니처 (모듈 유형) SOMETYPE의 모듈을 입력 매개 변수로 기대하며 실제로 제공된 모듈 (IntType)은 올바른 서명을 가지므로 f 함수가 예상대로 작동하는 유효한 출력 모듈 (IdentityInt)이 생성됩니다.

이제 직관적이지 않은 부분이 있습니다. 제공된 모듈 IntType이 참으로 SOMETYPE 유형의 모듈이라는 것을 명시하고 싶다면 어떻게해야할까요? 마찬가지로 ...

module IdentityInt = Identity(IntType) ;; 

의 새로 생성 된 모듈의 f 기능을 사용하려고하자 :

module IntType : SOMETYPE = struct type t = int end ;; 

다음은 펑터의 출력 모듈 이전과 같은 방법으로 생성

IdentityInt.f 0 ;; 

을

REPL이 다음과 같이 불평합니다 :

"Error: This expression [the value 0] has type int but an expression was expected of type IntType.t." 

어떻게 중복되지만 정확한 유형 정보를 제공하면 코드가 손상 될 수 있습니까? 경우에 있어서도 functor 모듈 Identity는 IntType 모듈을 SOMETYPE 유형으로 처리해야했습니다. 그렇다면 IntType을 SOMETYPE 유형으로 명시 적으로 선언하면 다른 결과가 나타납니다.

Answer 1

: 구조는 핵심 언어와 모듈 언어가 다릅니다. 핵심 언어에서는 주석 구조입니다. 예를 들어 ((3, x) : 'a * 'a list)은 표현식이 'a * 'a list의 인스턴스 인 일부 유형을 갖도록 제한합니다. 쌍의 첫 x 째 요소는 정수이 G로 let (a, b) = ((3, x) : 'a * 'a list) in a + 1은 올 Y로 유형이 지정됩니다. 모듈의 : 구조가이 것을 의미하지는 않습니다.

구조체 M : S밀봉 서명 S하도록 모듈 M. 이것은 불투명 한 인장입니다. M : S의 사용을 입력 할 때 S 기호에 주어진 정보 만 사용할 수 있습니다. 당신이 module IntType : SOMETYPE = struct type t end을 쓸 때,이 IntType은 추상 형식 필드 t을 가지고 SOMETYPE에서 t가 지정되지 않은 남아 유형 필드 이후

module IntType = (struct type t end : SOMETYPE) 

에 대한 대체 구문입니다 유형 IntType이 정의에 의해 생성 된 새로운 유형입니다.

그건 그렇고, 아마도 module IntType = (struct type t = int end : SOMETYPE)을 의미합니다. 하지만 어느 쪽이든, IntType.t은 추상 유형입니다.

모듈에 특정 서명이있는 상태로 지정하고 특정 형식을 공개하도록 지정하려면 이러한 형식에 대해 명시적인 동일성을 추가해야합니다. 모든 추측 할 수있는 동등성을 추가하는 구조는 없습니다. 왜냐하면 모듈에 서명을 적용하는 것은 정보 숨기기를위한 것이기 때문입니다. 단순함을 위해 언어는이 생성적인 씰링 구조를 제공합니다.당신이 정의 된 서명 SOMETYPE를 사용하고 유형 t의 투명도를 유지하려면, 서명에 제약 조건을 추가

module IntType = (struct type t = int end : SOMETYPE with type t = int) 

Answer 2

당신이 명시 적으로 뭔가를 작성하지 않는 추론 서명을 보면 :

# module IntType = struct type t = int end ;; 
module IntType : sig type t = int end 

서명이 t가 int 것을 제공합니다.귀하의 서명은, 반대로 :

# module IntType : SOMETYPE = struct type t = int end ;; 
module IntType : SOMETYPE 

은 정말 :

# module IntType : sig type t end = struct type t = int end ;; 
module IntType : sig type t end 

이 문제 해결하는 것 같다

# module IntType : (SOMETYPE with type t = int) = struct type t = int end ;; 
module IntType : sig type t = int end 
# module IdentityInt = Identity(IntType) ;; 
module IdentityInt : sig val f : IntType.t -> IntType.t end 
# IdentityInt.f 0 ;; 
- : IntType.t = 0 

(당신은 괄호가 필요하지 않습니다,하지만 그들은 도움 정신 분석). 기본적으로, 당신은 t가 당신의 서명과 함께 int임을 공개합니다. 그래서 OCaml은 평등을 알고 있습니다. IntType.t = int.

내부에 대한 자세한 내용은 더 잘 알고있는 사람들에게 맡깁니다.

Answer 3

당신은 쓸 때 : 당신은 정확히 SOMETYPE로 InType의 서명을 제약하는

module IntType : SOMETYPE = struct type t = int end ;; 

. 예를 들어, t 유형이 이제 추상 유형 (구현이 타이 퍼에 알려지지 않음)이되고 있음을 의미합니다.

so IdentityInt.f 유형은 여전히 ​​IntType.t -> IntType.t이지만 서명 제한 조건을 사용하여 방정식 지식에서 방정식 IntType.t = int을 명시 적으로 제거했습니다. 오류 메시지는 정확하게 알려줍니다.

Answer 4

키 오류가 여기에 있었다 :

모듈 IntType : SOMETYPE = 구조체 유형 t 끝 ;; 당신이 서명 SOMETYPE을 돌리는 경우

, 그것은 불투명 한 탓으로, 그리고 int와 신원가 손실됩니다. 형식 IntType.t은 이제 추상 형식입니다.

대신에 SOMETYPE with type t = int의 서명을 사용해야합니다. 모듈 및 귀속 주위

# module type SOMETYPE = sig type t end;; 
module type SOMETYPE = sig type t end 
# module IntType : SOMETYPE with type t = int = struct type t = int end;; 
module IntType : sig type t = int end 
# module AbsType : SOMETYPE = struct type t = int end;;     
module AbsType : SOMETYPE 

언어 설계 문제도 다룹니다 수석 디자이너의 1994 paper on modules, types, and separate compilation :

이 성적 차이를 보여줍니다. 털이 많은 수학 부분은 모두 건너 뛸 수 있습니다.