Я написал следующий тип, чтобы закодировать в нем все возможные рациональные числа:
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')
Интересно, что когда я нажимаю Alt-Ctrl-R в редакторе Atom, все в порядке (даже с директивой %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
и т. Д., Решит проблему, но этого не произошло, так что, вероятно, Идрис это видит, но у него проблемы с чем-то другим. Однако я не могу понять, что это могло быть.