{"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>&#8220;hydroxylic&#8221;<\/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>&#8220;hydroxylic&#8221;<\/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> &#8211; the latter is an error which is detected and flagged as quickly as possible (when the program is compiled, if not when it&#8217;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&#8217;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&#8217;s either a type itself (which can be used to declare variables) or a template type constructor, a &#8220;function&#8221; of sorts which, when given another type constructor, yields a third type constructor. C++, C# and Java programmers are familiar with these &#8220;functions&#8221; &#8211; they&#8217;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&#8217;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 &#8211; 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&#8217;t say &#8220;the type of the argument of <strong>FooCollection<\/strong>&#8221; because what it accepts isn&#8217;t a type &#8211; a type constructor can&#8217;t have a type, type is a kind of type constructor. And in fact that is exactly the word we use instead: &#8220;the kind of the argument of <strong>FooCollection<\/strong> is <strong>&lt;&gt;<\/strong>.&#8221; 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> &#8211; 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> &#8211; 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 &#8211; instead of the empty string for the kind of types, C++ uses &#8220;class&#8221; (a rather confusing overload of the word &#8211; distinct from &#8220;a structured type with default accessibility private&#8221;) or &#8220;typename&#8221; which is a bit better. Instead of <strong>&lt;&gt;<\/strong>, C++ uses &#8220;template&lt;typename&gt;&#8221;, instead of <strong>&lt;&gt;&lt;&gt;<\/strong>, C++ uses &#8220;template&lt;typename, typename&gt;&#8221; (C++ has no currying) and instead of <strong>&lt;&lt;&gt;&gt;<\/strong> C++ uses &#8220;template&lt;template&lt;typename&gt;&gt;&#8221; (a so-called &#8220;template template parameter&#8221; &#8211; one of the more obscure areas of C++).<\/p>\n<p>So we&#8217;ve gone from values to types to kinds, what comes next in the sequence? (&#8220;Sort?&#8221; 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 &#8211; 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 &#8220;fortunately&#8221; not just because it&#8217;s really confusing but because we&#8217;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&#8217;d need to use different brackets (I almost wrote &#8220;a different kind of brackets&#8221; which would further confuse things &#8211; 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&#8217;re just writing normal applications in this language you&#8217;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&#8217;s fun to think about though.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Programmers work with values like 4 and &#8220;hydroxylic&#8221;. 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 &#8220;hydroxylic&#8221;, [&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}]}}