我编写了以下类型来编码所有可能的有理数:
data Number : Type where
PosN : Nat -> Number
Zero : Number
NegN : Nat -> Number
Ratio : Number -> Number -> Number
请注意,PosN Z
实际编码数字1
,而NegN Z
编码-1
。我更喜欢Data.ZZ
模块给出的这种对称定义。现在我有一个问题,说服伊德里斯增加这样的数字是完全的:
mul : Number -> Number -> Number
mul Zero _ = Zero
mul _ Zero = Zero
mul (PosN k) (PosN j) = PosN (S k * S j - 1)
mul (PosN k) (NegN j) = NegN (S k * S j - 1)
mul (NegN k) (PosN j) = NegN (S k * S j - 1)
mul (NegN k) (NegN j) = PosN (S k * S j - 1)
mul (Ratio a b) (Ratio c d) = Ratio (a `mul` b) (c `mul` d)
mul (Ratio a b) c = Ratio (a `mul` c) b
mul a (Ratio b c) = Ratio (a `mul` b) c
plus : Number -> Number -> Number
plus Zero y = y
plus x Zero = x
plus (PosN k) (PosN j) = PosN (k + j)
plus (NegN k) (NegN j) = NegN (k + j)
plus (PosN k) (NegN j) = subtractNat k j
plus (NegN k) (PosN j) = subtractNat j k
plus (Ratio a b) (Ratio c d) =
let a' = assert_smaller (Ratio a b) a in
let b' = assert_smaller (Ratio a b) b in
let c' = assert_smaller (Ratio c d) c in
let d' = assert_smaller (Ratio c d) d in
Ratio ((mul a' d') `plus` (mul b' c')) (mul b' d')
plus (Ratio a b) c =
let a' = assert_smaller (Ratio a b) a in
let b' = assert_smaller (Ratio a b) b in
Ratio (a' `plus` (mul b' c)) c
plus a (Ratio b c) =
let b' = assert_smaller (Ratio b c) b in
let c' = assert_smaller (Ratio b c) c in
Ratio ((mul a c') `plus` b') (mul a c')
有趣的是,当我在Atom编辑器中按下Alt-Ctrl-R时,一切都很好(即使使用%default total
指令)。但是,当我将其加载到REPL中时,它警告我plus
可能不是全部:
|
29 | plus Zero y = y
| ~~~~~~~~~~~~~~~
Data.Number.NumType.plus is possibly not total due to recursive path
Data.Number.NumType.plus --> Data.Number.NumType.plus
从消息我明白,它担心这些递归调用plus
模式处理比率。我认为断言a
小于Ratio a b
等会解决问题,但事实并非如此,所以伊德里斯可能会看到这一点,但却遇到了其他问题。但是,我无法弄清楚它可能是什么。
assert_smaller (Ratio a b) a
已经为Idris所知(a
毕竟是“更大”的Ratio a b
类型的论据)。你需要证明(或断言)的是,mul
的结果在结构上小于plus
的论据。
所以它应该合作
plus (Ratio a b) (Ratio c d) =
let x = assert_smaller (Ratio a b) (mul a d) in
let y = assert_smaller (Ratio a b) (mul b c) in
Ratio (x `plus` y) (mul b d)
plus (Ratio a b) c =
let y = assert_smaller (Ratio a b) (mul b c) in
Ratio (a `plus` y) c
plus a (Ratio b c) =
let x = assert_smaller (Ratio b c) (mul a c) in
Ratio (x `plus` b) (mul a c)