debugging - 如何调试类型级程序

Question

我正在尝试进行一些类型级别的编程，但它不起作用。我正在绞尽脑汁地试图弄清楚为什么 GHC 完全无法推断出我想要的类型签名。

有什么方法可以让 GHC 告诉我它在做什么吗？

我尝试了-ddump-tc，它只打印出最终的类型签名。 (是的，他们错了。谢谢，我已经知道了。)

我还尝试了 -ddump-tc-trace，它转储出约 70KB 的难以理解的乱码。 (特别是，我在任何地方都看不到任何用户编写的标识符。)

我的代码非常接近可以工作，但不知何故，一个额外的类型变量不断出现。由于某种原因，GHC 无法看到该变量应该被完全确定。事实上，如果我手动写下五英里类型的签名，GHC 会很高兴地接受它。所以我显然只是在某个地方缺少一个约束... 但是在哪里？!？>_<

Answer 1

正如评论中提到的，用 :kind 和 :kind! 来探索一下!在 GHCi 中通常是我这样做的方式，但令人惊讶的是，将函数放置在哪里也很重要，而且看起来应该是相同的，但事实并非总是如此。

例如，我试图为个人项目制作一个等价的依赖类型仿函数，看起来像

class IFunctor f where 
  ifmap :: (a -> b) -> f n a -> f n b 

我正在编写

的实例

data IEither a n b where 
  ILeft :: a -> IEither a Z b 
  IRight :: b -> IEither a (S n) b 

我想这应该相当简单，只需忽略左侧的 f ，将其应用到右侧即可。

我试过了

instance IFunctor (IEither a) where
  ifmap _ l@(ILeft _) = l 
  ifmap f (IRight r) = IRight $ f r

但对于本例中 ifmap 的特殊版本是 ifmap::(b -> c) -> IEither a Z b -> IEither a Z c，Haskell 将 l 的类型推断为在 LHS 上是 IEither a Z b，这是有道理的，但随后拒绝生成 b ~ c。

因此，我必须解开 l，获取类型 a 的值，然后重新包装它以获得 IEither a Z c。

这不仅是依赖类型的情况，也是 n 级类型的情况。例如，我试图将适当形式的同构转换为自然变换，我认为这应该相当容易。

显然，我必须将解构函数放在函数的 where 子句中，否则类型推断将无法正常工作。