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 n
en le transformant en une valeur avec natVal
.)
Je veux créer un type existentiel ( SomeMyType
) qui nous permet de choisir un n
au 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 someMyTypeVal
fonction 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 <= n
contrainte, 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 > 0
au moment de l'exécution, cela ne me dérangerait pas d'utiliser une opération comme celle- unsafeCoerce
ci pour convaincre GHC que 1 <= n
c'est vrai - mais je ne peux pas simplement l' utiliser unsafeCoerce
car 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 %<=? b
nous permet de comparer deux nombres naturels au niveau du type et nous donne un témoin pour savoir si a
est inférieur à b
( LE
) ou non ( NLE
). Cela nous donne la contrainte supplémentaire dans le LE
cas de renvoyer a SomeMyType
, mais essayer de le faire dans le NLE
cas nous donnerait toujours l'erreur «ne peut pas correspondre à '1 <=? N' avec '' Vrai ''».
Notez la signature de type explicite pour - check
sans elle, le type de check
est déduit comme check :: SomeNat -> Maybe a
et 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 <= n
est 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-witnesses
se 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