싱글 톤 라이브러리와 관련하여 두 가지 존재 점에서 KnownNat을 추론 할 수 없습니다.

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 (Min a b)를 얻을 수 KnownNat b이 주어진 KnownNat a을 확인하고 증명하는 몇 가지 정리를 할 필요가있다. 가능한 솔루션 :

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