{"id":1597,"date":"2011-10-10T16:00:54","date_gmt":"2011-10-10T23:00:54","guid":{"rendered":"https:\/\/www.reenigne.org\/blog\/?p=1597"},"modified":"2012-08-23T00:54:03","modified_gmt":"2012-08-23T07:54:03","slug":"templates-and-kinds-in-alfe","status":"publish","type":"post","link":"https:\/\/www.reenigne.org\/blog\/templates-and-kinds-in-alfe\/","title":{"rendered":"Templates and Kinds in ALFE"},"content":{"rendered":"<p>Programmers work with values like <strong>4<\/strong> and <strong>\"hydroxylic\"<\/strong>. We also generally work with variables like <strong>count<\/strong> and <strong>acid<\/strong>. Each variable holds precisely one value. But in many languages, not every variable can hold any value. In a statically typed language, <strong>count<\/strong> might be able to hold <strong>4<\/strong> and <strong>acid<\/strong> might be able to hold <strong>\"hydroxylic\"<\/strong>, but not the other way around. That quality of variables and values that determines which objects can fit into which boxes is called type. So <strong>count<\/strong> might have a type of <strong>Integer<\/strong> and <strong>acid<\/strong> might have a type of <strong>String<\/strong>. Then if you have a function called <strong>square<\/strong> which multiplies its argument by itself and returns the result, it makes sense to say <strong>square(count)<\/strong> but not to say <strong>square(acid)<\/strong> - the latter is an error which is detected and flagged as quickly as possible (when the program is compiled, if not when it's typed in in the first place). On this blog, as a notational convention, types (and more generally type constructors, see below) start with a capital letter and variables and values don't. I think this is a useful convention, and some languages (<a href=\"https:\/\/www.reenigne.org\/blog\/cases\">including the language I am writing<\/a>) enforce it.<\/p>\n<p>A type constructor is a generalization of a type. It's either a type itself (which can be used to declare variables) or a template type constructor, a \"function\" of sorts which, when given another type constructor, yields a third type constructor. C++, C# and Java programmers are familiar with these \"functions\" - they're called templates or generics. A good example of a template type constructor is <strong>Array<\/strong>. You give it a type like <strong>String<\/strong> and you get back <strong>Array&lt;String&gt;<\/strong> (i.e. an array of strings). You can also have <strong>Array&lt;Array&lt;String&gt;&gt;<\/strong> if you're feeling adventurous. A type constructor can have multiple arguments, so you might have <strong>Pair&lt;Integer, String&gt;<\/strong> which (through the magic of something called <a href=\"http:\/\/en.wikipedia.org\/wiki\/Currying\">currying<\/a>) is the same thing as <strong>Pair&lt;Integer&gt;&lt;String&gt;<\/strong>.<\/p>\n<p>What if you have a template type constructor with a parameter that is not a type but is itself a template type constructor? Well, you can do that too - say you have a type constructor called <strong>FooCollection<\/strong> and you pass it <strong>Array<\/strong> (note, not <strong>Array&lt;Integer&gt;<\/strong> or <strong>Array&lt;String&gt;<\/strong>, which are types, just plain <strong>Array<\/strong>) and you get back <strong>FooCollection&lt;Array&gt;<\/strong> which might be implemented in terms of <strong>Array&lt;Foo&gt;<\/strong>. Similarly, <strong>FooCollection&lt;List&gt;<\/strong> might be implemented in terms of <strong>List&lt;Foo&gt;<\/strong>.<\/p>\n<p>So if the type of the argument of <strong>square<\/strong> is <strong>Integer<\/strong>, how do we talk about the argument of <strong>FooCollection<\/strong>. We can't say \"the type of the argument of <strong>FooCollection<\/strong>\" because what it accepts isn't a type - a type constructor can't have a type, type is a kind of type constructor. And in fact that is exactly the word we use instead: \"the kind of the argument of <strong>FooCollection<\/strong> is <strong>&lt;&gt;<\/strong>.\" Other examples of kinds are (nothing, i.e. the empty string) which is the kind of types like <strong>Integer<\/strong> and <strong>String<\/strong> (no angle brackets follow them), <strong>&lt;&gt;&lt;&gt;<\/strong> aka <strong>&lt;,&gt;<\/strong> (which is the kind of <strong>Pair<\/strong> - i.e. you need to give it two types to get back a type) and <strong>&lt;&lt;&gt;&gt;<\/strong> (which is the kind of <strong>FooCollection<\/strong> - i.e. you need to give it a type constructor of kind <strong>&lt;&gt;<\/strong> to get back a type). The <a href=\"http:\/\/en.wikipedia.org\/wiki\/Kind_(type_theory)\">wikipedia article on kinds<\/a> uses a different notation further removed from the C++-inspired one I use here, but the two are equivalent and the transformation from one to the other is purely mechanical.<\/p>\n<p>Incidentally, you can refer to kinds in C++ as well - instead of the empty string for the kind of types, C++ uses \"class\" (a rather confusing overload of the word - distinct from \"a structured type with default accessibility private\") or \"typename\" which is a bit better. Instead of <strong>&lt;&gt;<\/strong>, C++ uses \"template&lt;typename&gt;\", instead of <strong>&lt;&gt;&lt;&gt;<\/strong>, C++ uses \"template&lt;typename, typename&gt;\" (C++ has no currying) and instead of <strong>&lt;&lt;&gt;&gt;<\/strong> C++ uses \"template&lt;template&lt;typename&gt;&gt;\" (a so-called \"template template parameter\" - one of the more obscure areas of C++).<\/p>\n<p>So we've gone from values to types to kinds, what comes next in the sequence? (\"Sort?\" that already has another meaning in computer science though.) Suppose you had a function which accepts a kind and returns another kind. My angle brackets here have that effect - they take a list of kinds and return a kind which is the kind of a type constructor that accepts type constructors of the listed kinds and returns a type. What a confusing sentence! Fortunately nobody to my knowledge has found a non-trivial use for anything one level up from kind. I say \"fortunately\" not just because it's really confusing but because we've run out of notation! If you start with a lower case letter to signify a value argument and an upper case letter to signify a type constructor argument, how do you signify a kind argument? Also, if we'd need to use different brackets (I almost wrote \"a different kind of brackets\" which would further confuse things - writing about this stuff is hard!) to distinguish kind functions from value functions and type constructor functions, and all the ASCII brackets already have other meanings in my language.<\/p>\n<p>Anyway, this is the sort of thing that you bump your head against when you write compilers for languages which support templates. Fortunately, if you're just writing normal applications in this language you'll probably never need to be concerned with it. Until you do. At which point just doing the most obvious thing should work fine without any fuss. I think it's fun to think about though.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Programmers work with values like 4 and \"hydroxylic\". We also generally work with variables like count and acid. Each variable holds precisely one value. But in many languages, not every variable can hold any value. In a statically typed language, count might be able to hold 4 and acid might be able to hold \"hydroxylic\", [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[27],"tags":[],"class_list":["post-1597","post","type-post","status-publish","format-standard","hentry","category-language"],"_links":{"self":[{"href":"https:\/\/www.reenigne.org\/blog\/wp-json\/wp\/v2\/posts\/1597","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.reenigne.org\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.reenigne.org\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.reenigne.org\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.reenigne.org\/blog\/wp-json\/wp\/v2\/comments?post=1597"}],"version-history":[{"count":10,"href":"https:\/\/www.reenigne.org\/blog\/wp-json\/wp\/v2\/posts\/1597\/revisions"}],"predecessor-version":[{"id":1599,"href":"https:\/\/www.reenigne.org\/blog\/wp-json\/wp\/v2\/posts\/1597\/revisions\/1599"}],"wp:attachment":[{"href":"https:\/\/www.reenigne.org\/blog\/wp-json\/wp\/v2\/media?parent=1597"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.reenigne.org\/blog\/wp-json\/wp\/v2\/categories?post=1597"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.reenigne.org\/blog\/wp-json\/wp\/v2\/tags?post=1597"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}