为什么此"with"块会破坏此功能的整体? [英] Why does this 'with' block spoil the totality of this function?
问题描述
我正在尝试通过自然数来计算奇偶校验和一半的底数:
I'm trying to compute parity together with the floor of the half, over natural numbers:
data IsEven : Nat -> Nat -> Type where
Times2 : (n : Nat) -> IsEven (n + n) n
data IsOdd : Nat -> Nat -> Type where
Times2Plus1 : (n : Nat) -> IsOdd (S (n + n)) n
parity : (n : Nat) -> Either (Exists (IsEven n)) (Exists (IsOdd n))
我尝试使用parity
的明显实现:
I tried going with the obvious implementation of parity
:
parity Z = Left $ Evidence _ $ Times2 0
parity (S Z) = Right $ Evidence _ $ Times2Plus1 0
parity (S (S n)) with (parity n)
parity (S (S (k + k))) | Left (Evidence _ (Times2 k)) =
Left $ rewrite plusSuccRightSucc k k in Evidence _ $ Times2 (S k)
parity (S (S (S ((k + k))))) | Right (Evidence _ (Times2Plus1 k)) =
Right $ rewrite plusSuccRightSucc k k in Evidence _ $ Times2Plus1 (S k)
此类型检查并按预期工作.但是,如果我尝试将parity
标记为total
,则Idris开始抱怨:
This typechecks and works as expected. However, if I try to mark parity
as total
, Idris starts complaining:
parity is possibly not total due to: with block in parity
我在parity
中看到的唯一with
块是从parity (S (S n))
到parity n
的递归调用的块,但是显然,这是有充分根据的,因为n
在结构上小于S (S n)
.
The only with
block I see in parity
is the one with the recursive call from parity (S (S n))
to parity n
, but clearly that is well-founded, since n
is structurally smaller than S (S n)
.
如何使Idris相信parity
是总数?
How do I convince Idris that parity
is total?
推荐答案
对我来说这似乎是个错误,因为以下基于case
的解决方案通过了总计检查器:
It looks like a bug to me, because the following solution based on case
passes the totality checker:
total
parity : (n : Nat) -> Either (Exists (IsEven n)) (Exists (IsOdd n))
parity Z = Left $ Evidence _ $ Times2 0
parity (S Z) = Right $ Evidence _ $ Times2Plus1 0
parity (S (S k)) =
case (parity k) of
Left (Evidence k (Times2 k)) =>
Left $ rewrite plusSuccRightSucc k k in Evidence _ $ Times2 (S k)
Right (Evidence k (Times2Plus1 k)) =>
Right $ rewrite plusSuccRightSucc k k in Evidence _ $ Times2Plus1 (S k)
这篇关于为什么此"with"块会破坏此功能的整体?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!