使用类型族更有效的类型级计算？

Question

根据Monad Reader第8期中的文章,我使用功能依赖和类型系列编写了"Instant Insanity"拼图的类型级解决方案:

• fundeps解决方案:http://lpaste.net/113108
• 类型家庭解决方案:http://lpaste.net/113113

fundeps解决方案大约需要200秒.而类型族版本在大约800秒内完成.

是否有任何技术可以使类型族版本更有效地运行？

Answer 1

我已将以下定义添加main到您的两个片段中，以便解决方案显示在抱怨缺少Show实例的类型错误消息中：

-- fundeps.hs
{-# OPTIONS_GHC -fcontext-stack=400 #-}
main = print $ solutions (undefined :: Cubes)

-- families-open.hs
{-# OPTIONS_GHC -ftype-function-depth=400 #-}
data Proxy a = Proxy
main = print (Proxy :: Proxy (Solutions Cubes))

并使用 GHC 7.8.3 进行编译以获得一些基准计时：

• fundeps.hs：23秒
• families-open.hs：46秒

我发现只需将类型系列版本转换为使用封闭类型系列（此处的代码）即可加快速度，足以消除差异：

• families-closed.hs：36秒

我以为我可以通过使用（此处的DataKinds代码）为类型系列提供严格的种类来加快速度，但令人惊讶的是，这让我回到了第一个方面：

• families-closed-datakinds.hs：44秒

然而，至少它产生了所有四个版本中最可读的输出：

No instance for (Show
                   (Proxy
                      '['['Cube 'G 'B 'W 'R 'B 'G, 'Cube 'W 'G 'B 'W 'R 'R,
                          'Cube 'R 'W 'R 'B 'G 'R, 'Cube 'B 'R 'G 'G 'W 'W],
                        '['Cube 'G 'B 'R 'W 'B 'G, 'Cube 'R 'R 'W 'B 'G 'W,
                          'Cube 'R 'G 'B 'R 'W 'R, 'Cube 'W 'W 'G 'G 'R 'B],
                        '['Cube 'G 'W 'R 'B 'B 'G, 'Cube 'W 'B 'W 'R 'G 'R,
                          'Cube 'R 'R 'B 'G 'W 'R, 'Cube 'B 'G 'G 'W 'R 'W],
                        '['Cube 'G 'R 'W 'B 'B 'G, 'Cube 'R 'W 'B 'G 'R 'W,
                          'Cube 'R 'B 'R 'W 'G 'R, 'Cube 'W 'G 'G 'R 'W 'B],
                        '['Cube 'G 'R 'B 'B 'W 'G, 'Cube 'W 'W 'R 'G 'B 'R,
                          'Cube 'R 'B 'G 'W 'R 'R, 'Cube 'B 'G 'W 'R 'G 'W],
                        '['Cube 'G 'W 'B 'B 'R 'G, 'Cube 'R 'B 'G 'R 'W 'W,
                          'Cube 'R 'R 'W 'G 'B 'R, 'Cube 'W 'G 'R 'W 'G 'B],
                        '['Cube 'G 'B 'B 'W 'R 'G, 'Cube 'W 'R 'G 'B 'W 'R,
                          'Cube 'R 'G 'W 'R 'B 'R, 'Cube 'B 'W 'R 'G 'G 'W],
                        '['Cube 'G 'B 'B 'R 'W 'G, 'Cube 'R 'G 'R 'W 'B 'W,
                          'Cube 'R 'W 'G 'B 'R 'R, 'Cube 'W 'R 'W 'G 'G 'B]]))

因此，看来至少可以用来加速代码的一种技术是使用封闭类型族。

截至 2014 年 12 月的绩效数据更新

正如我之前评论的那样，我也在 GHC 7.9 开发线上尝试了这些相同的程序，并发现了一些严重的性能下降。这导致了GHC 错误单，现已解决，结果令人惊叹：涉及类型系列的所有三种解决方案在即将发布的 GHC 7.10 版本上进行类型检查的速度将显着加快！

新的时序数据（截至GHCa225c70）如下：

• families-open.hs：7秒
• families-closed.hs：6.5秒
• families-closed-datakinds.hs：7.5秒

鉴于我在没有任何严格性的情况下运行这些测试，上述三个时间应该被视为相同，这意味着我肯定会选择封闭类型族+数据类型方法作为类型最多且产生最好输出的方法。