When are higher kinded types useful?

Question

I've been doing dev in F# for a while and I like it. However one buzzword I know doesn't exist in F# is higher-kinded types. I've read material on higher-kinded types, and I think I understand their definition. I'm just not sure why they're useful. Can someone provide some examples of what higher-kinded types make easy in Scala or Haskell, that require workarounds in F#? Also for these examples, what would the workarounds be without higher-kinded types (or vice-versa in F#)? Maybe I'm just so used to working around it that I don't notice the absence of that feature.

(I think) I get that instead of myList |> List.map f or myList |> Seq.map f |> Seq.toList higher kinded types allow you to simply write myList |> map f and it'll return a List. That's great (assuming it's correct), but seems kind of petty? (And couldn't it be done simply by allowing function overloading?) I usually convert to Seq anyway and then I can convert to whatever I want afterwards. Again, maybe I'm just too used to working around it. But is there any example where higher-kinded types really saves you either in keystrokes or in type safety?

Answer 1

So the kind of a type is its simple type. For instance Int has kind * which means it's a base type and can be instantiated by values. By some loose definition of higher-kinded type (and I'm not sure where F# draws the line, so let's just include it) polymorphic containers are a great example of a higher-kinded type.

data List a = Cons a (List a) | Nil 

The type constructor List has kind * -> * which means that it must be passed a concrete type in order to result in a concrete type: List Int can have inhabitants like [1,2,3] but List itself cannot.

I'm going to assume that the benefits of polymorphic containers are obvious, but more useful kind * -> * types exist than just the containers. For instance, the relations

data Rel a = Rel (a -> a -> Bool) 

or parsers

data Parser a = Parser (String -> [(a, String)]) 

both also have kind * -> *.

---

We can take this further in Haskell, however, by having types with even higher-order kinds. For instance we could look for a type with kind (* -> *) -> *. A simple example of this might be Shape which tries to fill a container of kind * -> *.

data Shape f = Shape (f ())  Shape [(), (), ()] :: Shape [] 

This is useful for characterizing Traversables in Haskell, for instance, as they can always be divided into their shape and contents.

split :: Traversable t => t a -> (Shape t, [a]) 

---

As another example, let's consider a tree that's parameterized on the kind of branch it has. For instance, a normal tree might be

data Tree a = Branch (Tree a) a (Tree a) | Leaf 

But we can see that the branch type contains a Pair of Tree as and so we can extract that piece out of the type parametrically

data TreeG f a = Branch a (f (TreeG f a)) | Leaf  data Pair a = Pair a a type Tree a = TreeG Pair a 

This TreeG type constructor has kind (* -> *) -> * -> *. We can use it to make interesting other variations like a RoseTree

type RoseTree a = TreeG [] a  rose :: RoseTree Int rose = Branch 3 [Branch 2 [Leaf, Leaf], Leaf, Branch 4 [Branch 4 []]] 

Or pathological ones like a MaybeTree

data Empty a = Empty type MaybeTree a = TreeG Empty a  nothing :: MaybeTree a nothing = Leaf  just :: a -> MaybeTree a just a = Branch a Empty 

Or a TreeTree

type TreeTree a = TreeG Tree a  treetree :: TreeTree Int treetree = Branch 3 (Branch Leaf (Pair Leaf Leaf)) 

---

Another place this shows up is in "algebras of functors". If we drop a few layers of abstractness this might be better considered as a fold, such as sum :: [Int] -> Int. Algebras are parameterized over the functor and the carrier. The functor has kind * -> * and the carrier kind * so altogether

data Alg f a = Alg (f a -> a) 

has kind (* -> *) -> * -> *. Alg useful because of its relation to datatypes and recursion schemes built atop them.

-- | The "single-layer of an expression" functor has kind `(* -> *)` data ExpF x = Lit Int             | Add x x             | Sub x x             | Mult x x  -- | The fixed point of a functor has kind `(* -> *) -> *` data Fix f = Fix (f (Fix f))  type Exp = Fix ExpF  exp :: Exp exp = Fix (Add (Fix (Lit 3)) (Fix (Lit 4))) -- 3 + 4  fold :: Functor f => Alg f a -> Fix f -> a fold (Alg phi) (Fix f) = phi (fmap (fold (Alg phi)) f) 

---

Finally, though they're theoretically possible, I've never see an even higher-kinded type constructor. We sometimes see functions of that type such as mask :: ((forall a. IO a -> IO a) -> IO b) -> IO b, but I think you'll have to dig into type prolog or dependently typed literature to see that level of complexity in types.