亲笔签名和类型家庭
我预计
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扩展错误，或者是否有一点指向这种行为？
是的，有一个微妙的区别。
粗略地说， type family F a :: *->*表明， F Int是一个类似于[] ， Maybe的内射类型构造函数。 这由编译器利用，它可以键入检查以下代码：
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 ，从注入其中如下。
相反，声明type family F ab :: *不能保证F Int注入性，因为以下内容变得合法。
type family F a b :: *
type instance F Int a = ()