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?

Aug 17 2020

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

6 TikhonJelvis Aug 17 2020 at 05:21

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.

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

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