타입 멤버가있는 객체 : 스칼라의 객체 대 모듈 시스템은 무엇입니까? (경로 종속 유형에 대한 2014 년 Odersky 논문을 이해하려고 시도 함)

Question

나는 Foundations of path dependent types을 읽습니다. 첫 번째 페이지에서 오른쪽 열에에이 기록됩니다

Our motivation is twofold. First, we believe objects with type members are not fully understood. It is not clear what causes the complexity, which pieces of complexity are essential to the concept or accidental to a language implementation or calculus that tries to achieve something else. Second, we believe objects with type members are really useful. They can encode a variety of other, usually separate type system features. Most importantly, they unify concepts from object and module systems, by adding a notion of nominality to otherwise structural systems.

사람은 "개체 모듈 대"시스템이 무엇을 의미합니까/명확하게 설명 할 수 있을까요?

또는 일반적으로

,

"they (objects with type members) unify concepts from object and module systems, by adding a notion of nominality to otherwise structural systems."

은 무엇을 의미합니까?

어떤 개념입니까? 어디에서?

개체 이름/값의 Nominality는 무엇입니까? 유형의 구조는 무엇입니까? 아니면 다른 방법으로?

여기서 유형 회원은 어디에 속합니까? 모듈 시스템에? 객체 시스템? 방법? 왜?

편집 :

방법이 통일 경로 의존적 유형과 어떤 관련이 있습니까? 나에게이 통일은 일어날 수 있다고 생각합니다 (타입 멤버가있는 객체). 그래? 예인 경우 어떻게합니까?

간단한 예를 들어 주시겠습니까? (즉 경로 의존적 유형의 모듈과 객체 시스템의 통합을 허용하는 대 우리는 경로 의존적 유형이하지 않는다면 왜 통일이 일어날 수 없을 것?)

편집 2 :

종이에서 :

To make any use of type members, programmers need a way to refer to them. This means that types must be able to refer to objects, i.e. contain terms that serve as static approximation of a set of dynamic objects. In other words, some level of dependent types is required; the usual notion is that of path-dependent types.

그래서 내 이해 지금까지 (예스퍼의 답변의 도움으로) :

는

이상이 단락은 부분적으로 위의 몇 가지 질문에 대한 답변입니다. 주체는 유형 멤버가있는 객체를 갖고 그 객체가 동적/런타임에 의존하지만 유형이 정적 (컴파일 타임에 정의 됨)이기 때문에 유형 종속 멤버로 연결되는 객체가 작동하지 않기 때문에 해당 경로 종속 유형을 필요로하는 것 같습니다. 왜냐하면 그 타입 멤버가 컴파일 타임에 명확하게 정의되지 않기 때문이다.

경로 종속 형은 컴파일 타임에 유형 멤버로 이어지는 경로를 고정시킴으로써 (객체가 컴파일 시간에 이미 알려져 있거나 정의되어 있어야하므로) 경로가 객체를 통해 이동하더라도 컴파일 타임에 해당 객체가 이미 컴파일 타임에 고정되어 있다면 해당 유형 멤버도 컴파일 할 때 명확한 의미를 가질 수 있습니다.

Answer 1

나는 당신의 질문이 무엇인지 완전히 이해하고 있는지 잘 모르겠다. 그러나 나는 그것에 찔러 볼 것이다. :) 저는 저자가 주로 ML style modules을 참조하고 있다고 생각합니다. 여기서 시그너처는 스칼라 형질에 해당하고 구조체는 스칼라 객체에 해당합니다. Scala는 레코드 값, 오브젝트 및 모듈의 개념을 통합합니다. 대부분의 다른 언어 (예 : ML, Rust 등)에서는 개별 개념입니다. 주된 이점은 스칼라 모듈/객체가 일반 함수 인수로 전달 될 수 있다는 것입니다 (ML에서는 특수 펑터를 사용해야 함).

ML에서 모듈은 구조체 (Scala의 구조체 타이핑과 유사)를 기반으로 서명 (Scala의 특성)과의 호환성을 검사하지만 모듈은 이름 (공칭 형식 지정)으로 특성을 구현해야합니다.따라서 두 개의 모듈/객체가 스칼라에서 동일한 구조를 가지고 있더라도 슈퍼 유형 계층 구조에 따라 서로 호환되지 않을 수 있습니다.

스칼라의 유형 멤버와 관련하여 정말 강력한 기능은 형식이 안전한 방식으로 작업하는 한 유형 멤버의 정확한 유형을 모르는 경우에도 특성을 사용할 수 있다는 것입니다. 예를 들어,) ML 모듈에서 가능 :

trait A { 
    type X 
    def getX: X 
    def setX(x: X): Unit 
} 

def foo(a: A) = a.setX(a.getX) 

foo에서 스칼라 컴파일러는 a.X의 정확한 유형 여전히 컴파일러 안전 알고있는 방법으로 사용할 수있는 유형의 값을 알 수 없습니다. 예를 들어 in Rust은 가능하지 않습니다.

Scala 컴파일러의 다음 버전 인 Dotty는 사용자가 참조하는 논문에 설명 된 이론을 기반으로합니다. 서브 타입, 특성 및 타입 멤버와 결합 된 모듈 및 객체의 이러한 통합은 스칼라가 독특하고 매우 강력한 한 가지 이유입니다.

편집 :

error: type mismatch; 
found : b.T 
required: a.T 
    def foo(a: A, b: A) = a.setX(b.getX) 
           ^

: 이것은 컴파일 오류가 발생합니다

def bar(a: A, b: A) = a.setX(b.getX) 

: 경로 의존적 유형 스칼라의 모듈/오브젝트 시스템의 유연성을 증가 이유를 조금 확장하기 위해, 함께 위의 예제를 확장하자

그리고 정확하게 그 이유는 a.T과 b.T이 다른 유형을 해결할 수 있기 때문입니다. 당신은 경로 의존의 형태를 사용하여 문제를 해결할 수 있습니다

def bar(a: A)(b: A { type X = a.X }) = a.setX(b.getX) 

또는 유형 매개 변수를 추가 :

이

def bar[T](a: A { type X = T }, b: A { type X = T }) = a.setX(b.getX) 

따라서, 경로 의존 종류의 형식 매개 변수의 일부 필요성을 제거하고, 또한 우리가 존재 표현할 수 유형이 효율적으로 (A가 유형 구성원 대신 유형 매개 변수를 갖는 경우 A[_] 또는 A[T] forSome { type T }에 해당).