**Ci sono tipi e tipi**

ovvero come si traducono i giochi di parole di Miran? mica facile! ovvero non sono tanto buono. Ma come distinguere in italiano “type” e “kind”.

Type constructors take other types as parameters to eventually produce concrete types. That kind of reminds me of functions, which take values as parameters to produce values. We’ve seen that type constructors can be partially applied (** Either String** is a type that takes one type and produces a concrete type, like

**), just like functions can. This is all very interesting indeed. In this section, we’ll take a look at formally defining how types are applied to type constructors, just like we took a look at formally defining how values are applied to functions by using type declarations. You don’t really have to read this section to continue on your magical Haskell quest and if you don’t understand it, don’t worry about it. However, getting this will give you a very thorough understanding of the type system.**

`Either String Int`

So, values like ** 3**,

**or**

`"YEAH"`

**(functions are also values, because we can pass them around and such) each have their own type. Types are little labels that values carry so that we can reason about the values. But types have their own little labels, called kinds. A kind is more or less the type of a type. This may sound a bit weird and confusing, but it’s actually a really cool concept.**

`takeWhile`

What are kinds and what are they good for? Well, let’s examine the kind of a type by using the ** :k** command in GHCI.

`Prelude> `**:k Int**
Int :: *

A star? How quaint. What does that mean? A ** *** means that the type is a concrete type. A concrete type is a type that doesn’t take any type parameters and values can only have types that are concrete types. If I had to read

**out loud (I haven’t had to do that so far), I’d say star or just type.**

`*`

Okay, now let’s see what the kind of ** Maybe** is.

`Prelude> `**:k Maybe**
Maybe :: * -> *

The ** Maybe** type constructor takes one concrete type (like

**) and then returns a concrete type like**

`Int`

**. And that’s what this kind tells us. Just like**

`Maybe Int`

**means that a function takes an Int and returns an**

`Int -> Int`

**,**

`Int`

**means that the type constructor takes one concrete type and returns a concrete type. Let’s apply the type parameter to**

`* -> *`

**and see what the kind of that type is.**

`Maybe`

`Prelude> `**:k Maybe Int**
Maybe Int :: *

