Ç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?
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ı n
içeren bir değere dönüştürerek natVal
.)
Çalışma zamanında SomeMyType
bir 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 SomeMyType
bir someMyTypeVal
iş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 <= n
kı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 > 0
zamanında, ben gibi bir işlemi kullanarak sakıncası olmaz unsafeCoerce
o ghc ikna burada 1 <= n
olduğunu gerçek ama olamaz sadece kullanmak unsafeCoerce
olduğunu türü düzeyinde değerini kaybeder çünkü n
.
Bununla başa çıkmanın en iyi yolu nedir?
Yanıtlar
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 %<=? b
iki tür düzeyinde doğal sayıyı karşılaştırmamıza izin verir ve bize ( ) ' a
den küçük olup olmadığına b
( LE
) tanıklık eder NLE
. Bu bize, LE
durumda a döndürmek için fazladan kısıtlama sağlar SomeMyType
, ancak bu NLE
durumda 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ü check
olarak çıkarılır check :: SomeNat -> Maybe a
ve 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.
Daha doğrudan bir cevap olarak, kısıtlama 1 <= n
sadece 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-witnesses
kaputun 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