Idris의 한정어 및 복합 부울 제안을

Question

종속 유형에 익숙하지 않고 하스켈 환경에서 천천히 Idris를 배우고 있습니다. 운동을 위해 허프만 인코딩을 작성하려고합니다. 현재 코드 트리의 "병합 (flattening)"이 접두어 코드를 생성하지만 한정 기호에 얽매이지는 않았다는 증거를 작성하려고합니다.

using (xs : List a, ys : List a) 
    data Prefix : List a -> List a -> Type where 
     pEmpty : Prefix Nil ys 
     pNext : (x : a) -> Prefix xs ys -> Prefix (x :: xs) (x :: ys) 

1. 이 유효한 방법입니다 :

   나는 하나 개의 목록은 다른 접두사임을 간단한 유도 제안이? 또는 같은 것보다 "XS가있는 경우 YS의 접두사 ZS 같은 XS ++ ZS = YS가있다"?

2. "forall"한정 기호를 소개하는 올바른 방법 이었습니까? (내가 이해할 수있는 한 Agda에서는 pNext : ∀ {x xs ys} → Prefix xs ys → Prefix (x :: xs) (y :: ys)과 같을 것입니다)? pNext 첫 번째 인수가 암시 적이어야합니까? 두 변종 사이의 의미 차이는 무엇입니까?

   pvEmpty : PrefVect Nil 
   

   과 주어진 :

   data PrefVect : Vect n (List a) -> Type where 
   

   빈 벡터에는 접두사가 없습니다 : 요소 중 어느 것도 또 다른 접두사가없는 경우

그런 다음 나는 벡터를 구축하고자 요소 x, 벡터 xs, 그리고 xs의 아무 요소도 x의 접두어가 아니며 (그 반대의 경우도) x : xs는 해당 속성을 보유합니다.

pvNext : (x : [a]) -> (xs : Vect n [a]) -> 
       All (\y => Not (Prefix x y)) xs -> 
       All (\y => Not (Prefix y x)) xs -> 
       PrefVect (x :: xs) 

이것은 첫 번째 문제를 해결 한 후에 해결할 수있는 유효하지 않은 유형이지만 pvNext의 한정 기호에 대해 비슷한 질문이 있습니다.이 변형이 허용 가능하거나 "관계에 부정"을 형성하는 더 좋은 방법이 있습니다. ?

감사합니다.

Answer 1

여기서 유일한 문제는 a의 목록 유형으로 [a]을 사용했으며, 이스트리스에서는 List a 일 필요가있는 반면 하스켈 스타일에서는 생각한다고 생각합니다. 이다

data Prefix : List a -> List a -> Type where 
    pEmpty : Prefix [] ys 
    pNext : Prefix xs ys -> Prefix (x :: xs) (x :: ys) 

, x 암시 될 수 있으며, 이드리스가의 유형을 추론 할 수 있기 때문에 당신이 using 필요하지 않습니다 :

귀하의 Prefix 유형으로 내가 써서 있지만, 나에게 잘 보이는 xs 및 ys. 이것이 올바른 접근 방식인지 여부는 실제로 Prefix 유형을 사용하려는 계획에 달려 있습니다. 목록이 다른 목록의 접두어인지 여부를 테스트하기에 충분합니다. 뭔가 같이 :

testPrefix : DecEq a => (xs : List a) -> (ys : List a) -> Maybe (Prefix xs ys) 
testPrefix [] ys = Just pEmpty 
testPrefix (x :: xs) [] = Nothing 
testPrefix (x :: xs) (y :: ys) with (decEq x y) 
    testPrefix (x :: xs) (x :: ys) | (Yes Refl) = Just (pNext !(testPrefix xs ys 
    testPrefix (x :: xs) (y :: ys) | (No contra) = Nothing 

당신은 당신이 수도 보인다 부정을 증명하려는 경우, 당신은 할 유형을해야합니다 :

testPrefix : DecEq a => (xs : List a) -> (ys : List a) -> Dec (Prefix xs ys) 

내가 운동으로 하나를 떠날 것이다 :).