이드리스 유도 단계

에 대한 증거는 다음과 같은 기능 나는 다음과 같은 오류가 컴파일하려고이드리스 유도 단계

tryMove : (diskNumber : Nat) -> (from: Peg) -> (to: Peg)-> {default Oh prf: So (from /= to)} -> Disposition diskNumber -> Maybe (Disposition diskNumber) 
tryMove Z from to [] = Nothing 
tryMove (S k) from to (smallestDiskPosition :: restOfTheDisposition) = 
     map (smallestDiskPosition ::) (tryMove k from to restOfTheDisposition)

을 고려하십시오. 내가 명시 적으로

tryMove : (diskNumber : Nat) -> (from: Peg) -> (to: Peg)-> {default Oh prf: So (from /= to)} -> Disposition diskNumber -> Maybe (Disposition diskNumber) 
tryMove Z from to [] = Nothing 
tryMove (S k) from to {prf} (smallestDiskPosition :: restOfTheDisposition) = 
     map (smallestDiskPosition ::) (tryMove k from to {prf} restOfTheDisposition)

같이 {prf}을 전달하면 이 제대로 컴파일합니다.

왜 Idris는 귀납적 인 단계에서 증명을 자동으로 감지 할 수없는 반면, 정상적인 기능 호출에서이를 수행 할 수있는 이유는 무엇입니까?

편집 : 여기

완전한 요점은 사용하는 것입니다 이드리스는 재귀 호출에 Oh를 전달하는 데 노력하고있다, 그래서 https://gist.github.com/marcosh/d51479ea08e8522560713fd1e5ca9624

출처

2017-10-06 marcosh

당신은, prf의 기본값 (Oh)를 공급한다. 해당 오류 메시지가 표시 그 이유는, Oh는 So True을 입력 가지고 있으며, 이드리스는 prf 유형 So (from /= to) 될 것으로 예상하지만 to 및 from을 소멸하지 않기 때문에, 이드리스는 from /= to의 가치를 알 수 없다.

{auto prf: So (from /= to)}을 포함하도록 서명을 변경하거나 prf 인수를 모두 삭제할 수 있습니다. 실제로 사용하지 않으므로 아무 것도 수정하지 않고 재귀 호출에 전달하면됩니다.

출처

2017-10-06 10:33:14

답장을 보내 주셔서 감사합니다. 나는 하나의 것을 이해하지 못한다. '이드리스가 /로부터'의 가치를 알 수 없다는 점에서'와 함께 파괴하지 않기 때문에'무엇을 의미합니까? 'from'과'to'는 초기 호출과 동일합니다. 그들이 초기에 다른 경우, 왜 이드리스는 그들이 다르고 있다는 것을 알 수 없습니까? 또한, '~'과 '~'을 파괴하면 무엇을 의미합니까? 내가 어떻게 할 수 있니? – marcosh

Idris가 'So (from/= to)'타입의 값을 기대하는 곳에 'So True' 타입의'Oh '을 전달하면 Idris는'from/= to'와'True'가있는 한 그렇게 할 수 있습니다 'from/= to'가'True'로 평가되면이 경우에는 정의 적으로 같거나 더 정확합니다. 그러나'(/ =)'함수 응용 프로그램을 평가하려면 두 인수가 정확히 무엇인지 알아야합니다. Idris는 'from'과 'to'가 동일하지 않다는 것을 알지 못합니다. 패턴 일치는 정보를 전달하는 방식입니다. 그래서, Idris가'from '과'to'에 패턴 매치하는 것을 돕는 매우 추악한 방법은 - 이것은 9 개의 절 (3 개는 불가능 함)을 생성합니다. –

이드리스 유도 단계

답변

관련 문제