亲切的签名和类型系列

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

是的,有一个微妙的区别.

粗略地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 a b :: *并不能确保注入性F Int,因为以下内容变得合法.

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