सिंगलनेट लाइब्रेरी

Question

के संबंध में ज्ञात नाट को दो अस्तित्व में नहीं हटा सका मैं अकेले सिंगल लाइब्रेरी के साथ प्रयोग कर रहा था और मुझे एक ऐसा मामला मिला जो मुझे समझ में नहीं आया।

{-# LANGUAGE GADTs, StandaloneDeriving, RankNTypes, ScopedTypeVariables, 
FlexibleInstances, KindSignatures, DataKinds, StandaloneDeriving #-} 

import Data.Singletons.Prelude 
import Data.Singletons.TypeLits 

data Foo (a :: Nat) where 
Foo :: Foo a 
    deriving Show 

data Thing where 
    Thing :: KnownNat a => Foo a -> Thing 

deriving instance Show Thing 

afoo1 :: Foo 1 
afoo1 = Foo 

afoo2 :: Foo 2 
afoo2 = Foo 

athing :: Thing 
athing = Thing afoo1 

foolen :: forall n. KnownNat n => Foo n -> Integer 
foolen foo = 
    case sing of (SNat :: Sing n) -> natVal (Proxy :: Proxy n) 


minfoo :: forall a b c. (Min a b ~ c, KnownNat c) => Foo a -> Foo b -> Integer 
minfoo _ _ = 
    let c = case sing of (SNat :: Sing c) -> natVal (Proxy :: Proxy c) 
    in natVal (Proxy :: Proxy c) 

thinglen :: Thing -> Integer 
thinglen (Thing foo) = foolen foo 

मैं इस दो चीजें

minthing :: Thing -> Thing -> Integer 
minthing (Thing foo1) (Thing foo2) = min (foolen foo1) (foolen foo2) 

की न्यूनतम प्राप्त करने के लिए इस्तेमाल कर सकते हैं लेकिन मैं सिर्फ यह नहीं कर सकता?

minthing' :: Thing -> Thing -> Integer 
minthing' (Thing foo1) (Thing foo2) = minfoo foo1 foo2 

• Could not deduce (KnownNat 
         (Data.Singletons.Prelude.Ord.Case_1627967386 
         a 
         a1 
         (Data.Singletons.Prelude.Ord.Case_1627967254 
          a a1 (GHC.TypeLits.CmpNat a a1)))) 

Answer 1

आप कुछ प्रमेय जो दिया KnownNat a जाँच करने के लिए और KnownNat b आप KnownNat (Min a b) प्राप्त कर सकते हैं साबित करने की जरूरत है। सम्भावित समाधान:

import Data.Constraint 

(...)

theorem :: forall a b. (KnownNat a, KnownNat b) => 
      Sing a -> Sing b -> Dict (KnownNat (Min a b)) 
theorem sa sb = case sCompare sa sb of 
    SLT -> Dict 
    SEQ -> Dict 
    SGT -> Dict 

fooSing :: forall a. KnownNat a => Foo a -> Sing a 
fooSing _ = sing 

minthing' :: Thing -> Thing -> Integer 
minthing' (Thing foo1) (Thing foo2) = 
    case theorem (fooSing foo1) (fooSing foo2) of 
    Dict -> minfoo foo1 foo2 

Answer 2

मुझे लगता है user3237465 की टिप्पणी की तरह अमर होने के लिए, क्योंकि यह contraint पुस्तकालय निर्भरता को हटा की जरूरत है और यह बहुत साफ है।

minthing' :: Thing -> Thing -> Integer 
minthing' (Thing foo1) (Thing foo2) = 
    theorem (fooSing foo1) (fooSing foo2) $ minfoo foo1 foo2 
    where 
    fooSing :: KnownNat a => Foo a -> Sing a 
    fooSing = const sing 

theorem :: forall a b c. (KnownNat a, KnownNat b) => 
      Sing a -> Sing b -> (KnownNat (Min a b) => c) -> c 
theorem sa sb c = case sCompare sa sb of 
    SLT -> c 
    SEQ -> c 
    SGT -> c