Çalışma zamanında doğru olduğunu biliyorsam, GHC'ye bir tür düzeyinde <= kısıtlamasını karşılamasını nasıl söyleyebilirim?

Aug 17 2020

Doğal sayı ile parametrelendirilmiş bir türe sahibim n:

data MyType (n :: Nat) = MyType

Bu türdeki işlemler yalnızca ne zaman anlamlıdır n > 0, bu yüzden bunu bir kısıtlama olarak belirttim:

myFunction :: (KnownNat n, 1 <= n) => MyType n -> MyType n
myFunction = id

(Not bu fonksiyonların gerçek versiyonları olduğunu yapmak kullanımını niçeren bir değere dönüştürerek natVal.)

Çalışma zamanında SomeMyTypebir seçmemize izin veren varoluşsal bir tür ( ) oluşturmak istiyorum n:

data SomeMyType where
  SomeMyType :: forall n. (KnownNat n, 1 <= n) => MyType n -> SomeMyType

Değerlerini üretmek için şu şekilde çalışan SomeMyTypebir someMyTypeValişlev yazıyorum 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

Bu, 1 <= nkısıtlama olmadan mükemmel bir şekilde çalışır , ancak kısıtlamayla aşağıdaki tür hatasını alıyorum:

• Couldn't match type ‘1 <=? n’ with ‘'True’
    arising from a use of ‘SomeMyType’

Bu sınırlamayı nasıl aşabilirim? Bunu kontrol ettim yana n > 0zamanında, ben gibi bir işlemi kullanarak sakıncası olmaz unsafeCoerceo ghc ikna burada 1 <= nolduğunu gerçek ama olamaz sadece kullanmak unsafeCoerceolduğunu türü düzeyinde değerini kaybeder çünkü n.

Bununla başa çıkmanın en iyi yolu nedir?

Yanıtlar

6 TikhonJelvis Aug 17 2020 at 05:21

Biraz daha kafa yorduktan sonra benzer bir soruya Justin L'nin cevabını buldum . Çözümünü, typelits-witnessesbu sorunu oldukça temiz bir şekilde çözmek için kullanabildiğim pakete sardı :

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 %<=? biki tür düzeyinde doğal sayıyı karşılaştırmamıza izin verir ve bize ( ) ' aden küçük olup olmadığına b( LE) tanıklık eder NLE. Bu bize, LEdurumda a döndürmek için fazladan kısıtlama sağlar SomeMyType, ancak bu NLEdurumda bunu yapmaya çalışmak bize yine de "'1 <=? N' ile '' True '" hatasını eşleştiremez.

Açık tip imzasına dikkat edin check—bu olmadan, türü checkolarak çıkarılır check :: SomeNat -> Maybe ave aşağıdaki tür hatasını alırım:

• Couldn't match type ‘a’ with ‘SomeMyType’
   ‘a’ is untouchable
     inside the constraints: 'True ~ (1 <=? n)

Açık tip imzasıyla her şey çalışır ve kod bile (makul bir şekilde) okunabilir.

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

Daha doğrudan bir cevap olarak, kısıtlama 1 <= nsadece için bir tür takma adıdır 1 <=? n ~ 'True. Aşağıdakilerle güvenli olmayan bir şekilde böyle bir tür eşitliği kısıtlaması oluşturabilirsiniz:

{-# LANGUAGE DataKinds, TypeOperators #-}

import Data.Type.Equality
import GHC.TypeLits
import Unsafe.Coerce

unsafeDeclarePositive :: p n -> (1 <=? n) :~: 'True
unsafeDeclarePositive _ = unsafeCoerce Refl

typelits-witnesseskaputun altında ne yapıyor az ya da çok .

Bu tanım yerinde olduğunda, aşağıdakiler tip kontrolü yapmalıdır:

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