यदि मुझे पता है कि जीएचसी एक प्रकार के स्तर को संतुष्ट करने के लिए कैसे कह सकता है तो मैं इसे रनटाइम पर सच मान सकता हूं?
मेरे पास एक प्राकृतिक संख्या द्वारा एक प्रकार का पैराट्राइक है n
:
data MyType (n :: Nat) = MyType
इस प्रकार के ऑपरेशन केवल तभी समझ में आते हैं n > 0
, जब मैंने निर्दिष्ट किया कि बाधा के रूप में:
myFunction :: (KnownNat n, 1 <= n) => MyType n -> MyType n
myFunction = id
(ध्यान दें कि इन कार्यों के वास्तविक संस्करण इसे मूल्य में बदलकर उपयोग करते हैं ।)n
natVal
मैं एक अस्तित्वगत प्रकार ( SomeMyType
) बनाना चाहता हूं जो हमें एक n
रनटाइम चुनने की अनुमति देता है:
data SomeMyType where
SomeMyType :: forall n. (KnownNat n, 1 <= n) => MyType n -> SomeMyType
के मूल्यों का उत्पादन करने के लिए SomeMyType
, मैं एक someMyTypeVal
फ़ंक्शन लिख रहा हूं जो इस तरह काम करता है 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
यह 1 <= n
बाधा के बिना पूरी तरह से ठीक काम करेगा , लेकिन बाधा के साथ मुझे निम्न प्रकार की त्रुटि मिलती है:
• Couldn't match type ‘1 <=? n’ with ‘'True’
arising from a use of ‘SomeMyType’
मैं इस सीमा के आसपास कैसे पहुंच सकता हूं? जब से मैं देख लिया है कि n > 0
रनटाइम पर, मैं की तरह एक ऑपरेशन का उपयोग कर कोई फ़र्क नहीं पड़ेगा unsafeCoerce
GHC समझा दिया है कि यहाँ 1 <= n
है सच है, लेकिन मैं नहीं कर सकता बस का उपयोग unsafeCoerce
क्योंकि उस के प्रकार के स्तर के मूल्य खो देगा n
।
इससे निपटने का सबसे अच्छा तरीका क्या है?
जवाब
थोड़ा और आसपास घूमने के बाद, मैंने जस्टिन एल को इसी तरह के सवाल का जवाब दिया । उन्होंने अपने समाधान को उस typelits-witnessesपैकेज में लपेट दिया जिसे मैं इस समस्या को बहुत सफाई से हल करने में सक्षम था:
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
हमें दो प्रकार-स्तरीय प्राकृतिक संख्याओं की तुलना करने की अनुमति देता है और हमें इस बात का गवाह देता है कि क्या a
इससे कम b
( LE
) या नहीं ( NLE
) है। यह हमें LE
मामले में अतिरिक्त बाधा देता है SomeMyType
, लेकिन वापस लौटने की कोशिश करता है , लेकिन NLE
मामले में अभी भी हमें "1 <=? N" का मिलान '' सही '' त्रुटि से नहीं कर सकता है।
इसके लिए स्पष्ट प्रकार के हस्ताक्षर पर ध्यान दें check
- इसके साथ, इस प्रकार का check
अनुमान लगाया गया है check :: SomeNat -> Maybe a
और मुझे निम्न प्रकार की त्रुटि मिलेगी:
• Couldn't match type ‘a’ with ‘SomeMyType’
‘a’ is untouchable
inside the constraints: 'True ~ (1 <=? n)
स्पष्ट प्रकार के हस्ताक्षर के साथ सब कुछ काम करता है और कोड भी (यथोचित) पठनीय है।
अधिक प्रत्यक्ष उत्तर के रूप में, बाधा 1 <= n
केवल एक प्रकार का उपनाम है 1 <=? n ~ 'True
। आप इस तरह की समानता समानता को अनसुना कर सकते हैं:
{-# LANGUAGE DataKinds, TypeOperators #-}
import Data.Type.Equality
import GHC.TypeLits
import Unsafe.Coerce
unsafeDeclarePositive :: p n -> (1 <=? n) :~: 'True
unsafeDeclarePositive _ = unsafeCoerce Refl
typelits-witnesses
हुड के नीचे क्या कर रहा है कम या ज्यादा ।
उस परिभाषा के साथ, निम्नलिखित को टाइप-चेक करना चाहिए:
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