Kind signatures and Type families
I expect
type family Rep a
and
type family Rep :: * -> *
to be the same, but it seems there is a difference
type family Rep a
type instance Rep Int = Char
-- ok
type family Rep :: * -> *
type instance Rep Int = Char
-- Expected kind * -> *, but got 'Int' instead
Have I simply stumbled over an Haskell extension bug, or is there some point to this behavior?
Yes, there is a subtle difference.
Roughly, type family F a :: *->* states that, say, F Int is an injective type constructor like [] , Maybe . This is exploited by the compiler, which can type check the following code:
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
To type check the above, the compiler exploited the fact that F Int a ~ F Int b implies a ~ b , which follows from injectivity.
Instead, declaring type family F ab :: * does not ensure injectivity of F Int , since the following becomes legal.
type family F a b :: *
type instance F Int a = ()
上一篇: pkg检查黑线鳕警告
下一篇: 亲笔签名和类型家庭