종속 쌍을 사용하는 방법

StackOverflow https://stackoverflow.com//questions/9625951

  •  09-12-2019
  •  | 
  •  

문제

다음과 같은 함수가 있다고 가정해 보겠습니다(실제로 이름에서 알 수 있는 것과 같은 기능을 수행합니다).

filter : ∀ {A n} → (A → Bool) → Vec A n → ∃ (λ m → Vec A m)

이제 반환된 종속 쌍을 사용하여 어떻게든 작업하고 싶습니다.간단하게 썼어요 head 기능:

head :: ∀ {A} → ∃ (λ n → Vec A n) → Maybe A
head (zero   , _ )       = nothing
head (succ _ , (x :: _)) = just x

물론 완벽하게 작동합니다.그러나 그것은 나를 궁금하게 만들었습니다.함수가 다음과 같은 경우에만 호출될 수 있는지 확인할 수 있는 방법이 있나요? n ≥ 1?

이상적으로는 함수를 만들고 싶습니다. head : ∀ {A} → ∃ (λ n → Vec A n) → IsTrue (n ≥ succ zero) → A;하지만 그건 실패하기 때문에 n 내가 사용할 때 범위를 벗어납니다. IsTrue.

시간 내 줘서 고마워!

IsTrue 다음과 같습니다:

data IsTrue : Bool → Set where
  check : IsTrue true
도움이 되었습니까?

해결책

이건 uncurring에 대한 질문인 것 같아요.표준 라이브러리는 언커링을 제공합니다 제품에 대한 기능은 다음을 참조하십시오. 카레를 하지 않는다.귀하의 상황에서는 첫 번째 head 함수는 일반적으로 길이 인덱스를 암시 적 인수로 사용하기 때문에 argument가 숨겨져 있습니다.다음과 같이 uncurry 함수를 작성할 수 있습니다.

uncurryʰ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : (a : A) → B a → Set c} →
           ({x : A} → (y : B x) → C x y) →
           ((p : Σ A B) → uncurry C p)
uncurryʰ f (x , y) = f {x} y

벡터가 있는 경우 벡터의 머리를 반환하는 함수는 표준 라이브러리에 존재하지 않는 것 같습니다. 그래서 우리는 하나를 씁니다.

maybe-head : ∀ {a n} {A : Set a} → Vec A n → Maybe A
maybe-head []       = nothing
maybe-head (x ∷ xs) = just x

이제 원하는 기능은 maybe-head 함수를 첫 번째 인수-암시 적 uncurrying과 함께 위에 정의 된 기능 :

maybe-filter-head : ∀ {A : Set} {n} → (A → Bool) → Vec A n → Maybe A
maybe-filter-head p = uncurryʰ maybe-head ∘ filter p

결론:종속 제품은 비종속 버전처럼 기꺼이 카레를 만들고 카레를 하지 않습니다.

제쳐두고, 타입 시그니처로 작성하고 싶은 함수

head : ∀ {A} → ∃ (λ n → Vec A n) → IsTrue (n ≥ succ zero) → A

다음과 같이 쓸 수 있습니다: 

head : ∀ {A} → (p : ∃ (λ n → Vec A n)) → IsTrue (proj₁ p ≥ succ zero) → A

다른 팁

가장 좋은 방법은 종속 쌍을 먼저 해체하여 다음과 같이 작성할 수 있도록 하는 것입니다.

head :: ∀ {A n} → Vec A (S n) → A

그러나 함수 시그니처에서 종속 쌍을 그대로 유지하려면 쌍의 첫 번째 요소를 검사하고 그것이 양수인지 확인하는 조건자 PosN을 작성할 수 있습니다.

head :: ∀ {A p} → PosN p -> A

또는 유사합니다.연습문제로 PosN의 정의를 독자에게 맡기겠습니다.본질적으로 이것은 Vitus의 답변이 이미 수행한 작업이지만 대신 더 간단한 술어를 정의할 수 있습니다.

한동안 가지고 놀다가 처음에 원했던 기능과 유사한 솔루션을 생각해 냈습니다.

data ∃-non-empty (A : Set) : ∃ (λ n → Vec A n) → Set where
  ∃-non-empty-intro : ∀ {n} → {x : Vec A (succ n)} → ∃-non-empty A (succ n , x)

head : ∀ {A} → (e : ∃ (λ n → Vec A n)) → ∃-non-empty A e → A
head (zero   , [])       ()
head (succ _ , (x :: _)) ∃-non-empty-intro = x

누구든지 더 나은(또는 더 일반적인) 해결책을 생각해낸다면 나는 기꺼이 그들의 대답을 받아들일 것입니다.댓글도 환영합니다.

내가 생각해낸 좀 더 일반적인 술어는 다음과 같습니다.

data ∃-succ {A : Nat → Set} : ∃ A → Set where
  ∃-succ-intro : ∀ {n} → {x : A (succ n)} → ∃-succ (succ n , x)

-- or equivalently
data ∃-succ {A : Nat → Set} : ∃ (λ n → A n) → Set where
  ...

이건 평소랑 똑같아 head 에 대한 기능 Vec.

head' : ∀ {α} {A : Set α} → ∃ (λ n → Vec A (suc n)) → A
head' (_ , x ∷ _) = x
라이센스 : CC-BY-SA ~와 함께 속성
제휴하지 않습니다 StackOverflow
scroll top