Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Kind vs Rank in type theory

I'm having a hard time understanding Higher Kind vs Higher Rank types. Kind is pretty simple (thanks Haskell literature for that) and I used to think rank is like kind when talking about types but apparently not! I read the Wikipedia article to no avail. So can someone please explain what is a Rank? and what is meant by Higher Rank? Higher Rank Polymorphism? how that comes to Kinds (if any) ? Comparing Scala and Haskell would be awesome too.

like image 238
Ashkan Kh. Nazary Avatar asked Nov 09 '12 23:11

Ashkan Kh. Nazary


1 Answers

The concept of rank is not really related to the concept of kinds.

The rank of a polymorphic type system describes where foralls may appear in types. In a rank-1 type system foralls may only appear at the outermost level, in a rank-2 type system they may appear at one level of nesting and so on.

So for example forall a. Show a => (a -> String) -> a -> String would be a rank-1 type and forall a. Show a => (forall b. Show b => b -> String) -> a -> String would be a rank-2 type. The difference between those two types is that in the first case, the first argument to the function can be any function that takes one showable argument and returns a String. So a function of type Int -> String would be a valid first argument (like a hypothetical function intToString), so would a function of type forall a. Show a => a -> String (like show). In the second case only a function of type forall a. Show a => a -> String would be a valid argument, i.e. show would be okay, but intToString wouldn't be. As a consequence the following function would be a legal function of the second type, but not the first (where ++ is supposed to represent string concatenation):

higherRankedFunction(f, x) = f("hello") ++ f(x) ++ f(42)

Note that here the function f is applied to (potentially) three different types of arguments. So if f were the function intToString this would not work.

Both Haskell and Scala are Rank-1 (so the above function can not be written in those languages) by default. But GHC contains a language extension to enable Rank-2 polymorphism and another one to enable Rank-n polymorphism for arbitrary n.

like image 147
sepp2k Avatar answered Oct 11 '22 07:10

sepp2k