Como posso dizer ao GHC para satisfazer uma restrição de nível de tipo <= se eu sei que é verdade em tempo de execução?
Eu tenho um tipo parametrizado por um número natural n
:
data MyType (n :: Nat) = MyType
As operações neste tipo só fazem sentido quando n > 0
, portanto, especifiquei isso como uma restrição:
myFunction :: (KnownNat n, 1 <= n) => MyType n -> MyType n
myFunction = id
(Observe que as versões reais dessas funções são usadas n
, transformando-as em um valor com natVal
.)
Eu quero criar um tipo existencial ( SomeMyType
) que nos permite escolher um n
em tempo de execução:
data SomeMyType where
SomeMyType :: forall n. (KnownNat n, 1 <= n) => MyType n -> SomeMyType
Para produzir valores de SomeMyType
, estou escrevendo uma someMyTypeVal
função que funciona como 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
Isso funcionaria perfeitamente sem a 1 <= n
restrição, mas com a restrição, recebo o seguinte erro de tipo:
• Couldn't match type ‘1 <=? n’ with ‘'True’
arising from a use of ‘SomeMyType’
Como posso contornar essa limitação? Como verifiquei isso n > 0
em tempo de execução, não me importaria de usar uma operação como unsafeCoerce
esta para convencer o GHC de que 1 <= n
é verdade - mas não posso simplesmente usar unsafeCoerce
porque isso perderia o valor de nível de tipo de n
.
Qual é a melhor maneira de lidar com isso?
Respostas
Depois de bisbilhotar um pouco mais, encontrei a resposta de Justin L para uma pergunta semelhante . Ele embrulhou sua solução no typelits-witnessespacote que pude usar para resolver este problema de forma bastante limpa:
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
permite-nos comparar dois números naturais de nível de tipo e nos dá uma testemunha se a
é menor que b
( LE
) ou não ( NLE
). Isso nos dá a restrição extra no LE
caso de retornar a SomeMyType
, mas tentar fazer isso no NLE
caso ainda nos daria o erro "não é possível combinar '1 <=? N' com '' Verdadeiro '".
Observe a assinatura de tipo explícita para check
- sem ela, o tipo de check
é inferido como check :: SomeNat -> Maybe a
e eu obteria o seguinte erro de tipo:
• Couldn't match type ‘a’ with ‘SomeMyType’
‘a’ is untouchable
inside the constraints: 'True ~ (1 <=? n)
Com a assinatura de tipo explícita, tudo funciona e o código é (razoavelmente) legível.
Como uma resposta mais direta, a restrição 1 <= n
é apenas um alias de tipo para 1 <=? n ~ 'True
. Você pode criar de forma insegura essa restrição de igualdade de tipo com:
{-# LANGUAGE DataKinds, TypeOperators #-}
import Data.Type.Equality
import GHC.TypeLits
import Unsafe.Coerce
unsafeDeclarePositive :: p n -> (1 <=? n) :~: 'True
unsafeDeclarePositive _ = unsafeCoerce Refl
que é mais ou menos o que typelits-witnesses
está acontecendo nos bastidores.
Com essa definição em vigor, o seguinte deve verificar o tipo:
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