¿Cómo puedo decirle a GHC que satisfaga una restricción de nivel de tipo <= si sé que es verdadera en tiempo de ejecución?
Tengo un tipo parametrizado por un número natural n
:
data MyType (n :: Nat) = MyType
Las operaciones en este tipo solo tienen sentido cuando n > 0
, así que lo especifiqué como una restricción:
myFunction :: (KnownNat n, 1 <= n) => MyType n -> MyType n
myFunction = id
(Tenga en cuenta que las versiones reales de estas funciones hacen uso n
al convertirlo en un valor con natVal
.)
Quiero crear un tipo existencial ( SomeMyType
) que nos permita elegir un n
en tiempo de ejecución:
data SomeMyType where
SomeMyType :: forall n. (KnownNat n, 1 <= n) => MyType n -> SomeMyType
Para producir valores de SomeMyType
, estoy escribiendo una someMyTypeVal
función que funciona así 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
Esto funcionaría perfectamente sin la 1 <= n
restricción, pero con la restricción obtengo el siguiente error de tipo:
• Couldn't match type ‘1 <=? n’ with ‘'True’
arising from a use of ‘SomeMyType’
¿Cómo puedo sortear esta limitación? Desde He comprobado que n > 0
en tiempo de ejecución, no me importa usar una operación como unsafeCoerce
para convencer a GHC que 1 <= n
es cierto, pero no puedo simplemente usar unsafeCoerce
porque eso sería perder el valor de nivel de tipo de n
.
¿Cuál es la mejor forma de lidiar con esto?
Respuestas
Después de hurgar un poco más, encontré la respuesta de Justin L a una pregunta similar . Envolvió su solución en el typelits-witnessespaquete que pude usar para resolver este problema de manera bastante limpia:
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
nos permite comparar dos números naturales a nivel de tipo y nos da un testimonio de si a
es menor que b
( LE
) o no ( NLE
). Esto nos da la restricción adicional en el LE
caso de devolver a SomeMyType
, pero intentar hacer eso en el NLE
caso todavía nos daría el error "no puede coincidir '1 <=? N' con '' Verdadero '".
Tenga en cuenta la firma de tipo explícita para; check
sin ella, el tipo de check
se infiere como check :: SomeNat -> Maybe a
y obtendría el siguiente error de tipo:
• Couldn't match type ‘a’ with ‘SomeMyType’
‘a’ is untouchable
inside the constraints: 'True ~ (1 <=? n)
Con la firma de tipo explícita, todo funciona y el código es incluso (razonablemente) legible.
Como respuesta más directa, la restricción 1 <= n
es solo un alias de tipo para 1 <=? n ~ 'True
. Puede crear de forma insegura tal restricción de igualdad de tipos con:
{-# LANGUAGE DataKinds, TypeOperators #-}
import Data.Type.Equality
import GHC.TypeLits
import Unsafe.Coerce
unsafeDeclarePositive :: p n -> (1 <=? n) :~: 'True
unsafeDeclarePositive _ = unsafeCoerce Refl
que es más o menos lo que typelits-witnesses
se hace bajo el capó.
Con esa definición en su lugar, se debe verificar lo siguiente:
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