Haskell kind system vs type families and multi param type classes

Question

In Haskell I find it difficult to completely grasp the purpose of a kind system, and what it truly adds to the language.

I understand having kinds adds safety. For example consider fmap :: (a -> b) -> f a -> f b vs a monokinded version of it fmap2 :: (a -> b) -> p -> q.

My understanding is that, thanks to the kind system, I can specify beforehand with higher detail what the shape of the data should be. It is better, as the type checker can check more, and stricter requirements will make it less likely that users will mess up with types. This will reduce the likelihood of programming errors. I believe this is the main motivation for kinds but I might be wrong.

Now I think fmap2 can have the same implementation as fmap, since its types are unconstrained. Is it true?

Could one just replace all multi kinded types in the base/ghc library by mono kinded ones, and would it still compile correctly?

To clarify a little bit I mean that for a class like:

class  Functor f  where
    fmap        :: (a -> b) -> f a -> f b
    (<$)        :: a -> f b -> f a

I might replace it by something like

class  Functor a b p q  where
    fmap        :: (a -> b) -> p -> q
    (<$)        :: a -> q -> p

This way for a Functor instance like

instance Functor [] where fmap = map

I might replace it by

instance Functor a b p q where fmap = map

Remark: This wont work as is because i also need to modify map and go down the dependency chain. Will think more about this later..

I'm trying to figure out if kinds add more than just safety? Can I do something with multi kinded types that I cannot do with mono kinded ones?

Remark: Here I forgot to mention i'm usually using some language extensions, typically to allow more flexibility in writing classes. When doing vanilla haskell kinds can be really meaningful thing to use. But when I start using type families, and a few of other extensions it becomes much less clear that I need kinds at all.

I have in mind that there is some monotraversable library which reimplements many standard library functions using single kinded types, and type families to generalize signatures. That's why my intuition is that multi kinded variables might not really add that much expressive power after all, provided one uses type families. However a drawback of doing this is that you lose type safety. My question is do you really only lose just that, or do you really lose something else.

Answer 1

让我们备份。你似乎认为因为签名

id2 :: a -> b

比

id :: a -> a

这id2可能具有相同的执行情况id。但事实并非如此。实际上id2没有完全实现（任何实现都id2涉及无限循环或undefined）。

普遍性的结构会产生“压力”，而这种压力是我们必须导航才能为某事找到正确类型的原因。iff比 更通用g，这意味着可以在任何地方g使用，f也可以，但也意味着 的任何实现f都是 的有效实现g。因此，在使用站点上，它朝一个方向发展，而在定义站点上，它朝另一个方向发展。

我们可以id2在我们可以使用的任何地方使用id，但是 的签名id2太笼统了，无法实现。签名越通用，可以使用的上下文就越多，但实现的可能性也就越小。我想说一个好的类型签名的主要目标是找到尽可能少的预期函数实现的通用级别，而不是完全不可能编写。

你提议的签名fmap2 :: (a -> b) -> p -> q就像 一样id2，太笼统了，不可能实现。高级类型的目的是为我们提供具有非常通用的签名的工具，例如fmap，但不太通用fmap2。