idris - 让 Idris 相信递归调用的整体性
问题描述
我编写了以下类型来编码其中所有可能的有理数:
data Number : Type where
PosN : Nat -> Number
Zero : Number
NegN : Nat -> Number
Ratio : Number -> Number -> Number
请注意,PosN Z
实际上编码 number 1
,而NegN Z
编码-1
. 我更喜欢这样的对称定义,而不是Data.ZZ
module 给出的定义。现在我很难说服 Idris 将这些数字相加是总数:
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
etc. 可以解决问题,但它没有,所以 Idris 可能看到了这一点,但遇到了其他问题。不过,我无法弄清楚它可能是什么。
解决方案
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)
推荐阅读
- excel - 发送多封邮件时出现 Outlook 错误:“该项目已被移动或删除”
- sparql - 如何在 SPARQL 中获取特定类型的个人?
- python-3.x - 如何从python3中的类外访问类内函数的变量
- winforms - FireRequestAction 未在按钮单击时触发
- java - 我如何在java中的同一个for循环中返回和递增
- asp.net-core - 我可以为 Blazor 服务器页面设置 mime 类型吗?
- php - 在 aws lambda 中执行 php
- c - 多个数组的元素总和的内存高效 MPI 并行实现
- python - Tensorflow ImportError:DLL 加载失败:%1 不是有效的 Win32 应用程序
- azure - PowerShell 脚本可在 Azure 门户中创建新资源时获取通知