यदि मुझे पता है कि जीएचसी एक प्रकार के स्तर को संतुष्ट करने के लिए कैसे कह सकता है तो मैं इसे रनटाइम पर सच मान सकता हूं?

Aug 17 2020

मेरे पास एक प्राकृतिक संख्या द्वारा एक प्रकार का पैराट्राइक है n:

data MyType (n :: Nat) = MyType

इस प्रकार के ऑपरेशन केवल तभी समझ में आते हैं n > 0, जब मैंने निर्दिष्ट किया कि बाधा के रूप में:

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

(ध्यान दें कि इन कार्यों के वास्तविक संस्करण इसे मूल्य में बदलकर उपयोग करते हैं ।)nnatVal

मैं एक अस्तित्वगत प्रकार ( 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रनटाइम पर, मैं की तरह एक ऑपरेशन का उपयोग कर कोई फ़र्क नहीं पड़ेगा unsafeCoerceGHC समझा दिया है कि यहाँ 1 <= nहै सच है, लेकिन मैं नहीं कर सकता बस का उपयोग unsafeCoerceक्योंकि उस के प्रकार के स्तर के मूल्य खो देगा n

इससे निपटने का सबसे अच्छा तरीका क्या है?

जवाब

6 TikhonJelvis Aug 17 2020 at 05:21

थोड़ा और आसपास घूमने के बाद, मैंने जस्टिन एल को इसी तरह के सवाल का जवाब दिया । उन्होंने अपने समाधान को उस 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 K.A.Buhr Aug 19 2020 at 05:24

अधिक प्रत्यक्ष उत्तर के रूप में, बाधा 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