¿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?

Aug 17 2020

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 nal convertirlo en un valor con natVal.)

Quiero crear un tipo existencial ( SomeMyType) que nos permita elegir un nen 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 someMyTypeValfunció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 <= nrestricció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 > 0en tiempo de ejecución, no me importa usar una operación como unsafeCoercepara convencer a GHC que 1 <= nes cierto, pero no puedo simplemente usar unsafeCoerceporque eso sería perder el valor de nivel de tipo de n.

¿Cuál es la mejor forma de lidiar con esto?

Respuestas

6 TikhonJelvis Aug 17 2020 at 05:21

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 %<=? bnos permite comparar dos números naturales a nivel de tipo y nos da un testimonio de si aes menor que b( LE) o no ( NLE). Esto nos da la restricción adicional en el LEcaso de devolver a SomeMyType, pero intentar hacer eso en el NLEcaso todavía nos daría el error "no puede coincidir '1 <=? N' con '' Verdadero '".

Tenga en cuenta la firma de tipo explícita para; checksin ella, el tipo de checkse infiere como check :: SomeNat -> Maybe ay 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.

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

Como respuesta más directa, la restricción 1 <= nes 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-witnessesse 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