基于GHC的依赖型程序设计的运行时间成本

Question

我正在哈斯克尔设计一个可靠的类型化的图书馆。通过对测试可执行文件进行分析，我可以看到如下内容：

commutativity' Math 1189 4022787186 29.1 27.2 29.1 27.2

commutativity'基本上是类型级整数的整数相加交换性性质的(递归)证明.其定义如下：

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%都花在了完全无用的东西上。

我天真地以为这不会发生。

我能做些什么来优化这些无用的呼叫吗？

Answer 1

如果您非常确定证明术语终止，则可以使用以下内容

unsafeProof :: proof -> proof
unsafeProof _ = unsafeCoerce ()

someFunction :: forall n m.  ...
someFunction = case unsafeProof myProof :: Plus (S n) m :~: Plus n (S m) of
   Refl -> ...

这必须仅用于具有单个无参数构造函数的类型，例如用于Refl的a :~: b。否则，您的程序可能会崩溃或行为怪异。注意，清空者！

更安全(但仍然不安全！)变体

unsafeProof :: a :~: b -> a :~: b
unsafeProof _ = unsafeCoerce ()

请注意，如果您将底部传递给程序，仍然可以使程序崩溃。

我希望有一天，GHC将安全、自动地执行这一优化，通过静态分析确保终止。