런타임에 이것이 사실이라는 것을 알고 있다면 GHC에게 유형 수준 <= 제약 조건을 충족하도록 어떻게 알릴 수 있습니까?
자연수로 매개 변수화 된 유형이 있습니다 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
.
이를 처리하는 가장 좋은 방법은 무엇입니까?
답변
조금 더 둘러 본 후 비슷한 질문에 대한 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 <= n
은 1 <=? 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