我正在
Haskell中编写一个依赖类型的库.在我的测试可执行文件上使用分析,我看到类似于：
commutativity' Math 1189 4022787186 29.1 27.2 29.1 27.2
“交换性”基本上是(递归)证明类型级整数的整数加法交换性质.它定义如下：
commutativity' :: SNat n -> SNat m -> Plus (S n) m :~: Plus n (S m) commutativity' SZ m = Refl commutativity' (SS n) m = gcastWith (commutativity' n m) Refl
然后在我的库中使用gcastWith来证明各种类型的等价性.
所以……我的运行时有29％用在完全没用的东西上,因为类型检查是在编译时发生的.
我天真地认为这不会发生.
我能做些什么来优化这些无用的通话吗？
解决方法
如果您非常确定证明术语终止,您可以使用类似的东西
unsafeProof :: proof -> proof unsafeProof _ = unsafeCoerce () someFunction :: forall n m. ... someFunction = case unsafeProof myProof :: Plus (S n) m :~: Plus n (S m) of Refl -> ...
这必须仅用于具有单个无参数构造函数的类型,例如,反映a：〜：b.否则,您的程序可能会崩溃或表现得很奇怪.买者自负！
一个更安全(但仍然不安全！)的变体可能是
unsafeProof :: a :~: b -> a :~: b unsafeProof _ = unsafeCoerce ()
请注意,如果将底部传递给它,您仍然可以使程序崩溃.
我希望有一天GHC能够安全自动地执行这种优化,确保通过静态分析终止.
版权声明：本文内容由互联网用户自发贡献，该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容， 请发送邮件至 [email protected] 举报，一经查实，本站将立刻删除。