Just like I expected! We applied the type parameter to ** Maybe** and got back a concrete type (that’s what

**means. A parallel (although not equivalent, types and kinds are two different things) to this is if we do**

`* -> *`

**and**

`:t isUpper`

**.**

`:t isUpper 'A'`

**has a type of**

`isUpper`

**and**

`Char -> Bool`

**has a type of**

`isUpper 'A'`

**, because its value is basically**

`Bool`

**. Both those types, however, have a kind of**

`True`

**.**

`*`

`Prelude> `**import Data.Char (isUpper)**
Prelude Data.Char> **:t isUpper**
isUpper :: Char -> Bool
Prelude Data.Char> **:t isUpper 'A'**
isUpper 'A' :: Bool
Prelude Data.Char> **:k isUpper**
:1:1: error: Not in scope: type variable ‘isUpper’
Prelude Data.Char> :k Data.Char.isUpper
:1:1: error: parse error on input ‘Data.Char.isUpper’

mystero kwy: non trovo il kind.

We used ** :k** on a type to get its kind, just like we can use

**on a value to get its type. Like we said, types are the labels of values and kinds are the labels of types and there are parallels between the two.**

`:t`

Let’s look at another kind.

`Prelude> `**:k Either**
Either :: * -> * -> *

produce a concrete type. It also looks kind of like a type declaration of a function that takes two values and returns something. Type constructors are curried (just like functions), so we can partially apply them.

`Prelude> `**:k Either**
Either :: * -> * -> *
Prelude> **:k Either String**
Either String :: * -> *
Prelude> **:k Either String Int**
Either String Int :: *

When we wanted to make ** Either a** part of the

**typeclass, we had to partially apply it because**

`Functor`

**wants types that take only one parameter while**

`Functor`

**takes two. In other words,**

`Either`

**wants types of kind**

`Functor`

**and so we had to partially apply**

`* -> *`

**to get a type of kind**

`Either`

**instead of its original kind**

`* -> *`

**. If we look at the definition of**

`* -> * -> *`

**again**

`Functor`

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

we see that the ** f** type variable is used as a type that takes one concrete type to produce a concrete type. We know it has to produce a concrete type because it’s used as the type of a value in a function. And from that, we can deduce that types that want to be friends with

**have to be of kind**

`Functor`

**.**

`* -> *`

Now, let’s do some type-foo. Take a look at this typeclass that I’m just going to make up right now:

**class Tofu t where
tofu :: j a -> t a j**

Man, that looks weird. How would we make a type that could be an instance of that strange typeclass? Well, let’s look at what its kind would have to be. Because ** j a** is used as the type of a value that the

**function takes as its parameter,**

`tofu`

**has to have a kind of**

`j a`

**. We assume**

`*`

**for**

`*`

**and so we can infer that**

`a`

**has to have a kind of**

`j`

**. We see that**

`* -> *`

**has to produce a concrete value too and that it takes two types. And knowing that**

`t`

**has a kind of**

`a`

**and**

`*`

**has a kind of**

`j`

**, we infer that**

`* -> *`

**has to have a kind of**

`t`

**. So it takes a concrete type (**

`* -> (* -> *) -> *`

**), a type constructor that takes one concrete type (**

`a`

**) and produces a concrete type. Wow.**

`j`

OK, so let’s make a type with a kind of ** * -> (* -> *) -> ***. Here’s one way of going about it.

`data Frank a b = Frank {frankField :: b a} deriving (Show)`

How do we know this type has a kind of ** * -> (* -> *) - > ***? Well, fields in ADTs are made to hold values, so they must be of kind

**, obviously. We assume**

`*`

**for**

`*`

**, which means that**

`a`

**takes one type parameter and so its kind is**

`b`

**. Now we know the kinds of both**

`* -> *`

**and**

`a`

**and because they’re parameters for**

`b`

**, we see that**

`Frank`

**has a kind of**

`Frank`

**The first**

`* -> (* -> *) -> *`

**represents**

`*`

**and the**

`a`

**represents**

`(* -> *)`

**. Let’s make some**

`b`

**values and check out their types.**

`Frank`

`Prelude> `**import Data.Char**
Prelude Data.Char> **:set prompt "ghci> "**
ghci> **data Frank a b = Frank {frankField :: b a} deriving (Show)**
ghci> **:t Frank {frankField = Just "HAHA"}**
Frank {frankField = Just "HAHA"} :: Frank [Char] Maybe
ghci> **:t Frank {frankField = "YES"}**
Frank {frankField = "YES"} :: Frank Char []

non ho riportato tutto l’esempio, avrei dovuto caricare ** Tree** definito in un post precedente.

Hmm. Because ** frankField** has a type of form

**, its values must have types that are of a similar form as well. So they can be**

`a b`

**, which has a type of**

`Just "HAHA"`

**or it can have a value of**

`Maybe [Char]`

**, which has a type of**

`['Y','E','S']`

**(if we used our own list type for this, it would have a type of**

`[Char]`

**). And we see that the types of the**

`List Char`

**values correspond with the kind for**

`Frank`

**.**

`Frank`

**has a kind of**

`[Char]`

**and**

`*`

**has a kind of**

`Maybe`

**. Because in order to have a value, it has to be a concrete type and thus has to be fully applied, every value of**

`* -> *`

**has a kind of**

`Frank blah blaah`

**.**

`*`

Making ** Frank** an instance of

**is pretty simple. We see that**

`Tofu`

**takes a**

`tofu`

**(so an example type of that form would be**

`j a`

**) and returns a**

`Maybe Int`

**. So if we replace**

`t a j`

**with**

`Frank`

**, the result type would be**

`j`

**.**

`Frank Int Maybe`

**instance Tofu Frank where
tofu x = Frank x**

Il codice seguente non riesco a eseguirlo; non ho capito perché.

`ghci> `**tofu (Just 'a') :: Frank Char Maybe**
Frank {frankField = Just 'a'}
ghci> **tofu ["HELLO"] :: Frank [Char] []**
Frank {frankField = ["HELLO"]}

Not very useful, but we did flex our type muscles. Let’s do some more type-foo. We have this data type:

**ghci> data Barry t k p = Barry { yabba :: p, dabba :: t k }**

And now we want to make it an instance of ** Functor**. Functor wants types of kind

**but**

`* -> *`

**doesn’t look like it has that kind. What is the kind of**

`Barry`

**? Well, we see it takes three type parameters, so it’s going to be**

`Barry`

**. It’s safe to say that**

`something -> something -> something -> *`

**is a concrete type and thus has a kind of**

`p`

**. For**

`*`

**, we assume**

`k`

**and so by extension,**

`*`

**has a kind of**

`t`

**. Now let’s just replace those kinds with the somethings that we used as placeholders and we see it has a kind of**

`* -> *`

**. Let’s check that with GHCI.**

`(* -> *) -> * -> * -> *`

`ghci> `**:k Barry**
Barry :: (* -> *) -> * -> * -> *

Ah, we were right. How satisfying. Now, to make this type a part of ** Functor** we have to partially apply the first two type parameters so that we’re left with

**. That means that the start of the instance declaration will be:**

`* -> *`

**. If we look at**

`instance Functor (Barry a b) where`

**as if it was made specifically for**

`fmap`

**, it would have a type of**

`Barry`

**, because we just replace the**

`fmap :: (a -> b) -> Barry c d a -> Barry c d b`

**‘s**

`Functor`

**with**

`f`

**. The third type parameter from**

`Barry c d`

**will have to change and we see that it’s conviniently in its own field.**

`Barry`

**instance Functor (Barry a b) where
fmap f (Barry {yabba = x, dabba = y}) = Barry {yabba = f x, dabba = y}**

There we go! We just mapped the ** f** over the first field.

In this section, we took a good look at how type parameters work and kind of formalized them with kinds, just like we formalized function parameters with type declarations. We saw that there are interesting parallels between functions and type constructors. They are, however, two completely different things. When working on real Haskell, you usually won’t have to mess with kinds and do kind inference by hand like we did now. Usually, you just have to partially apply your own type to ** * -> *** or

**when making it an instance of one of the standard typeclasses, but it’s good to know how and why that actually works. It’s also interesting to see that types have little types of their own. Again, you don’t really have to understand everything we did here to read on, but if you understand how kinds work, chances are that you have a very solid grasp of Haskell’s type system.**

`*`

Miran 👽 rockz! 💥 Haskell a conoscerlo tutto è come Ankh-Morpork (cioè che non è stata costrita in un giorno; Piobes (*pron. piubes*) nemmeno).

🤩

## Trackback

[…] da qui, copio […]