haskell - 种类签名和类型系列

Question

我期待

type family Rep a

和

type family Rep :: * -> *

虽然是一样的，但是好像还是有区别

type family   Rep a
type instance Rep Int  = Char
-- ok

type family   Rep :: * -> *
type instance Rep Int  = Char
-- Expected kind * -> *, but got 'Int' instead

我只是偶然发现了 Haskell 扩展错误，还是这种行为有某种意义？

Answer 1

是的，有细微的差别。

粗略地说，类型族 F a::*->* 表明，F Int 是一个单射类型构造函数，例如 []，也许。编译器可以利用这一点，对以下代码进行类型检查:

type family F a :: * -> *

-- these three examples can be removed / changed, if wished
type instance F Int = []
type instance F Char = Maybe
type instance F Bool = (,) String

foo :: (F Int a :~: F Int b) -> (a :~: b)
foo Refl = Refl

为了对上面的内容进行类型检查，编译器利用了以下事实:F Int a ~ F Int b 意味着 a ~ b，这是从单射性得出的。

相反，声明类型族 F a b::* 并不能确保 F Int 的单射性，因为以下内容变得合法。

type family F a b :: *
type instance F Int a = ()