haskell – 使用GHC进行依赖类型编程的运行时成本

2023年4月9日 215次阅读

我正在
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能够安全自动地执行这种优化,确保通过静态分析终止.

点赞