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.

@WillemVanOnsem Yes, so am I correct that fmap2 is strictly more general than fmap and its implementation could be identical? — jam
Im not an expert of type theory, i've been looking at this article en.wikipedia.org/wiki/Kind_(type_theory) but I find it hard to understand the deep underlying reason why this whole kind system really exist — jam
As there is type based function level programming, there is kind based type level programming and perhaps even a sort based kind level programming might exist in the future. Types and Kinds and Sorts, Oh My! is a good read. — Redu
@J.M. you are not correct about that. It is more general, but it cannot be implemented. — luqui
The complete type of fmap is actually longer than what you say in your question: fmap :: Functor f => (a -> b) -> f a -> f b. How would you state the constraint analogous to Functor f for your proposed alternative type? — Daniel Wagner

luqui luqui · Accepted Answer · 2019-12-25T19:47:57

Let's back up. It seems like you think that because the signature

id2 :: a -> b

is more general than

id :: a -> a

that id2 could have the same implementation as id. But that's not true. In fact id2 has no total implementation (any implementation of id2 involves an infinite loop or undefined).

The structure of generality creates a "pressure", and this pressure is what we must navigate to find the right type for something. If f is more general than g, that means that anywhere g could be used, f could also but it also means that any implementation of f is a valid implementation of g. So at the use site it goes one direction, at the definition site it goes the other.

We can use id2 anywhere we could have used id, but the signature of id2 is so general that it is impossible to implement. The more general a signature gets, the more contexts it can be used in, but also the less likely it is to have an implementation. I would say a main goal of a good type signature is to find the level of generality where there are as few as possible implementations of your intended function, without making it impossible to write altogether.

Your proposed signature fmap2 :: (a -> b) -> p -> q is, like id2, so general that it is impossible to implement. The purpose of higher-kinded types is to give us the tools to have very general signatures like fmap, which are not too general like fmap2.

Haskell kind system vs type families and multi param type classes

1 Answers