如何调试类型级别的程序 [英] How to debug type-level programs

问题描述

我正在尝试做一些沙发类型级别的编程，但它不起作用。我试着弄清楚为什么GHC完全无法推断我想要的类型签名。

有没有办法让GHC 告诉我它在干什么？

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

我也试过 -ddump-tc-trace ，它会抛出大约70KB的无法理解的乱码。 （特别是，我看不到任何用户编写的标识符在任何地方。）

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

解决方案

正如评论中所提到的那样：善良和善良！在GHCi中通常是我如何去做的，但令人惊讶的是，你放置这些功能的位置，看起来应该是相同的，并不总是如此。例如，我试图让一个依赖类型的函数等价于一个个人项目，它看起来像

pre> class IFunctor f其中
ifmap ::（a - > b） - > f n a - > fnb


我正在为

  data或者anb where 
 ILeft :: a  - > IE或者b b 
 IRight :: b  - >不管是（S $）b 
  

它应该相当简单，我认为只需忽略f左边的情况下，在右边应用它。

我试过了

$ pre $实例IFunctor（IE或a）其中
ifmap _l @（ILeft _）= l
ifmap f（IRight r）= IRight $ fr

，但是在这种情况下ifmap的专用版本是 ifmap ::（b - > c） - >或者Z b - >无论是Z c ，Haskell都推断L的类型为 IE或LHS上的Z b ，这是合理的，但是拒绝产生 b〜c 。

因此，我必须展开l，得到类型a的值，然后重新包装它以得到 IE或Z c 。

这不仅仅是依赖类型的情况，而且还有等级n类型。
例如，我想将适当形式的同构转换为自然转换，这应该相当容易。

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

I'm trying to do some hoopy type-level programming, and it just doesn't work. I'm tearing my hair out trying to figure out why the heck GHC utterly fails to infer the type signatures I want.

Is there some way to make GHC tell me what it's doing?

I tried -ddump-tc, which just prints out the final type signatures. (Yes, they're wrong. Thanks, I already knew that.)

I also tried -ddump-tc-trace, which dumps out ~70KB of unintelligible gibberish. (In particular, I can't see any user-written identifiers mentioned anywhere.)

My code is so close to working, but somehow an extra type variable keeps appearing. For some reason, GHC can't see that this variable should be completely determined. Indeed, if I manually write the five-mile type signature, GHC happily accepts it. So I'm clearly just missing a constraint somewhere... but where?!? >_<

解决方案

As has been mentioned in the comments, poking around with :kind and :kind! in GHCi is usually how I go about doing it, but it also surprisingly matters where you place the functions, and what looks like it should be the same, isn't always.

For instance, I was trying to make a dependently typed functor equivalent, for a personal project, which looked like

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

and I was writing the instance for

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

It should be fairly simple, I thought, just ignore f for the left case, apply it in the right.

I tried

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

but for the specialized version of ifmap in this case being ifmap :: (b -> c) -> IEither a Z b -> IEither a Z c, Haskell inferred the type of l to be IEither a Z b on the LHS, which, makes sense, but then refused to produce b ~ c.

So, I had to unwrap l, get the value of type a, then rewrap it to get the IEither a Z c.

This isn't just the case with dependent types, but also with rank-n types. For instance, I was trying to convert isomorphisms of a proper form into natural transformations, which should be fairly easy, I thought.

Apparently, I had to put the deconstructors in a where clause of the function, because otherwise type inference didn't work properly.

这篇关于如何调试类型级别的程序的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！