Idris에서 최소한의 게으른 버전을 작성하는 방법은 무엇입니까?

Question

inf : Nat 
inf = S inf 

minimum' : Lazy Nat -> Lazy Nat -> Lazy Nat 
minimum' Z b = Z 
minimum' b Z = Z 
minimum' (S a) (S b) = S (minimum' a b) 

main : IO() 
main = do 
    print $ Force $ minimum' 2 inf 

내가 minimum 2 inf이 2을 것으로 평가하지만, 내 코드가 작동하지 않는 것 같습니다 있도록 최소의 게으른 버전을 작성하려면, 그것은 결코 멈추지, 최소의 "게으른"버전은 그래서, 어떤 다른하지 않습니다 정말 게으른 버전을 작성하는 법?

Answer 1

게으른 Nat는 유도 성 Nat와 동일하지 않습니다. Nat에는 2 개의 생성자, Z와 S가 있습니다. S는 Lazy Nat를 사용하도록 변형되어야합니다. 동일해야

codata CoNat : Type where 
    Z : CoNat 
    S : CoNat -> CoNat 

가로 :

data CoNat : Type where 
    Z : CoNat 
    S : Inf CoNat -> CoNat 

당신이 키워드 또는 사용하는 "전체"를 사용하십시오 "% 기본

당신은 coinductive 그래서 같은 냇를 쓸 수 있습니다 합계 "로 계산합니다. 이렇게하면 Idris가 올바른 위치의 오류 메시지를 알려줍니다.

CoNat와 Nat가 모두있는 경우 몇 가지 다른 서명으로 minimum'을 작성할 수 있습니다. 어쩌면 CoNat -> CoNat -> CoNat을 원할 수도 있습니다. 나는 대신 슈퍼 간단한 하나를 갔다 :

total 
inf : CoNat 
inf = S inf 

total 
minimum' : Nat -> CoNat -> Nat 
minimum' Z b = Z 
minimum' b Z = Z 
minimum' (S a) (S b) = S (minimum' a b) 

total 
main : IO() 
main = do 
    print $ minimum' 2 inf