[haskell] `coerce`에 의한 역할과 혼란스러운 행동

Program / 글쓴이

나는 유형을 가지고 있으며 Id a실수로 강요되는 것을 막으려 고 Id Double합니다 Id Int.

유형 역할을 올바르게 이해하면 다음을 컴파일해서는 안됩니다.

{-# LANGUAGE RoleAnnotations #-}
import Data.Coerce (coerce)

type role Id nominal
newtype Id a = Id String

badKey :: Id Int
badKey = coerce (Id "I point to a Double" :: Id Double)

불행히도, 그것은 :

Prelude> :load Id.hs
[1 of 1] Compiling Main             ( Id.hs, interpreted )
Ok, one module loaded.
*Main> :type badKey
badKey :: Id Int

유형 역할에서 무엇을 놓치고 있습니까?

답변

Coercible인스턴스의 세 가지 가능한 “유형”(사용자가 정의하지 않은 컴파일러에 의해 자동 생성됨)이 있습니다. 이들 중 하나만 실제로 역할의 영향을받습니다 .

  • 모든 유형은 스스로 강제적입니다.
  • 영향을받는 유형 변수가 representational또는 이면 유형 생성자를 “아래로”강제 변환 할 수 있습니다 phantom. 예를 들어, Map Char Inta Map Char (Data.Monoid.Sum Int)때문에를 a 로 강제 변환 할 수 Map있습니다 type role Map nominal representational.
  • newtype 생성자가 범위 내에있는 경우 항상 기본 형식으로 새 형식을 강제 변환 할 수 있습니다 . 이것은 모든 역할을 무시합니다! 이론적 근거는 생성자가 사용 가능한 경우 항상 수동으로 랩핑 및 랩핑 해제 할 수 있으므로 역할이 안전을 제공하지 않는다는 것입니다.

귀하의 예에서 세 번째 규칙이 적용됩니다. newtype이 다른 모듈에 정의되어 있고 생성자를 가져 오지 않은 경우 강제 변환이 실패했습니다 (다시 작동하게하려면 역할을로 전환해야 함 phantom).

이 GHC 문제 에는 새로운 유형에 대한 다소 놀라운 특수 동작이 설명되어 있습니다.

답변