'singleton'패키지에 Ord 인스턴스 추가하기 Naturals 생성

Question

싱글 톤 패키지로 생성 된 매우 간단한 유형 수준의 자연어를 사용하고 있습니다. Ord 인스턴스를 추가하려고합니다.

{-# LANGUAGE MultiParamTypeClasses, TemplateHaskell, KindSignatures, DataKinds, ScopedTypeVariables, GADTs, TypeFamilies, FlexibleInstances, TypeOperators, UndecidableInstances, InstanceSigs #-} 

module Functions where 

import Data.Singletons 
import Data.Singletons.TH 
import Data.Singletons.Prelude 
import Data.Promotion.Prelude 

singletons [d| 
      data Nat = Z | S Nat 
       deriving Eq 

      instance Ord Nat where 
       (<=) Z  _ = True 
       (<=) (S _) Z = False 
       (<=) (S n) (S m) = n <= m 
      |] 

다른 오류가 발생했습니다. 최신 버전은 다음과 같습니다.

src/Functions.hs:10:1: 
    Couldn't match kind ‘Nat’ with ‘*’ 
    When matching types 
     n0 :: Nat 
     t1 :: * 
    Expected type: Sing t1 
     Actual type: Sing n0 
    Relevant bindings include 
     n_a9na :: Sing n0 (bound at src/Functions.hs:10:1) 
     lambda :: Sing n0 -> Sing m0 -> Sing (Apply (Apply (:<=$) t00) t10) 
     (bound at src/Functions.hs:10:1) 
    In the second argument of ‘applySing’, namely ‘n_a9na’ 
    In the first argument of ‘applySing’, namely 
     ‘applySing (singFun2 (Proxy :: Proxy (:<=$)) (%:<=)) n_a9na’ 

src/Functions.hs:10:1: 
    Could not deduce (SOrd 'KProxy) arising from a use of ‘%:<=’ 
    from the context (t00 ~ 'S n) 
     bound by a pattern with constructor 
       SS :: forall (z_a9mg :: Nat) (n_a9mh :: Nat). 
         (z_a9mg ~ 'S n_a9mh) => 
         Sing n_a9mh -> Sing z_a9mg, 
       in an equation for ‘%:<=’ 
     at src/Functions.hs:(10,1)-(18,15) 
    or from (t10 ~ 'S n1) 
     bound by a pattern with constructor 
       SS :: forall (z_a9mg :: Nat) (n_a9mh :: Nat). 
         (z_a9mg ~ 'S n_a9mh) => 
         Sing n_a9mh -> Sing z_a9mg, 
       in an equation for ‘%:<=’ 
     at src/Functions.hs:(10,1)-(18,15) 
    or from (t00 ~ Apply SSym0 n0, t10 ~ Apply SSym0 m0) 
     bound by the type signature for 
       lambda_a9n9 :: (t00 ~ Apply SSym0 n0, t10 ~ Apply SSym0 m0) => 
           Sing n0 -> Sing m0 -> Sing (Apply (Apply (:<=$) t00) t10) 
     at src/Functions.hs:(10,1)-(18,15) 
    In the second argument of ‘singFun2’, namely ‘(%:<=)’ 
    In the first argument of ‘applySing’, namely 
     ‘singFun2 (Proxy :: Proxy (:<=$)) (%:<=)’ 
    In the first argument of ‘applySing’, namely 
     ‘applySing (singFun2 (Proxy :: Proxy (:<=$)) (%:<=)) n_a9na’ 

누구나 올바른 방법은 무엇입니까?

Answer 1

왜 이것이 실패하는지 잘 모르겠습니다. 나는 동일 (단순 해 보이는)을 시도 할 때 대신 compare을 구현, 더욱 의아해 내가 얻을 실패로 때 얻을 비슷한 실패

singletons [d| data Nat = Z | S Nat deriving (Eq,Ord) |] 

내 생각은 Ord에 뭔가가 꺼져 있다는 것이다 의해 의아해하고 ... 그러나 이것은 효과적이다. 나중에 singleton의 배짱이를 살펴 보려고합니다.

그런데 저는 여기 GHC 8.0을 사용하고 있습니다.

편집

singletons에서 주변에 파고 후, 나는 문제의 실제 원인을 발견했습니다 (그리고 많은 유형 수준의 해커가 가능한 방법으로 날아되었다). GHC에서 -ddump-splices을 사용하여 생성 된 실제 Haskell 코드를 얻을 수있었습니다 (질문에 대한 초기 코드 용). 문제가되는 부분은, 내가 PEq에 (Proxy :: Proxy Nat_a7Vb)에 관한 이러한

Expecting one more argument to ‘Proxy’ 
Expected kind ‘Proxy Nat_a7Vb’, but ‘Proxy’ has kind ‘k0 -> *’ 

의 모두에 대해 약간 더 유용한 오류 메시지를받은 코드가 생성 컴파일

instance PEq (Proxy :: Proxy Nat_a7Vb) where 
    type (:==) (a_a8Rs :: Nat_a7Vb) (b_a8Rt :: Nat_a7Vb) = Equals_1627424016_a8Rr a_a8Rs b_a8Rt 

및

instance POrd (Proxy :: Proxy Nat_a7Vb) where 
    type (:<=) (a_aa9e :: Nat_a7Vb) (a_aa9f :: Nat_a7Vb) = Apply (Apply TFHelper_1627428966Sym0 a_aa9e) a_aa9f 

했다 및 POrd 클래스. 그것은 -XPolyKinds 없이는 컴파일되지 않습니다. 리볼로 singletons을 확인했으며 실제로 -XTypeInType을 사용하도록 설정 했으므로 -XPolyKinds을 사용할 수 있음을 알립니다.

그래서, 당신은 (즉, 패키지가 ... 권장 무엇 때문에 나는 후자를 추천) 일을 모든 것을 얻을 수 있도록 LANGUAGE 프라 그마에 하나 PolyKinds 또는 TypeInType 추가해야, 어떤 버그가 없다.

Answer 2

해제 된 부울 관계로 작업 isnevercomfortable. 불법 행위자는 학습에 관심이있는 정보를 지우고 테스트 결과에 아무 것도하지 않으려 고 할 때 당신을 떠들썩하게 만듭니다. 그냥 안된다고, 애들.

더 좋은 방법이 있습니다. "n가 m에보다 적게 또는 동등하다"는 풍부한 정보 증거으로 입증 될 수 제안이다.

이

data LE n m where 
    LE :: Natty z -> LE n (n :+ z) 

우리는 주어진 숫자가 다른 것보다 작은 지 여부를 테스트하기위한 절차를 가지고 올 수 : 하나 개의 번호가 다른 것보다 작다는 것을 증명하는 한 가지 방법은 자신의 차이 (의 싱글 표현)을 제공하는 것입니다. le은 을 m에서 뺍니다. 실패하면 Nothing을 반환하거나 그 차이는 Natty이며 LE 생성자에 뺄셈이 올바른지 증명할 수 있습니다.

le :: Natty n -> Natty m -> Maybe (LE n m) 
le Zy m = Just (LE m) 
le (Sy n) (Sy m) = fmap (\(LE z) -> LE z) (le n m) 
le _ _ = Nothing 

이 아이디어는 우리에게 "강력한 형식의 compare"을 부여하기 위해 일반화 할 수 있습니다. 두 숫자를 비교할 때, 당신은 그들이 동등하다는 것을 알게되거나, 하나가 다른 것보다 적음을 알게 될 것입니다. (Either (LE n m) (LE m n)도 일을하지만,이 버전은 약간 더 정확하다.)

data Compare n m where 
    LT :: Natty z -> Compare n (n :+ S z) 
    EQ :: Compare n n 
    GT :: Natty z -> Compare (m :+ S z) m 

compare :: Natty n -> Natty m -> Compare n m 
compare Zy Zy = EQ 
compare Zy (Sy m) = LT m 
compare (Sy n) Zy = GT n 
compare (Sy n) (Sy m) = case compare n m of 
    LT z -> LT z 
    EQ -> EQ 
    GT z -> GT z 

(나는 Hasochism에서 이것을 해제.) le 달리, compare 총이다,

참고. 항상은 모든 숫자가 다른 모든 숫자보다 작거나 같거나 큰 결과를 제공합니다. 우리의 목표는 두 개의 숫자 중 더 작은 숫자를 테스트하는 절차를 작성하는 것이었지만 숫자가 totally ordered임을 증명하고 유형 안전 차감 루틴을 작성하는 것이 모두 동일한 함수에 있음을 발견했습니다.

compare을 보는 다른 방법은 보기의 자연수 쌍입니다. 두 숫자를 비교할 때, 어느 것이 더 적은지, 얼마나 많이, 그 숫자 자체에 대한 지식을 정제 하는지를 배웁니다. 내가 직접 singletons 버그의 소스에 말할 수없는, 어쨌든

compare : (n m : Nat) -> Compare n m 
compare zero zero = eq 
compare zero (suc m) = lt m 
compare (suc n) zero = gt n 
compare (suc n)   (suc m)   with compare n m 
         -- see how matching on `lt` refines `m` to `n + suc z` 
compare (suc n)   (suc .(n + suc z)) | lt z = lt z 
compare (suc m)   (suc .m)   | eq = eq 
    -- likewise matching on `gt` refines `n` to `m + suc z` 
compare (suc .(m + suc z)) (suc m)   | gt z = gt z 

---

,하지만 하나의 이유 Ord을위한 작업하기 좀 어렵습니다 : AGDA의 도트 패턴이 세련미의이 개념에 대한 좋은 지원을 두 개의 싱글을 비교 할 때

class Ord a where 
    compare :: a -> a -> Ordering 

, 그들은 일반적으로 동일한 유형이되지 않습니다 싱글 값은 같은 유형의 값을 비교하는 가정이다! 이것이 싱글 톤의 전체적인 특징입니다. 유형이 직접적으로 그 가치를 반영합니다. 두 개의 Natty n 값 (그 중 n과 일치 함)이있는 경우 비교하는 데 별다른 차이가 없습니다. 평등하지 않다면 비교할 수 없습니다!

단순 유형의 세계에서 설계된 Ord과 같은 클래스가 반드시 종속 형식의 프로그램에서 유용하지는 않습니다. 종속 형을 사용하는 경우 올바른 방법은 이전 도구를 악용하지 않는 것입니다. 오픈 무기로 안전하고 정보가 풍부한 프로그래밍의 새로운 세계를 선도하십시오!