Comment puis-je dire à GHC de satisfaire une contrainte de niveau de type <= si je sais que c'est vrai au moment de l'exécution?
J'ai un type paramétré par un nombre naturel n:
data MyType (n :: Nat) = MyType
Les opérations sur ce type n'ont de sens que lorsque n > 0, j'ai donc spécifié cela comme une contrainte:
myFunction :: (KnownNat n, 1 <= n) => MyType n -> MyType n
myFunction = id
(Notez que les versions réelles de ces fonctions font usage nen le transformant en une valeur avec natVal.)
Je veux créer un type existentiel ( SomeMyType) qui nous permet de choisir un nau moment de l'exécution:
data SomeMyType where
  SomeMyType :: forall n. (KnownNat n, 1 <= n) => MyType n -> SomeMyType
Pour produire des valeurs de SomeMyType, j'écris une someMyTypeValfonction qui fonctionne comme 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
Cela fonctionnerait parfaitement sans la 1 <= ncontrainte, mais avec la contrainte, j'obtiens l'erreur de type suivante:
• Couldn't match type ‘1 <=? n’ with ‘'True’
    arising from a use of ‘SomeMyType’
Comment contourner cette limitation? Depuis que j'ai vérifié cela n > 0au moment de l'exécution, cela ne me dérangerait pas d'utiliser une opération comme celle- unsafeCoerceci pour convaincre GHC que 1 <= nc'est vrai - mais je ne peux pas simplement l' utiliser unsafeCoercecar cela perdrait la valeur de niveau de type n.
Quelle est la meilleure façon de gérer cela?
Réponses
Après avoir fouillé un peu plus, j'ai trouvé la réponse de Justin L à une question similaire . Il a emballé sa solution dans le typelits-witnessespackage que j'ai pu utiliser pour résoudre ce problème assez proprement:
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 %<=? bnous permet de comparer deux nombres naturels au niveau du type et nous donne un témoin pour savoir si aest inférieur à b( LE) ou non ( NLE). Cela nous donne la contrainte supplémentaire dans le LEcas de renvoyer a SomeMyType, mais essayer de le faire dans le NLEcas nous donnerait toujours l'erreur «ne peut pas correspondre à '1 <=? N' avec '' Vrai ''».
Notez la signature de type explicite pour - checksans elle, le type de checkest déduit comme check :: SomeNat -> Maybe aet j'obtiendrais l'erreur de type suivante:
• Couldn't match type ‘a’ with ‘SomeMyType’
   ‘a’ is untouchable
     inside the constraints: 'True ~ (1 <=? n)
Avec la signature de type explicite, tout fonctionne et le code est même (raisonnablement) lisible.
En guise de réponse plus directe, la contrainte 1 <= nest juste un alias de type pour 1 <=? n ~ 'True. Vous pouvez créer de manière non sécurisée une telle contrainte d'égalité de type avec:
{-# LANGUAGE DataKinds, TypeOperators #-}
import Data.Type.Equality
import GHC.TypeLits
import Unsafe.Coerce
unsafeDeclarePositive :: p n -> (1 <=? n) :~: 'True
unsafeDeclarePositive _ = unsafeCoerce Refl
ce qui est plus ou moins ce qui typelits-witnessesse fait sous le capot.
Avec cette définition en place, les éléments suivants devraient vérifier le type:
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