이러한 선언 (같은 패턴에 대한)이 형식 검사기를 만족시키는 이유는 무엇입니까?

Question

저는 놀라운 TDDwI와 함께 간단하게 removeElem을 쓰고 있습니다. 그것에 대해

네 가지 질문 :

1. 가 왜 같은 패턴 3 명 선언을 쓸 수 있습니까?

2. absurd과 impossible의 차이점은 무엇입니까? [] 반환 세번째 경우

3. , []는 ... 따라서, 값 증거 xs가 a 제거했고, 바로 ... 한 것을?

4. 그 중 3 개를 모두 제거하면 기능이 여전히 남아 있으며 이상한 일이 일어나는 이상한 간질이 생깁니다. ?. 당신이 무엇을 중요하지 않게

---

removeElem : (value : a) 
      -> (xs : Vect (S n) a) 
      -> (prf : Elem value xs) 
      -> Vect n a 
removeElem value (value :: ys) Here = ys 
removeElem {n = Z} value (y :: []) (There later) = absurd later -- ?? 
removeElem {n = Z} value (y :: []) (There later) impossible  -- ?? 
removeElem {n = Z} value (y :: []) (There later) = []   -- ?? 
removeElem {n = (S k)} value (y :: ys) (There later) = 
    y :: removeElem value ys later 

Answer 1

가 왜 같은 패턴 3 명 선언을 쓸 수있는 증명하여 문자열 "안녕하세요"를 반환 할 수 있습니다

?

이 경우 (y :: []) 1 요소 벡터를 처리하기 때문에. 즉, later은 Elem value [] 유형을 갖습니다. 즉, 빈 목록에 value 요소가 있습니다. 즉, 은 터무니없는입니다. absurd의 유형은 Uninhabited t => t -> a이고 "유형이 t 인 경우 사람이 거주하지 않으며 해당 유형의 주민이있는 경우 임의로 유형 a"의 주민을 구성 할 수 있습니다. 따라서 해당 인터페이스 (here)를 구현하려면 Elem x []이 필요합니다. 그래서 absurd later가 작동합니다.

impossible은 Idris가 위의 모든 추측을 독자적으로 수행 할 수 있기 때문에 효과가 있습니다.

absurd과 impossible의 차이점은 무엇입니까?

impossible 키워드이 absurd 그냥 보조 정리 동안, 유형 체킹이되지 않는 경우를 배제 할 수 있습니다, 그래서 당신이 그것을 사용하는 경우 모든 유형 체킹해야합니다. [] 반환 세번째 경우

, []는 xs 제거하는 a가 있고, 바로 ... 한하는 값 때문에 ... 증거?

네, 맞습니다. removeElem은 값, 양수 길이의 벡터, 값이 벡터에 속해 있다는 증거를 가져 와서 감소 된 길이의 벡터를 반환합니다. 1 요소 벡터를 취하면 은 값과 증명을 무시하고 즉시 빈 벡터를 반환 할 수 있습니다. 내 요점은 당신이 증거를 사용할 필요가 없다는 것입니다, 그것은 당신에게 추가 보증을 제공하지만 당신은 그들을 무시할 자유입니다.

내가 그들 모두 3를 제거하는 경우, 함수가 여전히 전체, 그리고 내가 뭔가 이상한 여기

모두에서 잘되어 가고 있다고 설명 할 수없는 자극이 함수는 여전히 작동 - 이드리스는 할 수 있습니다 당신은 불가능한 경우를 생략합니다 :

removeElem {n = Z} value (y :: []) (There later) impossible 

Answer 2

상황은 불가능하다 (나는 그 질문이라고 생각). 하나가 2와 같으면 달이 치즈로 만들어진다는 것은 하나가 2와 같지 않기 때문에 진실한 진술이다. absurd은 Uninhabited t => t -> a의 기능입니다. Idris는 상황이 불가능하므로 당신이 그것을 처리 할 필요가 없다는 것을 알고 있습니다. 당신은 Vect 0 a = String

removeElem : (value : a) 
    -> (xs : Vect (S n) a) 
    -> (prf : Elem value xs) 
    -> Vect n a 
removeElem value (value :: ys) Here = ys 
removeElem {n = Z} value (y :: []) (There later) = absurd later -- ?? 
removeElem {n = Z} value (y :: []) (There later) impossible  -- ?? 
removeElem {a} {n = Z} value (y :: []) (There later) = rewrite (the (Vect 0 a = String) (absurd later)) in "Hi"   -- ?? 
removeElem {n = (S k)} value (y :: ys) (There later) = y :: removeElem value ys later