fix indentation
This commit is contained in:
parent
5b550d68e7
commit
1dcf51bfaa
@ -38,10 +38,10 @@
|
||||
<p>may return <code>True</code>, <code>False</code>, or <code>_|_</code>; the latter meaning that it would never terminate.</p>
|
||||
<p>Interestingly, once you accept the bottom as part of the type system, it is convenient to treat every runtime error as a bottom, and even allow functions to return the bottom explicitly. The latter is usually done using the expression <code>undefined</code>, as in:</p>
|
||||
<pre>f :: Bool -> Bool
|
||||
f x = undefined</pre>
|
||||
f x = undefined</pre>
|
||||
<p>This definition type checks because <code>undefined</code> evaluates to bottom, which is a member of any type, including <code>Bool</code>. You can even write:</p>
|
||||
<pre>f :: Bool -> Bool
|
||||
f = undefined</pre>
|
||||
f = undefined</pre>
|
||||
<p>(without the <code>x</code>) because the bottom is also a member of the type <code>Bool->Bool</code>.</p>
|
||||
<p>Functions that may return bottom are called partial, as opposed to total functions, which return valid results for every possible argument.</p>
|
||||
<p>Because of the bottom, you’ll see the category of Haskell types and functions referred to as <strong>Hask</strong> rather than <strong>Set</strong>. From the theoretical point of view, this is the source of never-ending complications, so at this point I will use my butcher’s knife and terminate this line of reasoning. From the pragmatic point of view, it’s okay to ignore non-terminating functions and bottoms, and treat <strong>Hask</strong> as bona fide <strong>Set</strong> (see Bibliography at the end).</p>
|
||||
@ -81,31 +81,31 @@
|
||||
<pre>int f44() { return 44; }</pre>
|
||||
<p>You might think of this function as taking “nothing”, but as we’ve just seen, a function that takes “nothing” can never be called because there is no value representing “nothing.” So what does this function take? Conceptually, it takes a dummy value of which there is only one instance ever, so we don’t have to mention it explicitly. In Haskell, however, there is a symbol for this value: an empty pair of parentheses, <code>()</code>. So, by a funny coincidence (or is it a coincidence?), the call to a function of void looks the same in C++ and in Haskell. Also, because of the Haskell’s love of terseness, the same symbol <code>()</code> is used for the type, the constructor, and the only value corresponding to a singleton set. So here’s this function in Haskell:</p>
|
||||
<pre>f44 :: () -> Integer
|
||||
f44 () = 44</pre>
|
||||
f44 () = 44</pre>
|
||||
<p>The first line declares that <code>f44</code> takes the type <code>()</code>, pronounced “unit,” into the type <code>Integer</code>. The second line defines <code>f44</code> by pattern matching the only constructor for unit, namely <code>()</code>, and producing the number 44. You call this function by providing the unit value <code>()</code>:</p>
|
||||
<pre>f44 ()</pre>
|
||||
<p>Notice that every function of unit is equivalent to picking a single element from the target type (here, picking the <code>Integer</code> 44). In fact you could think of <code>f44</code> as a different representation for the number 44. This is an example of how we can replace explicit mention of elements of a set by talking about functions (arrows) instead. Functions from unit to any type A are in one-to-one correspondence with the elements of that set A.</p>
|
||||
<p>What about functions with the <code>void</code> return type, or, in Haskell, with the unit return type? In C++ such functions are used for side effects, but we know that these are not real functions in the mathematical sense of the word. A pure function that returns unit does nothing: it discards its argument.</p>
|
||||
<p>Mathematically, a function from a set A to a singleton set maps every element of A to the single element of that singleton set. For every A there is exactly one such function. Here’s this function for <code>Integer</code>:</p>
|
||||
<pre>fInt :: Integer -> ()
|
||||
fInt x = ()</pre>
|
||||
fInt x = ()</pre>
|
||||
<p>You give it any integer, and it gives you back a unit. In the spirit of terseness, Haskell lets you use the wildcard pattern, the underscore, for an argument that is discarded. This way you don’t have to invent a name for it. So the above can be rewritten as:</p>
|
||||
<pre>fInt :: Integer -> ()
|
||||
fInt _ = ()</pre>
|
||||
fInt _ = ()</pre>
|
||||
<p>Notice that the implementation of this function not only doesn’t depend on the value passed to it, but it doesn’t even depend on the type of the argument.</p>
|
||||
<p>Functions that can be implemented with the same formula for any type are called parametrically polymorphic. You can implement a whole family of such functions with one equation using a type parameter instead of a concrete type. What should we call a polymorphic function from any type to unit type? Of course we’ll call it <code>unit</code>:</p>
|
||||
<pre>unit :: a -> ()
|
||||
unit _ = ()</pre>
|
||||
unit _ = ()</pre>
|
||||
<p>In C++ you would write this function as:</p>
|
||||
<pre>template<class T>
|
||||
void unit(T) {}</pre>
|
||||
void unit(T) {}</pre>
|
||||
<p>Next in the typology of types is a two-element set. In C++ it’s called <code>bool</code> and in Haskell, predictably, <code>Bool</code>. The difference is that in C++ <code>bool</code> is a built-in type, whereas in Haskell it can be defined as follows:</p>
|
||||
<pre>data Bool = True | False</pre>
|
||||
<p>(The way to read this definition is that <code>Bool</code> is either <code>True</code> or <code>False</code>.) In principle, one should also be able to define a Boolean type in C++ as an enumeration:</p>
|
||||
<pre>enum bool {
|
||||
true,
|
||||
false
|
||||
};</pre>
|
||||
true,
|
||||
false
|
||||
};</pre>
|
||||
<p>but C++ <code>enum</code> is secretly an integer. The C++11 “<code>enum class</code>” could have been used instead, but then you would have to qualify its values with the class name, as in <code>bool::true</code> and <code>bool::false</code>, not to mention having to include the appropriate header in every file that uses it.</p>
|
||||
<p>Pure functions from <code>Bool</code> just pick two values from the target type, one corresponding to <code>True</code> and another to <code>False</code>.</p>
|
||||
<p>Functions to <code>Bool</code> are called <i>predicates</i>. For instance, the Haskell library <code>Data.Char</code> is full of predicates like <code>isAlpha</code> or <code>isDigit</code>. In C++ there is a similar library <code></code> that defines, among others, <code>isalpha</code> and <code>isdigit</code>, but these return an <code>int</code> rather than a Boolean. The actual predicates are defined in <code>std::ctype</code> and have the form <code>ctype::is(alpha, c)</code>, <code>ctype::is(digit, c)</code>, etc.</p>
|
||||
|
@ -99,13 +99,13 @@ greet = catstr “Hello “</pre>
|
||||
<pre>(a, b) -> c</pre>
|
||||
<p>It's trivial to convert between the two representations, and the two (higher-order) functions that do it are called, unsurprisingly, <code>curry</code> and <code>uncurry</code>:</p>
|
||||
<pre>curry :: ((a, b)->c) -> (a->b->c)
|
||||
curry f a b = f (a, b)</pre>
|
||||
curry f a b = f (a, b)</pre>
|
||||
<p>and</p>
|
||||
<pre>uncurry :: (a->b->c) -> ((a, b)->c)
|
||||
uncurry f (a, b) = f a b</pre>
|
||||
<p>Notice that <code>curry</code> is the <em>factorizer</em> for the universal construction of the function object. This is especially apparent if it's rewritten in this form:</p>
|
||||
<pre>factorizer :: ((a, b)->c) -> (a->(b->c))
|
||||
factorizer g = \a -> (\b -> g (a, b))</pre>
|
||||
factorizer g = \a -> (\b -> g (a, b))</pre>
|
||||
<p>(As a reminder: A factorizer produces the factorizing function from a candidate.)</p>
|
||||
<p>In non-functional languages, like C++, currying is possible but nontrivial. You can think of multi-argument functions in C++ as corresponding to Haskell functions taking tuples (although, to confuse things even more, in C++ you can define functions that take an explicit <code>std::tuple</code>, as well as variadic functions, and functions taking initializer lists).</p>
|
||||
<p>You can partially apply a C++ function using the template <code>std::bind</code>. For instance, given a function of two strings:</p>
|
||||
@ -115,8 +115,8 @@ uncurry f (a, b) = f a b</pre>
|
||||
<p>you can define a function of one string:</p>
|
||||
<pre>using namespace std::placeholders;
|
||||
|
||||
auto greet = std::bind(catstr, "Hello ", _1);
|
||||
std::cout << greet("Haskell Curry");</pre>
|
||||
auto greet = std::bind(catstr, "Hello ", _1);
|
||||
std::cout << greet("Haskell Curry");</pre>
|
||||
<p>Scala, which is more functional than C++ or Java, falls somewhere in between. If you anticipate that the function you’re defining will be partially applied, you define it with multiple argument lists:</p>
|
||||
<pre>def catstr(s1: String)(s2: String) = s1 + s2</pre>
|
||||
<p>Of course that requires some amount of foresight or prescience on the part of a library writer.</p>
|
||||
@ -202,7 +202,7 @@ eval (f, x) = f x</pre>
|
||||
<p>Finally, we come to the meaning of the <code>absurd</code> function:</p>
|
||||
<pre>absurd :: Void -> a</pre>
|
||||
<p>Considering that <code>Void</code> translates into false, we get:</p>
|
||||
<pre> false ⇒ a</pre>
|
||||
<pre>false ⇒ a</pre>
|
||||
<p>Anything follows from falsehood (<em>ex falso quodlibet</em>). Here's one possible proof (implementation) of this statement (function) in Haskell:</p>
|
||||
<pre>absurd (Void a) = absurd a</pre>
|
||||
<p>where <code>Void</code> is defined as:</p>
|
||||
|
@ -33,7 +33,7 @@
|
||||
<p>It states that an empty list <code>[]</code> is the unit element, and list concatenation <code>(++)</code> is the binary operation.</p>
|
||||
<p>As we have seen, a list of type <code>a</code> corresponds to a free monoid with the set <code>a</code> serving as generators. The set of natural numbers with multiplication is not a free monoid, because we identify lots of products. Compare for instance:</p>
|
||||
<pre>2 * 3 = 6
|
||||
[2] ++ [3] = [2, 3] // not the same as [6]</pre>
|
||||
[2] ++ [3] = [2, 3] // not the same as [6]</pre>
|
||||
<p>That was easy, but the question is, can we perform this free construction in category theory, where we are not allowed to look inside objects? We'll use our workhorse: the universal construction.</p>
|
||||
<p>The second interesting question is, can any monoid be obtained from some free monoid by identifying more than the minimum number of elements required by the laws? I'll show you that this follows directly from the universal construction.</p>
|
||||
|
||||
|
@ -44,7 +44,7 @@
|
||||
<p>We have already seen this contravariant functor in Haskell. We called it <code>Op</code>:</p>
|
||||
<pre>type Op a x = x -> a</pre>
|
||||
<pre>instance Contravariant (Op a) where
|
||||
contramap f h = h . f</pre>
|
||||
contramap f h = h . f</pre>
|
||||
<p>Finally, if we let both objects vary, we get a profunctor <code>C(-, =)</code>, which is contravariant in the first argument and covariant in the second (to underline the fact that the two arguments may vary independently, we use a double dash as the second placeholder). We have seen this profunctor before, when we talked about functoriality:</p>
|
||||
<pre>instance Profunctor (->) where
|
||||
dimap ab cd bc = cd . bc . ab
|
||||
@ -77,7 +77,7 @@
|
||||
<p>We will see later that a natural transformation from <code>C(a, -)</code> to any <b>Set</b>-valued functor always exists (Yoneda's lemma) but it is not necessarily invertible. </p>
|
||||
<p>Let me give you an example in Haskell with the list functor and <code>Int</code> as <code>a</code>. Here's a natural transformation that does the job:</p>
|
||||
<pre>alpha :: forall x. (Int -> x) -> [x]
|
||||
alpha h = map h [12]</pre>
|
||||
alpha h = map h [12]</pre>
|
||||
<p>I have arbitrarily picked the number 12 and created a singleton list with it. I can then <code>fmap</code> the function <code>h</code> over this list and get a list of the type returned by <code>h</code>. (There are actually as many such transformations as there are list of integers.) </p>
|
||||
<p>The naturality condition is equivalent to the composability of <code>map</code> (the list version of <code>fmap</code>):</p>
|
||||
<pre>map f (map h [12]) = map (f . h) [12]</pre>
|
||||
@ -86,18 +86,18 @@
|
||||
<p>You might think of retrieving an <code>x</code> from the list, e.g., using <code>head</code>, but that won't work for an empty list. Notice that there is no choice for the type <code>a</code> (in place of <code>Int</code>) that would work here. So the list functor is not representable.</p>
|
||||
<p>Remember when we talked about Haskell (endo-) functors being a little like containers? In the same vein we can think of representable functors as containers for storing memoized results of function calls (the members of hom-sets in Haskell are just functions). The representing object, the type <code>a</code> in <code>C(a, -)</code>, is thought of as the key type, with which we can access the tabulated values of a function. The transformation we called α is called <code>tabulate</code>, and its inverse, β, is called <code>index</code>. Here's a (slightly simplified) <code>Representable</code> class definition:</p>
|
||||
<pre>class Representable f where
|
||||
type Rep f :: *
|
||||
tabulate :: (Rep f -> x) -> f x
|
||||
index :: f x -> Rep f -> x</pre>
|
||||
type Rep f :: *
|
||||
tabulate :: (Rep f -> x) -> f x
|
||||
index :: f x -> Rep f -> x</pre>
|
||||
<p>Notice that the representing type, our <code>a</code>, which is called <code>Rep f</code> here, is part of the definition of <code>Representable</code>. The star just means that <code>Rep f</code> is a type (as opposed to a type constructor, or other more exotic kinds).</p>
|
||||
<p>Infinite lists, or streams, which cannot be empty, are representable. </p>
|
||||
<pre>data Stream x = Cons x (Stream x)</pre>
|
||||
<p>You can think of them as memoized values of a function taking an <code>Integer</code> as an argument. (Strictly speaking, I should be using non-negative natural numbers, but I didn't want to complicate the code.) </p>
|
||||
<p>To <code>tabulate</code> such a function, you create an infinite stream of values. Of course, this is only possible because Haskell is lazy. The values are evaluated on demand. You access the memoized values using <code>index</code>:</p>
|
||||
<pre>instance Representable Stream where
|
||||
type Rep Stream = Integer
|
||||
tabulate f = Cons (f 0) (tabulate (f . (+1)))
|
||||
index (Cons b bs) n = if n == 0 then b else index bs (n - 1)</pre>
|
||||
type Rep Stream = Integer
|
||||
tabulate f = Cons (f 0) (tabulate (f . (+1)))
|
||||
index (Cons b bs) n = if n == 0 then b else index bs (n - 1)</pre>
|
||||
<p>It's interesting that you can implement a single memoization scheme to cover a whole family of functions with arbitrary return types.</p>
|
||||
<p>Representability for contravariant functors is similarly defined, except that we keep the second argument of <code>C(-, a)</code> fixed. Or, equivalently, we may consider functors from <i>C</i><sup>op</sup> to <b>Set</b>, because <code>C<sup>op</sup>(a, -)</code> is the same as <code>C(-, a)</code>.</p>
|
||||
<p>There is an interesting twist to representability. Remember that hom-sets can internally be treated as exponential objects, in cartesian closed categories. The hom-set <code>C(a, x)</code> is equivalent to <code>x<sup>a</sup></code>, and for a representable functor <code>F</code> we can write:</p>
|
||||
|
Loading…
Reference in New Issue
Block a user