런타임에 이것이 사실이라는 것을 알고 있다면 GHC에게 유형 수준 <= 제약 조건을 충족하도록 어떻게 알릴 수 있습니까?

Aug 17 2020

자연수로 매개 변수화 된 유형이 있습니다 n.

data MyType (n :: Nat) = MyType

이 유형에 대한 작업은 인 경우에만 의미가 n > 0있으므로 제약 조건으로 지정했습니다.

myFunction :: (KnownNat n, 1 <= n) => MyType n -> MyType n
myFunction = id

(주이 기능의 실제 버전은 어떻게 사용할 수 n있는 값으로 돌려 natVal.)

런타임에 SomeMyType선택할 수 있는 존재 유형 ( ) 을 만들고 싶습니다 n.

data SomeMyType where
  SomeMyType :: forall n. (KnownNat n, 1 <= n) => MyType n -> SomeMyType

의 값을 생성하기 위해 다음 과 같이 작동 SomeMyType하는 someMyTypeVal함수를 작성하고 있습니다 someNatVal.

someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n
  | n > 0 = case someNatVal n of
      Just (SomeNat (_ :: p n)) -> Just (SomeMyType (MyType @n))
      Nothing                   -> Nothing
  | otherwise = Nothing

이것은 1 <= n제약 조건 없이는 완벽하게 작동 하지만 제약 조건으로 인해 다음과 같은 유형 오류가 발생합니다.

• Couldn't match type ‘1 <=? n’ with ‘'True’
    arising from a use of ‘SomeMyType’

이 제한을 어떻게 피할 수 있습니까? 나는 것을 확인했습니다 때문에 n > 0런타임에, 나는 같은 작업을 사용하여 상관 없어 unsafeCoerce그 GHC를 설득하기 위해 여기에 1 <= n있는 경우에 true-하지만 난 수 없습니다 그냥 사용 unsafeCoerce그 유형 수준의 가치를 상실하기 때문 n.

이를 처리하는 가장 좋은 방법은 무엇입니까?

답변

6 TikhonJelvis Aug 17 2020 at 05:21

조금 더 둘러 본 후 비슷한 질문에 대한 Justin L의 답변을 찾았습니다 . 그는 typelits-witnesses이 문제를 아주 깔끔하게 해결하는 데 사용할 수 있는 패키지에 자신의 솔루션을 포장했습니다 .

someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n = someNatVal n >>= check
  where check :: SomeNat -> Maybe SomeMyType
        check (SomeNat (_ :: p n)) = case (SNat @1) %<=? (SNat @n) of
          LE Refl -> Just (SomeMyType (MyType @n))
          NLE _ _ -> Nothing

a %<=? b두 가지 유형 수준의 자연수를 비교하고 a보다 작은 지 b( LE) 아닌지 ( )에 대한 증거를 제공합니다 NLE. 이것은 우리에게 LE를 반환하는 경우에 추가적인 제약을 SomeMyType주지만, 이 경우에 그렇게하려고하면 NLE여전히 "ca n't match '1 <=? n'with ''True '"오류가 발생합니다.

에 대한 명시 적 유형 서명 참고 check그것을 수리공 없이도을,의 유형 check으로 추정되고 check :: SomeNat -> Maybe a나는 다음과 같은 유형의 오류가 발생합니다 :

• Couldn't match type ‘a’ with ‘SomeMyType’
   ‘a’ is untouchable
     inside the constraints: 'True ~ (1 <=? n)

명시 적 유형 서명을 사용하면 모든 것이 작동하고 코드는 (합리적으로) 읽을 수 있습니다.

1 K.A.Buhr Aug 19 2020 at 05:24

보다 직접적인 대답으로 제약 조건 1 <= n1 <=? n ~ 'True. 다음을 사용하여 이러한 유형 같음 제약 조건을 안전하지 않게 만들 수 있습니다.

{-# LANGUAGE DataKinds, TypeOperators #-}

import Data.Type.Equality
import GHC.TypeLits
import Unsafe.Coerce

unsafeDeclarePositive :: p n -> (1 <=? n) :~: 'True
unsafeDeclarePositive _ = unsafeCoerce Refl

이것은 typelits-witnesses후드 아래에서하는 일입니다.

해당 정의를 사용하면 다음이 유형을 확인해야합니다.

someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n
  | n > 0 = case someNatVal n of
      Just (SomeNat (pxy :: p n)) ->
        case unsafeDeclarePositive pxy of
          Refl -> Just (SomeMyType (MyType @n))
      Nothing -> Nothing
  | otherwise = Nothing