为什么 ghci 脱糖类型列表和类型族? 这可以被选择性禁用吗？

我试图使类型 ghci 显示为我的库尽可能直观，但我遇到了很多困难，当使用更高级的类型功能。

假设我在一个文件中有这样的代码:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}


import GHC.TypeLits


data Container (xs::[*]) = Container

我用 ghci 加载它，然后输入以下命令:

ghci> :t undefined :: Container '[String,String,String,String,String]

不幸的是，ghci 给了我一个相当难看的外表:

:: Container
((':)
*
String
((':)
* String ((':) * String ((':) * String ((':) * String ('[] *))))))

Ghci 删除了类型级别字符串的 Sugar。有没有什么办法可以阻止 Ghi 这么做给我一个漂亮的版本？

在一个相关的说明中，让我们假设我创建了一个类型级别的 Replicate函数

data Nat1 = Zero | Succ Nat1


type family Replicate (n::Nat1) x :: [*]
type instance Replicate Zero x = '[]
type instance Replicate (Succ n) x = x ': (Replicate n x)


type LotsOfStrings = Replicate (Succ (Succ (Succ (Succ (Succ Zero))))) String

现在，当我使用 LotsOfStrings请求 ghci 输入一个类型时:

ghci> :t undefined :: Container LotsOfStrings

Ghci 很不错，给了我一个很好的结果:

undefined :: Container LotsOfStrings

但如果我要 Replicated 版本,

ghci> :t undefined :: Container (Replicate (Succ (Succ (Succ (Succ (Succ Zero))))) String)

Ghci 替换了类型族，但是没有替换类型同义词:

:: Container
((':)
*
[Char]
((':)
* [Char] ((':) * [Char] ((':) * [Char] ((':) * [Char] ('[] *))))))

为什么 ghci 替换类型族而不替换类型同义词？有没有办法控制 ghci 什么时候进行置换？

3072 次浏览
小开 
import GHC.TypeLits


data Container (xs::[*]) = Container

I load it up in ghci, then I type the following command:

:t undefined :: Container '[String,String,String,String,String]
小开

The workaround that I know of is using :kind. For instance,

ghci> :kind (Container '[String,String,String,String,String])

Gives:

( Container '[String,String,String,String,String]) :: *

While

ghci> :kind! (Container '[String,String,String,String,String])

Will print something like this:

Container

((':)

  *
[Char]
((':)
* [Char] ((':) * [Char] ((':) * [Char] ((':) * [Char] ('[] *))))))

Officially, of course, you're asking ghci a different question with kind, but it works. Using undefined :: is sort of a workaround anyhow, so I thought this might suffice.

小开

This is fixed in upcoming GHC 7.8.

GHC 7.6 prints kinds if a datatype uses PolyKinds. So you see (':) * String ('[] *) instead of just (':) String '[].

In GHC 7.8, kinds are no longer shown by default and your datatype is pretty printed as a list, as you would expect. You can use the new flag -fprint-explicit-kinds to see explicit kinds as in GHC 7.6. I don't know the reasons for this, presumably explicit kinds were meant to be an aid for understanding PolyKinds.


提交答案