如何调试类型级程序

Question

我正在尝试做一些hoopy类型级编程,它只是不起作用.我正在试图弄清楚为什么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 的类型在IEither a Z bLHS 上，这是有道理的，但随后拒绝生成b ~ c。

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

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

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