data Ikky a b = Ikky a b
Well that would be a type Ikky that can be parameterized with two different sub types. So ...
Ikky Int Int
Ikky [Int] Float
Ikky (Ikky Int) [Int]
These are all valid instances of Ikky. Now what about this:
data Ikky a b = Ikky (a b)
Today's topic is about Kinds ... the Type of a type.
The appropriate GHC compiler directive is:
{-# LANGUAGE KindSignatures #-}
With it we can rewrite "data Ikky a b = Ikky (a b)" into:
data Ikky (a :: * -> *) b = Ikky (a b)
Let's talk about Kinds in a bit more detail.
So most types we are aware of have a Kind of *. * means that it is a normal type, so ...
Int
[Int]
Maybe Int
Are all of kind *. However, how might we specify something like ...
Maybe
Well, we can sort of think about it as a function that takes a type as a parameter and returns another type as the result. So * -> *. This can be expanded into * -> * -> * and so on and so forth. Also there's (* -> *) -> * type of kinds which are similar conceptually to functions like map ... they take a type "function" that goes from one type to another and they apply it to something, and then yield a new type. And of course there's also * -> (* -> *), but whatever, it's more or less the same as normal function types except with types as the parameters.
Although it's not exactly the same. In normal function types we see things like a -> a. Here we just have a single *. Doesn't really leave much room for parametric polymorphism on the type level. And that's because it doesn't allow parametric polymorphism on the type level. Why not? Well there's not mathematical reason why you can't do it. However for whatever reason they decided not to include polymorphic kinds or even user defined kinds in Haskell (actually I think recent GHC releases have introduced polymorphic kinds and user defined kinds ... but so far I haven't gone through the work of understanding their syntax, so let's just focus on normal kinds for now).
Okay, so data Ikky (a :: * -> *) b = Ikky (a b) would be use like ...
x = Ikky (Just 5)
And "x" would have a type like ...
x :: Ikky (Maybe Int)
I'm honestly not really sure why anyone would ever want to do that sort of thing, but I've probably just not encountered any problems that are best structured in such a manner. There are some type classes that make use of this sort of thing, so it's probably more interesting to talk about how kinds are used with type classes, but first consider the following:
x = Ikky (Left 5)
Now Left belongs to the Either type.
data Either a b = Left a | Right b
Just specifying "Left 5" let's us know that we're dealing with "Either Int b", but it doesn't tell us what the "b" is. However, that's exactly what the Ikky type is all about.
So ...
x = Ikky (Left 5)
x :: Ikky (Either Int) b
And you might say, "but what can we do with the 'b'". And the answer is nothing. We don't know what concrete type is it, but we can put it into a container, other type constructors, or return it. If that doesn't make much sense don't worry about it too much. Just keep it in mind if you ever take a look at the Functor type class and see it applied to "Either e" or something like that.
Here's some type classes.
class Jabber1 (a :: *) where
wocky1 :: a -> a
class Jabber2 (j :: * -> *) where
wocky2 :: j a -> j b
class Jabber3 (j :: * -> * -> *) where
wocky3 :: j a b -> j c d
data Ikky (a :: * -> *) = Ikky (a Int)
data Ikky2 b (a :: * -> *) = Ikky2 (a b)
data Neep a = Neep a
class Jabber4 (j :: (* -> *) -> *) where
wocky4 :: j a -> j a
instance Jabber4 Ikky where
wocky4 = undefined
x (Ikky Nothing) = undefined
x (Ikky (Just x)) = undefined
instance Jabber4 (Ikky2 x) where
wocky4 = undefined
All of that compiles. The important thing to do in order to get the hang of this is to sit down until you're confident that you get the hang of what's going on.
However, there's the gist.
class Jabber a where
wocky :: a -> a
This means that you need to hand the Jabber type class a nice first order type and the wocky function will map from that type to that type.
data Neep = A | B | C
data Blah a = Blah a
instance Jabber Neep where
wocky a = undefined
instance Jabber (Blah Int) where
wocky a = undefined
Now, then there are type classes like this:
class Jabber j where
wocky :: j a -> j b
which can be more clearly written like ...
class Jabber (j :: * -> *) where
wocky :: j a -> j b
This type class demands a higher order type. So the "data Neep = A | B | C" isn't valid any more, but the "data Blah a = Blah a" is valid as long as you leave off what type the "a" is.
instance Jabber Blah where
wocky a = undefined
This is a fundamentally different function from the earlier wocky. The first wocky was moving some type to the same type. This new higher order typed wocky is moving one type to another type, but within some other container type. And of course you can make those kind signatures really complex, so the story only get's more complicated.
So the first question might be, "why do all of this?" And the answer is probably along the lines of, "this is the type of things that mathematicians like to dream up." However, "why do this in Haskell ... it seems really complex and abstract", seems like a much more pragmatic question, and the answer is unfortunately, "when you want to do complex and abstract things." Originally, you probably could have gotten away with not thinking about this and using Haskell ... but at some point someone squinted their eyes and said, "hey Haskell sort of looks like a category", and the next thing you know there's a mountain of category theory concepts that are a core part of Haskell. There are certain Monads and Functors which I could not make sense of at all until I went through and figured out what was going on at the Kind level.
Now personally, I like the idea of kinds a lot more than sub-typing. Sub-typing is of course the thing that most programmers are familiar with ... or at least most programmers are familiar with sub-classing and basically they sometimes use it to handle situations where you want sub-typing. Unfortunately, few languages have any sort of useful kind stuff going on, so I haven't really been able to experiment with it very much. However, GHC has some sort of polymorphic kind support now, and I've gotten a renewed interest in assembly. So I can stare at what Haskell is doing with kinds to see what I think about it. Or, maybe ... I can get some sort of rudimentary programming language up and running and experiment with type systems on my own.
No comments:
Post a Comment