큐빅 호환

큐빅 호환 (Cubical compatible)

--cubical=compatible 옵션은 타입 체크되는 모듈이 Cubical Agda와 호환되는지 여부를 지정해요. 이 플래그가 없는 모듈은 --cubical 모듈에서 임포트할 수 없어요.

참고: Agda 2.6.3 이전에는 --cubical=compatible 플래그가 존재하지 않았고, --without-K가 Cubical Agda 특정 코드의 (내부) 생성을 암시하기도 했어요. 이 변경의 근거는 Agda 이슈 #5843을 참고하세요.

Cubical Agda와의 호환성은 다음으로 구성돼요:

유니벌런트 타입 이론과 호환되지 않는 추론 원리는 사용할 수 없어요. 이 동작은 --cubical=compatible이 암시하는 Without K 플래그(--without-K)에 의해 제어돼요.
Cubical Agda 구현의 특수성 때문에 여러 종류의 Agda 정의는 정교화(elaboration) 과정에서 내부 지원 코드가 생성될 필요가 있어요.
때때로 정교화 버그로 인해 코드가 타입적으로 정확함에도 불구하고 이러한 내부 정의에서 오류가 표면화될 수 있어요. 사용자가 작성한 코드가 Cubical Agda와 독립적일 때 큐빅 정의를 언급하는 오류가 표시되는 것을 피하기 위해, 이 내부 정의들은 현재 --cubical=compatible 뒤로 게이트되어 있어요.

(만) --without-K를 사용하는 코드는 --cubical을 사용하는 코드에서 임포트할 수 없다는 점에 주의하세요. 따라서 라이브러리 개발자들은 가능하면 --without-K 대신 --cubical=compatible을 사용하는 것이 권장돼요.

또한 --cubical=compatible 대신 --without-K를 사용하면 Agda가 꽤 빨라지는 경향이 있다는 점도 주의하세요.

--cubical=compatible 옵션은 감염성(coinfective)이에요 (일관성을 위한 옵션 검사 참고): 함수에 대해 생성된 지원 코드는 임포트하는 모듈의 지원 코드에 의존할 수 있어요.