Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
branch: master
Fetching contributors…

Cannot retrieve contributors at this time

1197 lines (1122 sloc) 191.346 kb
<!DOCTYPE html>
<!--[if IEMobile 7 ]><html class="no-js iem7"><![endif]-->
<!--[if lt IE 9]><html class="no-js lte-ie8"><![endif]-->
<!--[if (gt IE 8)|(gt IEMobile 7)|!(IEMobile)|!(IE)]><!--><html class="no-js" lang="en"><!--<![endif]-->
<head>
<meta charset="utf-8">
<title>Paolo Capriotti's blog</title>
<meta name="author" content="Paolo Capriotti">
<meta name="HandheldFriendly" content="True">
<meta name="MobileOptimized" content="320">
<meta name="viewport" content="width=device-width, initial-scale=1">
<link rel="canonical" href="http://paolocapriotti.com/index.html">
<link href="/css/screen.css" media="screen, projection" rel="stylesheet" type="text/css">
<link href="/css/agda.css" rel="stylesheet" type="text/css">
<script src="/js/modernizr-2.0.js"></script>
<script src="/js/ender.js"></script>
<script src="/js/octopress.js" type="text/javascript"></script>
<script type="text/javascript" src="http://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML,http://paolocapriotti.com/js/mathjax_config.js"></script>
<link href="/atom.xml" rel="alternate" title="Paolo Capriotti's blog" type="application/atom+xml">
<!--Fonts from Google"s Web font directory at http://google.com/webfonts -->
<link href="http://fonts.googleapis.com/css?family=PT+Serif:regular,italic,bold,bolditalic" rel="stylesheet" type="text/css">
<link href="http://fonts.googleapis.com/css?family=PT+Sans:regular,italic,bold,bolditalic" rel="stylesheet" type="text/css">
<script type="text/javascript">
var _gaq = _gaq || [];
_gaq.push(['_setAccount', 'UA-31066956-1']);
_gaq.push(['_trackPageview']);
(function() {
var ga = document.createElement('script'); ga.type = 'text/javascript'; ga.async = true;
ga.src = ('https:' == document.location.protocol ? 'https://ssl' : 'http://www') + '.google-analytics.com/ga.js';
var s = document.getElementsByTagName('script')[0]; s.parentNode.insertBefore(ga, s);
})();
</script>
</head>
<body>
<header role="banner"><hgroup>
<h1><a href="/">Paolo Capriotti's blog</a></h1>
<h2>Functional programming and more</h2>
</hgroup>
</header>
<nav role="navigation"><ul class="subscription" data-subscription="rss">
<li><a href="/atom.xml" rel="subscribe-rss" title="subscribe via RSS">RSS</a></li>
</ul>
<form action="http://google.com/search" method="get">
<fieldset role="search">
<input type="hidden" name="q" value="site:http://paolocapriotti.com" />
<input class="search" type="text" name="q" results="0" placeholder="Search" />
</fieldset>
</form>
<ul class="main-navigation">
<li><a href="/">Blog</a></li>
<li><a href="/blog/archives">Archives</a></li>
<li><a href="/about">About</a></li>
</ul>
</nav>
<div id="main">
<div id="content">
<div class="blog-index">
<article>
<header>
<h1 class="entry-title"><a href="/blog/2013/12/16/free-monads-part-3/">Free monads in category theory (part 3)</a></h1>
<p class="meta">
<time datetime="2013-12-16" pubdate>Dec 16<span>th</span>, 2013</time>
</p>
</header>
<div class="entry-content">
<h2 id="introduction">Introduction</h2>
<p>In the previous post, we investigated free monads, i.e. those whose monad algebras are the same as algebras of some functor. In general, however, not all monads are free, not even in Haskell! Nevertheless, monad algebras can often be regarded as algebras of some functor, satisfying certain “algebraic laws”.</p>
<p>In the first post of the series, we looked at the list monad <span class="math">\(L\)</span>. We observed that monad algebras of <span class="math">\(L\)</span> can be regarded as monoids, which is to say they are algebras of the functor <span class="math">\(F\)</span> given by <span class="math">\(F X = 1 + X²\)</span>, subject to unit and associativity laws.</p>
<p>The list example is interesting, because it suggests a strong connection between monads and algebraic structures. Can we always regard algebraic structures (such as groups, rings, vector spaces, etc…) as the algebras of some monad?</p>
<p>In this post, we will try to generalise this example to other monads by developing a categorical definition of <em>algebraic theory</em> based on monads and monad algebras.</p>
<h2 id="algebraic-theories">Algebraic theories</h2>
<p>The theory of monoids is a particular instance of a general pattern that occurs over and over in mathematics. We have a set of operations, each with a specified arity, and a set of laws that these operations are required to satisfy. The laws all have the form of equations with universally quantified variables.</p>
<p>For monoids, we have two operations: a unit <span class="math">\(e\)</span>, which is a nullary operation (i.e. a constant), and multiplication <span class="math">\(·\)</span>, a binary operation (written infix). The laws should be very familiar: <span class="math">\[
\begin{aligned}
e · x &amp; = x \\
x · e &amp; = x \\
x · (y · z) &amp; = (x · y) · z
\end{aligned}
\]</span> where every free variable is implicitly considered to be universally quantified.</p>
<p>As we observed in the first post of this series, the functor <span class="math">\(F\)</span> corresponding to the algebraic theory of monoids is given by <span class="math">\(F X = 1 + X²\)</span>. Algebras of <span class="math">\(F\)</span> are sets equipped with the operations of a monoid, but there is no requirement that they satisfy the laws.</p>
<p>Since <span class="math">\(F\)</span> is polynomial, it has an algebraically free monad <span class="math">\(F^*\)</span>, so <span class="math">\(F^* X\)</span> is in particular an <span class="math">\(F\)</span>-algebra. If we focus on the first law above, we see that it just consists of a pair of terms in <span class="math">\(F^* X\)</span>, parameterised over some unspecified element <span class="math">\(x : X\)</span>. This can be expressed as a natural transformation: <span class="math">\[
X → F^*X × F^* X
\]</span> The same holds for the second law, while the third can be regarded as a function: <span class="math">\[
X³ → F^*X × F^*X
\]</span></p>
<p>We can assemble those three functions into a single datum, consisting of a pair of natural transformations: <span class="math">\[
X + X + X³ ⇉ F^* X
\]</span></p>
<p>If we set <span class="math">\(G X = X + X + X³\)</span>, we have that the laws can be summed up concisely by giving a pair of natural transformations: <span class="math">\[
G ⇉ F^*,
\]</span> which, since algebraically free monads are free, is the same as a parallel pair of monad morphisms: <span class="math">\[
l, r : G^* ⇉ F^*,
\]</span> and this is something that we can easily generalise. Namely, we say that an <em>algebraic theory</em> is a parallel pair of morphisms of algebraically free monads.</p>
<p>Note that the terminology here is a bit fuzzy. Some authors might refer to the parallel pair above as a <em>presentation</em> of an algebraic theory. It ultimately depends on whether or not you want to consider theories with different syntactical presentations but identical models to be equal. With our definition, they would be considered different.</p>
<h2 id="models">Models</h2>
<p>To really motivate this definition, we now need to explain what the models of an algebraic theory are. This is quite easy if we just follow our derivation of the general definition from the example.</p>
<p>We know that a monoid is an <span class="math">\(F\)</span>-algebra <span class="math">\(θ : F X → X\)</span> that satisfies the monoid laws. Since <span class="math">\(F\)</span>-algebras are the same as <span class="math">\(F^*\)</span>-algebras, we can work with the corresponding <span class="math">\(F^*\)</span>-algebra instead, which we denote by <span class="math">\(θ^* : F^*X → X\)</span>.</p>
<p>This algebra satisfies the laws exactly when the two natural transformations above become equal when composed with <span class="math">\(θ^*\)</span>, i.e. when <span class="math">\(θ^* ∘ l = θ^* ∘ r\)</span>.</p>
<p>We thus define the category of models of an algebraic theory <span class="math">\(l, r : G^* ⇉ F^*\)</span> as the full subcategory of <span class="math">\(\cat{Alg}_F ≅ \cat{mAlg}_{F^*}\)</span> consisting of all those monad algebras <span class="math">\(θ^* : F^* X → X\)</span> such that <span class="math">\(θ^* ∘ l = θ^* ∘ r\)</span>.</p>
<p>Now, we know that, in the case of monoids, this subcategory is monadic over <span class="math">\(\set\)</span>, but is this true in general?</p>
<p>We begin by defining the notion of a <em>free model</em> for some algebraic theory. In the monoid example, we used the list monad to build a monoid out of any set, and then proceeded to prove that this construction gives the left adjoint of the forgetful functor <span class="math">\(\cat{Alg}_F → \set\)</span>. This is of course the first step towards proving monadicity.</p>
<p>In general, there does not seem to be a way to generalise this construction directly. We pulled the list monad out of a hat, and showed that it was exactly the monad that we were looking for. We did not derive it using the functor <span class="math">\(F\)</span> in a systematic way that we could replicate in the general case.</p>
<p>Fortunately, there is another way to produce the free monoid over a set <span class="math">\(X\)</span>. We start with the free <span class="math">\(F\)</span>-algebra <span class="math">\(F^* X\)</span>, then <em>quotient</em> it according to the laws. Intuitively, we define an equivalence relation that relates two elements <span class="math">\(t₁\)</span> and <span class="math">\(t₂\)</span> whenever there is a law that requires them to be equal.</p>
<p>The straightforward way to formalise this intuition is to take the equivalence relation generated by such pairs <span class="math">\((t₁, t₂)\)</span>, then take the corresponding quotient. A more conceptual approach is to say that <span class="math">\(T X\)</span> is obtained as a coequaliser: <span class="math">\[
G^* X ⇉ F^* X → T X.
\]</span></p>
<p>In the monoid example, <span class="math">\(F^* X\)</span> is the set of all trees with leaves labelled by elements of <span class="math">\(X\)</span>. If we regard a tree as a parenthesised string of elements of <span class="math">\(X\)</span>, then the equivalence relation on <span class="math">\(F^*\)</span> given by the coequaliser above corresponds to identifying strings with the same underlying <em>list</em> of elements but possibly different parenthesizations. Therefore, <span class="math">\(T X\)</span> is clearly isomorphic to the list monad.</p>
<h2 id="conclusion">Conclusion</h2>
<p>More generally, we can take any algebraic theory, which we defined as a parallel pair of monad morphisms between free monads <span class="math">\(F^*\)</span> and <span class="math">\(G^*\)</span>, and take the coequaliser in the category of (finitary) monads.</p>
<p>With some reasonable assumptions on the functors <span class="math">\(F\)</span> and <span class="math">\(G\)</span>, we can show that this coequaliser always exists, and that the algebras of the resulting monad are exactly the models of the algebraic theory we started with.</p>
<h2 id="further-reading">Further reading</h2>
<p>This concludes my series on the underlying theory of free monads and their relation with universal algebra.</p>
<p>Here is a list of resources where you can learn more about this topic:</p>
<h4 id="michael-barr-and-charles-wells-toposes-triples-and-theories">Michael Barr and Charles Wells, Toposes, Triples and Theories</h4>
<p>“Triple” is the old term for monads. Chapter 3 is about the monadicity theorem and some of the material that I covered in this series.</p>
<h4 id="saunders-mac-lane-categories-for-the-working-mathematician">Saunders Mac Lane, Categories for the Working Mathematician</h4>
<p>Chapter 6 is about monads and their algebras.</p>
<h4 id="steve-awodey-category-theory">Steve Awodey, Category Theory</h4>
<p>The last chapter explains the relationship between initial algebras and monadic functors.</p>
<h4 id="francis-borceux-handbook-of-categorical-algebra">Francis Borceux, Handbook of Categorical Algebra</h4>
<p>A very comprehensive resource, with detailed proofs.</p>
</div>
</article>
<article>
<header>
<h1 class="entry-title"><a href="/blog/2013/12/04/free-monads-part-2/">Free monads in category theory (part 2)</a></h1>
<p class="meta">
<time datetime="2013-12-04" pubdate>Dec 4<span>th</span>, 2013</time>
</p>
</header>
<div class="entry-content">
<h2 id="introduction">Introduction</h2>
<p>In the <a href="http://paolocapriotti.com/blog/2013/11/20/free-monads-part-1/">previous post</a>, I introduced the notion of <em>monadic functor</em>, exemplified by the forgetful functor from the category of monoids to <span class="math">\(\set\)</span>. We saw that monoids form a subcategory of the category of algebras of the functor <span class="math">\(F\)</span> defined by <span class="math">\(F X = 1 + X²\)</span>, and we observed that those are the same as the monad algebras of the list monad.</p>
<h2 id="algebraically-free-monads">Algebraically free monads</h2>
<p>More generally, we can try different subcategories of <span class="math">\(\cat{Alg}_F\)</span> and check whether they are monadic as well. So let’s start with possibly the simplest one: the whole of <span class="math">\(\cat{Alg}_F\)</span>.</p>
<p>This leads us to the following definition: we say that an endofunctor <span class="math">\(F\)</span> <em>admits an algebraically free monad</em> if <span class="math">\(\cat{Alg}_F\)</span> is monadic. The corresponding monad is called the <em>algebraically free monad</em> over <span class="math">\(F\)</span>.</p>
<p>Informally, the algebraically free monad over <span class="math">\(F\)</span> is a monad <span class="math">\(T\)</span> such that monad algebras of <span class="math">\(T\)</span> are the same as functor algebras of <span class="math">\(F\)</span>.</p>
<p>Unfortunately, not all functors admit an algebraically free monad. For example, it is easy to see that the powerset functor does not.</p>
<h2 id="free-monads-as-initial-algebras">Free monads as initial algebras</h2>
<p>The <a href="http://hackage.haskell.org/package/free-4.2/docs/Control-Monad-Free.html">free</a> package on Hackage defines something called “free monad” for every Haskell functor. What does this have to do with the notion of algebraically free monad defined above?</p>
<p>Here is the definition of <code>Free</code> from the above package:</p>
<pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="kw">data</span> <span class="dt">Free</span> f a
<span class="fu">=</span> <span class="dt">Pure</span> a
<span class="fu">|</span> <span class="dt">Free</span> (f (<span class="dt">Free</span> f a))</code></pre>
<p>Translating into categorical language, we can define, for an endofunctor <span class="math">\(F\)</span>, the functor <span class="math">\(F^*\)</span>, which returns, for a set <span class="math">\(X\)</span>, a fixpoint of the functor <span class="math">\[
G Y = X + F Y.
\]</span></p>
<p>Let’s assume that the fixpoint is to be intended as inductive, i.e. as an initial algebra. Therefore, we get, for all objects <span class="math">\(X\)</span>, an initial algebra: <span class="math">\[
X + F (F^* X) → F^* X.
\]</span></p>
<p>Of course, those initial algebras might not exist, but they do if we choose <span class="math">\(F\)</span> carefully. For example, if <span class="math">\(F\)</span> is polynomial, then all the functors <span class="math">\(G\)</span> above are also polynomial, thus they have initial algebras.</p>
<p>In general, if we assume that those initial algebras all exist, then we can prove that the resulting functor <span class="math">\(F^*\)</span> is a monad, and is indeed the algebraically free monad over <span class="math">\(F\)</span>.</p>
<p>We will first show that <span class="math">\(F^*\)</span> allows us to define a left adjoint <span class="math">\(L\)</span> for the forgetful functor <span class="math">\(U : \cat{Alg}_F → \set\)</span>. In fact, for any set <span class="math">\(X\)</span>, let the carrier of <span class="math">\(L X\)</span> be <span class="math">\(F^* X\)</span>, and define the algebra morphism by restriction from the initial algebra structure on <span class="math">\(F^* X\)</span>: <span class="math">\[
F (F^* X) → X + F (F^* X) → F^* X.
\]</span></p>
<p>By definition, <span class="math">\(F^* X\)</span> is the initial object in the category of algebras of the functor <span class="math">\(Y ↦ X + F Y\)</span>. Moreover, it is easy to see that the latter category is equivalent to the comma category <span class="math">\((X ↓ U)\)</span>, where the equivalence maps <span class="math">\(F^* X\)</span> to the obvious morphism <span class="math">\(X → U L X\)</span>. By the <a href="http://ncatlab.org/nlab/show/adjoint+functor#UniversalArrows">characterisation of adjunctions in terms of universal arrows</a>, it follows that <span class="math">\(L\)</span> is left adjoint to <span class="math">\(U\)</span>. Clearly, <span class="math">\(U L = F^*\)</span>, therefore <span class="math">\(F^*\)</span> is a monad.</p>
<p>To conclude the proof, we need to show that the adjunction <span class="math">\(L ⊣ U\)</span> is monadic, i.e. that the comparison functor from <span class="math">\(F\)</span>-algebras to <span class="math">\(F^*\)</span>-algebras is an equivalence. One way to do that is to appeal to <a href="http://en.wikipedia.org/wiki/Beck%27s_monadicity_theorem">Beck’s monadicity theorem</a>. Verifying the hypotheses is a simple exercise.</p>
<p>It is also instructive to look at the comparison functor as implemented in haskell:</p>
<pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="ot">iter ::</span> <span class="dt">Functor</span> f <span class="ot">=&gt;</span> (f x <span class="ot">→</span> x) <span class="ot">→</span> (<span class="dt">Free</span> f x <span class="ot">→</span> x)
iter θ (<span class="dt">Pure</span> x) <span class="fu">=</span> x
iter θ (<span class="dt">Free</span> t) <span class="fu">=</span> θ (fmap (iter θ) t)</code></pre>
<p>and its inverse</p>
<pre class="sourceCode haskell"><code class="sourceCode haskell">uniter <span class="fu">:</span> <span class="dt">Functor</span> f <span class="ot">=&gt;</span> (<span class="dt">Free</span> f x <span class="ot">→</span> x) <span class="ot">→</span> (f x <span class="ot">→</span> x)
uniter ψ <span class="fu">=</span> ψ <span class="fu">.</span> liftF
<span class="kw">where</span> liftF <span class="fu">=</span> <span class="dt">Free</span> <span class="fu">.</span> fmap <span class="dt">Pure</span></code></pre>
<p>It is not hard to prove directly, using equational reasoning, that <code>iter θ</code> is a monad algebra, and that <code>iter</code> and <code>uniter</code> are inverses to each other.</p>
<h2 id="algebraically-free-monads-are-free">Algebraically free monads are free</h2>
<p>The documentation for <code>Free</code> says:</p>
<blockquote>
<p>A Monad <code>n</code> is a free Monad for <code>f</code> if every monad homomorphism from <code>n</code> to another monad <code>m</code> is equivalent to a natural transformation from <code>f</code> to <code>m</code></p>
</blockquote>
<p>which doesn’t look at all like our definition of algebraically free monad. Rather, this says that <span class="math">\(N\)</span> is defined to be the <em>free monad</em> over <span class="math">\(F\)</span> if the canonical natural transformation <span class="math">\(F → N\)</span> is a universal arrow from <span class="math">\(F\)</span> to the forgetful functor <span class="math">\(\cat{Mon}(\set) → \cat{Func}(\set, \set)\)</span>.</p>
<p>If that forgetful functor had a left adjoint, then we could just say that the free monad is obtained by applying this left adjoint to any endofunctor. This is actually the case if we replace <span class="math">\(\set\)</span> with a so-called <em>algebraically complete category</em>, such as the ones modelled by Haskell, where the left adjoint is given by the (higher order) functor <code>Free</code>.</p>
<p>In <span class="math">\(\set\)</span>, however, we need to stick to the more awkward definition in terms of universal arrows, as not all functors are going to admit free monads. In any case, the relationship with the previously defined notion of algebraically free monad is not immediately clear.</p>
<p>Fortunately, we can prove that a monad is algebraically free if and only if it is free! Proving that an algebraically free monad <span class="math">\(F^*\)</span> on <span class="math">\(F\)</span> is free amounts to proving that the following natural transformation (corresponding to <code>liftF</code> in the Haskell code above): <span class="math">\[
\require{AMScd}
\begin{CD}
F X @&gt;{F η}&gt;&gt; F (F^* X) @&gt;&gt;&gt; F^* X
\end{CD}
\]</span> is universal, which is a simple exercise.</p>
<p>To prove the converse, we will be using Haskell notation. Suppose given a functor <code>f</code>, and a monad <code>t</code> that is free on <code>f</code>. Therefore, we have a natural transformation:</p>
<pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="ot">l ::</span> f x <span class="ot">→</span> t x</code></pre>
<p>and a function that implements the universal property for <code>t</code>:</p>
<pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="ot">hoist ::</span> <span class="dt">Monad</span> m <span class="ot">=&gt;</span> (<span class="ot">∀</span> x <span class="fu">.</span> f x <span class="ot">→</span> m x) <span class="ot">→</span> t x <span class="ot">→</span> m x</code></pre>
<p>Now we define a functor <span class="math">\(\set → \cat{Alg}_f\)</span> which is going to be the left adjoint of the forgetful functor. The carrier of this functor is given by <code>t</code> itself, so we only need to define the algebra morphism:</p>
<pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="ot">alg ::</span> f (t x) <span class="ot">→</span> t x
alg u <span class="fu">=</span> join (l u)</code></pre>
<p>To show that this functor is the sought left adjoint, we have to fix a type <code>x</code> and an <code>f</code>-algebra <code>θ : f y → y</code>, define functions:</p>
<pre class="sourceCode haskell"><code class="sourceCode haskell">φ<span class="ot"> ::</span> (x <span class="ot">→</span> y) <span class="ot">→</span> (t x <span class="ot">→</span> y)
ψ<span class="ot"> ::</span> (t x <span class="ot">→</span> y) <span class="ot">→</span> (x <span class="ot">→</span> y)</code></pre>
<p>then prove that <code>φ g</code> is an <code>f</code>-algebra morphism for all <code>g : x → y</code>, and that <code>φ</code> and <code>ψ</code> are inverses to each other.</p>
<p>The function <code>ψ</code> is easy to implement:</p>
<pre class="sourceCode haskell"><code class="sourceCode haskell">ψ a h <span class="fu">=</span> h <span class="fu">.</span> return</code></pre>
<p>Defining <code>φ</code> is a bit more involved. The only tool at our disposal to define functions out of <code>t x</code> is <code>hoist</code>. For that, we need a monad <code>m</code>, and a natural transformation <code>f → m</code>.</p>
<p>The trick is to consider the <em>continuation monad</em> <code>Cont y</code>. Using <code>θ</code>, we define a natural transformation</p>
<pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="ot">w ::</span> f z <span class="ot">→</span> <span class="dt">Cont</span> y z
w u <span class="fu">=</span> <span class="dt">Cont</span> (\k <span class="ot">-&gt;</span> θ (fmap k u))</code></pre>
<p>on which we can apply the universal property of <code>t</code> to get <code>φ</code>:</p>
<pre class="sourceCode haskell"><code class="sourceCode haskell">φ g <span class="fu">=</span> (<span class="ot">`runCont`</span> id) <span class="fu">.</span> hoist w <span class="fu">.</span> fmap g</code></pre>
<p>From here, the proof proceeds by straightforward equational reasoning, and is left as an exercise.</p>
<h2 id="conclusion">Conclusion</h2>
<p>We looked at two definitions of “free monad”, proved that they are equivalent, and shown the relationship with the Haskell definition of <code>Free</code>. In the next post, we will resume our discussion of algebraic theories “with laws” and try to approach them from the point of view of free monads and monadic functors.</p>
</div>
</article>
<article>
<header>
<h1 class="entry-title"><a href="/blog/2013/11/20/free-monads-part-1/">Free monads in category theory (part 1)</a></h1>
<p class="meta">
<time datetime="2013-11-20" pubdate>Nov 20<span>th</span>, 2013</time>
</p>
</header>
<div class="entry-content">
<h2 id="introduction">Introduction</h2>
<p>Free monads can be used in Haskell for modelling a number of different concepts: trees with arbitrary branching, terms with free variables, or program fragments of an EDSL.</p>
<p>This series of posts is <em>not</em> an introduction to free monads in Haskell, but to the underlying theory. In the following, we will work in the category <span class="math">\(\set\)</span> of sets and functions. However, most of what we say can be trivially generalised to an arbitrary category.</p>
<h2 id="algebras-of-a-functor">Algebras of a functor</h2>
<p>If <span class="math">\(F\)</span> is an endofunctor on <span class="math">\(\set\)</span>, an <strong>algebra</strong> of <span class="math">\(F\)</span> is a set <span class="math">\(X\)</span> (called its <em>carrier</em>), together with a morphism <span class="math">\(FX → X\)</span>. Algebras of <span class="math">\(F\)</span> form a category, where morphisms are functions of their respective carriers that make the obvious square commute.</p>
<p>Bartosz Milewski wrote a nice introductory <a href="https://www.fpcomplete.com/user/bartosz/understanding-algebras">post on functor algebras</a> from the point of view of functional programming, which I strongly recommend reading to get a feel for why it is useful to consider such objects.</p>
<p>More abstractly, a functor <span class="math">\(F : \set → \set\)</span> generalises the notion of a <em>signature</em> of an algebraic theory. For a signature with <span class="math">\(a_i\)</span> operators of arity <span class="math">\(i\)</span>, for <span class="math">\(i = 0, \ldots, n\)</span>, the corresponding functor is the polynomial: <span class="math">\[
F X = a₀ + a₁ × X + ⋯ + a_n × X^n,
\]</span> where the natural number <span class="math">\(a_i\)</span> denotes a finite set of cardinality <span class="math">\(a_i\)</span>.</p>
<p>For example, the theory of monoids has 1 nullary operation, and 1 binary operation. That results in the functor: <span class="math">\[
F X = 1 + X^2
\]</span></p>
<p>Suppose that <span class="math">\((X, θ)\)</span> is an algebra for this particular functor. That is, <span class="math">\(X\)</span> is a set, and <span class="math">\(θ\)</span> is a function <span class="math">\(1 + X² → X\)</span>. We can split <span class="math">\(θ\)</span> into its two components: <span class="math">\[
θ_e : 1 → X,
\]</span> which we can simply think of as an element of <span class="math">\(X\)</span>, and <span class="math">\[
θ_m : X × X → X.
\]</span></p>
<p>So we see that an algebra for <span class="math">\(F\)</span> is exactly a set, together with the operations of a monoid. However, there is nothing that tells us that <span class="math">\(X\)</span> is indeed a monoid with those operations!</p>
<p>In fact, for <span class="math">\(X\)</span> to be a monoid, the operations above need to satisfy the following laws: <span class="math">\[
\begin{aligned}
&amp; θ_m (θ_e(∗), x) = x \\
&amp; θ_m (x, θ_e(∗)) = x \\
&amp; θ_m (θ_m (x, y), z) = θ_m (x, θ_m (y, z)).
\end{aligned}
\]</span></p>
<p>However, any two operations <span class="math">\(θ_e\)</span> and <span class="math">\(θ_m\)</span> with the above types can be assembled into an <span class="math">\(F\)</span>-algebra, regardless of whether they do satisfy the monoid laws or not.</p>
<h2 id="lawful-algebras">“Lawful” algebras</h2>
<p>The above example shows that functor algebras don’t quite capture the general notion of “algebraic structure” in the usual sense. They can express the idea of a set equipped with operations complying to a given signature, but we cannot enforce any sort of <em>laws</em> on those operations.</p>
<p>For the monoid example above, we noticed that we can realise any actual monoid as an <span class="math">\(F\)</span>-algebra (for <span class="math">\(FX = 1 + X²\)</span>), but that not every such algebra is a monoid. This means that monoids can be regarded as the objects of the subcategory of <span class="math">\(\cat{Alg}_F\)</span> consisting of the “lawful” algebras (exercise: make this statement precise and prove it).</p>
<p>Therefore, we have the following commutative diagram of functors: <span class="math">\[
\require{AMScd}
\begin{CD}
\mathsf{Mon} @&gt;&gt;&gt; \mathsf{Alg}_F\\
@VUVV @VVV\\
\mathsf{Set} @&gt;=&gt;&gt; \mathsf{Set}
\end{CD}
\]</span></p>
<p>and it is easy to see that <span class="math">\(U\)</span> (which is just the restriction of the obvious forgetful functor <span class="math">\(\cat{Alg}_F → \set\)</span> on the right side of the diagram) has a left adjoint <span class="math">\(L\)</span>, the functor that returns the free monoid on a set.</p>
<p>Explicitly, <span class="math">\(LX\)</span> has <span class="math">\(X^*\)</span> as carrier (i.e. the set of <em>lists</em> of elements of <span class="math">\(X\)</span>), and the algebra is given by the coproduct of the function <span class="math">\(1 → X^*\)</span> that selects the empty list, and the list concatenation function <span class="math">\(X^* × X^* → X^*\)</span>.</p>
<p>In Haskell, this algebra looks like:</p>
<pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="ot">alg ::</span> <span class="dt">Either</span> () ([x], [x]) <span class="ot">→</span> [x]
alg (<span class="dt">Left</span> _) <span class="fu">=</span> []
alg (<span class="dt">Right</span> (xs, ys)) <span class="fu">=</span> xs <span class="fu">++</span> ys</code></pre>
<p>The endofunctor <span class="math">\(UL\)</span>, obtained by taking the carrier of the free monoid, is a monad, namely the <em>list monad</em>.</p>
<h2 id="algebras-of-a-monad">Algebras of a monad</h2>
<p>Given a monad <span class="math">\((T, η, μ)\)</span> on <span class="math">\(\set\)</span>, a monad algebra of <span class="math">\(T\)</span> is an algebra <span class="math">\((X, θ)\)</span> of the underlying functor of <span class="math">\(T\)</span>, such that the following two diagrams commute:</p>
<p><span class="math">\[
\begin{CD} X @&gt;η&gt;&gt; T X \\
@V=VV @VVθV\\
X @&gt;=&gt;&gt; X
\end{CD}
\]</span></p>
<p><span class="math">\[
\begin{CD}
T(T X) @&gt;μ&gt;&gt; T X \\
@V{T θ}VV @VVθV \\
T X @&gt;θ&gt;&gt; X
\end{CD}
\]</span></p>
<p>In Haskell notation, this means that the following two equations are satisfied:</p>
<pre class="sourceCode haskell"><code class="sourceCode haskell">θ (return x) <span class="fu">=</span> x
θ (fmap θ m) <span class="fu">=</span> θ (join m)</code></pre>
<p>In the case where the monad <span class="math">\(T\)</span> returns the set of “terms” of some language for a given set of free variables, a monad algebra can be thought of as an evaluation function.</p>
<p>The first law says that a variable is evaluated to itself, while the second law expresses the fact that when you have a “term of subterms”, you can either evaluate every subterm and then evaluate the resulting term, or regard it as a single term and evaluate it directly, and these two procedures should give the same result.</p>
<p>Naturally, monad algebras of <span class="math">\(T\)</span> form a full subcategory of <span class="math">\(\cat{Alg}_T\)</span> which we denote by <span class="math">\(\cat{mAlg}_T\)</span>.</p>
<p>We can now go back to our previous example, and look at what the monad algebras for the list monad are. Suppose we have a set <span class="math">\(X\)</span> and a function <span class="math">\(θ : X^* → X\)</span> satisfying the two laws stated above.</p>
<p>We can now define a monoid instance for <span class="math">\(X\)</span>. In Haskell, it looks like this:</p>
<pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="kw">instance</span> <span class="dt">Monoid</span> <span class="dt">X</span> <span class="kw">where</span>
empty <span class="fu">=</span> θ []
mappend x y <span class="fu">=</span> θ [x, y]</code></pre>
<p>The monoid laws follow easily from the monad algebra laws. Verifying them explicitly is a useful (and fun!) exercise. Vice versa, any monoid can be given a structure of a <span class="math">\(T\)</span>-algebra, simply by taking <code>mconcat</code> as <span class="math">\(θ\)</span>.</p>
<p>Therefore, we can extend the previous diagram of functors with an equivalence of categories: <span class="math">\[
\begin{CD}
\mathsf{mAlg}_T @&gt;&gt;&gt; \mathsf{Mon} @&gt;&gt;&gt; \mathsf{Alg}_F\\
@VVV @VUVV @VVV\\
\mathsf{Set} @&gt;=&gt;&gt; \mathsf{Set} @&gt;=&gt;&gt; \mathsf{Set}
\end{CD}
\]</span> where the top-left equivalence (which is actually an isomorphism) is determined by the <code>Monoid</code> instance that we defined above, while its inverse is given by <code>mconcat</code>.</p>
<p>Let’s step back at this whole derivation, and reflect on what it is exactly that we have proved. We started with some category of “lawful” algebras, a subcategory of <span class="math">\(\cat{Alg}_F\)</span> for some endofunctor <span class="math">\(F\)</span>. We then observed that the forgetful functor from this category to <span class="math">\(\set\)</span> admits a left adjoint <span class="math">\(L\)</span>. We then considered monad algebras of the monad <span class="math">\(UL\)</span>, and we finally observed that these are exactly those “lawful” algebras that we started with!</p>
<h2 id="monadic-functors">Monadic functors</h2>
<p>We will now generalise the previous example to an arbitrary category of algebra-like objects.</p>
<p>Suppose <span class="math">\(\cat{D}\)</span> is a category equipped with a functor <span class="math">\(G : \cat{D} → \set\)</span>. We want to think of <span class="math">\(G\)</span> as some sort of “forgetful” functor, stripping away all the structure on the objects of <span class="math">\(\cat{D}\)</span>, and returning just their carrier.</p>
<p>To make this intuition precise, we say that <span class="math">\(G\)</span> is <em>monadic</em> if:</p>
<ol style="list-style-type: decimal">
<li><span class="math">\(G\)</span> has a left adjoint <span class="math">\(L\)</span></li>
<li>The <em>comparison functor</em> <span class="math">\(\cat{D} → \cat{mAlg}_T\)</span> is an equivalence of categories, where <span class="math">\(T = GL\)</span>.</li>
</ol>
<p>The comparison functor is something that we can define for any adjunction <span class="math">\(L ⊢ G\)</span>, and it works as follows. For any object <span class="math">\(A : \cat{D}\)</span>, it returns the monad algebra structure on <span class="math">\(G A\)</span> given by <span class="math">\(G \epsilon\)</span>, where <span class="math">\(\epsilon\)</span> is the counit of the adjunction (exercise: check all the details).</p>
<p>So, what this definition is saying is that a functor is monadic if it really is the forgetful functor for the category of monad algebras for some monad. Sometimes, we say that a <em>category</em> is monadic, when the functor <span class="math">\(G\)</span> is clear.</p>
<p>The monoid example above can then be summarised by saying that the category of monoids is monadic.</p>
<h2 id="conclusion">Conclusion</h2>
<p>I’ll stop here for now. In the next post we will look at algebraically free monads and how they relate to the corresponding <a href="http://hackage.haskell.org/package/free-4.2/docs/Control-Monad-Free.html">Haskell definition</a>.</p>
</div>
</article>
<article>
<header>
<h1 class="entry-title"><a href="/blog/2013/09/18/another-proof-of-funext/">Another proof of function extensionality</a></h1>
<p class="meta">
<time datetime="2013-09-18" pubdate>Sep 18<span>th</span>, 2013</time>
</p>
</header>
<div class="entry-content">
<p>The fact that the univalence axiom implies function extensionality is one of the most well-known results of Homotopy Type Theory.</p>
<p>The <a href="https://github.com/vladimirias/Foundations/blob/master/Proof_of_Extensionality/funextfun.v">original proof</a> by Voevodsky has been simplified over time, and eventually assumed the distilled form presented in the <a href="http://homotopytypetheory.org/book/">HoTT book</a>.</p>
<p>All the various versions of the proof have roughly the same outline. They first show that the <em>weak function extensionality principle</em> (WFEP) follows from univalence, and then prove that this is enough to establish function extensionality.</p>
<p>Following the book, WFEP is the statement that contractible types are closed under <span class="math">\(Π\)</span>, i.e.:</p>
<pre class="Agda"><code><a name="1192" href="#1192" class="Function">WFEP</a><a name="1196"> </a><a name="1197" class="Symbol">:</a><a name="1198"> </a><a name="1199" class="Symbol">∀</a><a name="1200"> </a><a name="1201" href="#1201" class="Bound">i</a><a name="1202"> </a><a name="1203" href="#1203" class="Bound">j</a><a name="1204"> </a><a name="1205" class="Symbol">→</a><a name="1206"> </a><a name="1207" class="PrimitiveType">Set</a><a name="1210"> </a><a name="1211" class="Symbol">_</a><a name="1212">
</a><a name="1213" href="#1192" class="Function">WFEP</a><a name="1217"> </a><a name="1218" href="#1218" class="Bound">i</a><a name="1219"> </a><a name="1220" href="#1220" class="Bound">j</a><a name="1221"> </a><a name="1222" class="Symbol">=</a><a name="1223"> </a><a name="1224" class="Symbol">{</a><a name="1225" href="#1225" class="Bound">A</a><a name="1226"> </a><a name="1227" class="Symbol">:</a><a name="1228"> </a><a name="1229" class="PrimitiveType">Set</a><a name="1232"> </a><a name="1233" href="#1218" class="Bound">i</a><a name="1234" class="Symbol">}{</a><a name="1236" href="#1236" class="Bound">B</a><a name="1237"> </a><a name="1238" class="Symbol">:</a><a name="1239"> </a><a name="1240" href="#1225" class="Bound">A</a><a name="1241"> </a><a name="1242" class="Symbol">→</a><a name="1243"> </a><a name="1244" class="PrimitiveType">Set</a><a name="1247"> </a><a name="1248" href="#1220" class="Bound">j</a><a name="1249" class="Symbol">}</a><a name="1250">
</a><a name="1260" class="Symbol">→</a><a name="1261"> </a><a name="1262" class="Symbol">((</a><a name="1264" href="#1264" class="Bound">x</a><a name="1265"> </a><a name="1266" class="Symbol">:</a><a name="1267"> </a><a name="1268" href="#1225" class="Bound">A</a><a name="1269" class="Symbol">)</a><a name="1270"> </a><a name="1271" class="Symbol">→</a><a name="1272"> </a><a name="1273" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.hlevel.core.html#451" class="Function">contr</a><a name="1278"> </a><a name="1279" class="Symbol">(</a><a name="1280" href="#1236" class="Bound">B</a><a name="1281"> </a><a name="1282" href="#1264" class="Bound">x</a><a name="1283" class="Symbol">))</a><a name="1285">
</a><a name="1295" class="Symbol">→</a><a name="1296"> </a><a name="1297" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.hlevel.core.html#451" class="Function">contr</a><a name="1302"> </a><a name="1303" class="Symbol">((</a><a name="1305" href="#1305" class="Bound">x</a><a name="1306"> </a><a name="1307" class="Symbol">:</a><a name="1308"> </a><a name="1309" href="#1225" class="Bound">A</a><a name="1310" class="Symbol">)</a><a name="1311"> </a><a name="1312" class="Symbol">→</a><a name="1313"> </a><a name="1314" href="#1236" class="Bound">B</a><a name="1315"> </a><a name="1316" href="#1305" class="Bound">x</a><a name="1317" class="Symbol">)</a></code></pre>
<h3 id="wfep-implies-function-extensionality">WFEP implies function extensionality</h3>
<p>Showing that WFEP implies function extensionality does not need univalence, and is quite straightforward. First, we define what we mean by function extensionality:</p>
<pre class="Agda"><code><a name="1552" href="#1552" class="Function">Funext</a><a name="1558"> </a><a name="1559" class="Symbol">:</a><a name="1560"> </a><a name="1561" class="Symbol">∀</a><a name="1562"> </a><a name="1563" href="#1563" class="Bound">i</a><a name="1564"> </a><a name="1565" href="#1565" class="Bound">j</a><a name="1566"> </a><a name="1567" class="Symbol">→</a><a name="1568"> </a><a name="1569" class="PrimitiveType">Set</a><a name="1572"> </a><a name="1573" class="Symbol">_</a><a name="1574">
</a><a name="1575" href="#1552" class="Function">Funext</a><a name="1581"> </a><a name="1582" href="#1582" class="Bound">i</a><a name="1583"> </a><a name="1584" href="#1584" class="Bound">j</a><a name="1585"> </a><a name="1586" class="Symbol">=</a><a name="1587"> </a><a name="1588" class="Symbol">{</a><a name="1589" href="#1589" class="Bound">A</a><a name="1590"> </a><a name="1591" class="Symbol">:</a><a name="1592"> </a><a name="1593" class="PrimitiveType">Set</a><a name="1596"> </a><a name="1597" href="#1582" class="Bound">i</a><a name="1598" class="Symbol">}{</a><a name="1600" href="#1600" class="Bound">B</a><a name="1601"> </a><a name="1602" class="Symbol">:</a><a name="1603"> </a><a name="1604" href="#1589" class="Bound">A</a><a name="1605"> </a><a name="1606" class="Symbol">→</a><a name="1607"> </a><a name="1608" class="PrimitiveType">Set</a><a name="1611"> </a><a name="1612" href="#1584" class="Bound">j</a><a name="1613" class="Symbol">}</a><a name="1614">
</a><a name="1626" class="Symbol">→</a><a name="1627"> </a><a name="1628" class="Symbol">{</a><a name="1629" href="#1629" class="Bound">f</a><a name="1630"> </a><a name="1631" href="#1631" class="Bound">g</a><a name="1632"> </a><a name="1633" class="Symbol">:</a><a name="1634"> </a><a name="1635" class="Symbol">(</a><a name="1636" href="#1636" class="Bound">x</a><a name="1637"> </a><a name="1638" class="Symbol">:</a><a name="1639"> </a><a name="1640" href="#1589" class="Bound">A</a><a name="1641" class="Symbol">)</a><a name="1642"> </a><a name="1643" class="Symbol">→</a><a name="1644"> </a><a name="1645" href="#1600" class="Bound">B</a><a name="1646"> </a><a name="1647" href="#1636" class="Bound">x</a><a name="1648" class="Symbol">}</a><a name="1649">
</a><a name="1661" class="Symbol">→</a><a name="1662"> </a><a name="1663" class="Symbol">((</a><a name="1665" href="#1665" class="Bound">x</a><a name="1666"> </a><a name="1667" class="Symbol">:</a><a name="1668"> </a><a name="1669" href="#1589" class="Bound">A</a><a name="1670" class="Symbol">)</a><a name="1671"> </a><a name="1672" class="Symbol">→</a><a name="1673"> </a><a name="1674" href="#1629" class="Bound">f</a><a name="1675"> </a><a name="1676" href="#1665" class="Bound">x</a><a name="1677"> </a><a name="1678" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#145" class="Datatype Operator">≡</a><a name="1679"> </a><a name="1680" href="#1631" class="Bound">g</a><a name="1681"> </a><a name="1682" href="#1665" class="Bound">x</a><a name="1683" class="Symbol">)</a><a name="1684">
</a><a name="1696" class="Symbol">→</a><a name="1697"> </a><a name="1698" href="#1629" class="Bound">f</a><a name="1699"> </a><a name="1700" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#145" class="Datatype Operator">≡</a><a name="1701"> </a><a name="1702" href="#1631" class="Bound">g</a></code></pre>
<p>Now we want to show the following:</p>
<pre class="Agda"><code><a name="1765" href="#1765" class="Function">wfep-to-funext</a><a name="1779"> </a><a name="1780" class="Symbol">:</a><a name="1781"> </a><a name="1782" class="Symbol">∀</a><a name="1783"> </a><a name="1784" class="Symbol">{</a><a name="1785" href="#1785" class="Bound">i</a><a name="1786" class="Symbol">}{</a><a name="1788" href="#1788" class="Bound">j</a><a name="1789" class="Symbol">}</a><a name="1790"> </a><a name="1791" class="Symbol">→</a><a name="1792"> </a><a name="1793" href="#1192" class="Function">WFEP</a><a name="1797"> </a><a name="1798" href="#1785" class="Bound">i</a><a name="1799"> </a><a name="1800" href="#1788" class="Bound">j</a><a name="1801"> </a><a name="1802" class="Symbol">→</a><a name="1803"> </a><a name="1804" href="#1552" class="Function">Funext</a><a name="1810"> </a><a name="1811" href="#1785" class="Bound">i</a><a name="1812"> </a><a name="1813" href="#1788" class="Bound">j</a><a name="1814">
</a><a name="1815" href="#1765" class="Function">wfep-to-funext</a><a name="1829"> </a><a name="1830" class="Symbol">{</a><a name="1831" href="#1831" class="Bound">i</a><a name="1832" class="Symbol">}{</a><a name="1834" href="#1834" class="Bound">j</a><a name="1835" class="Symbol">}</a><a name="1836"> </a><a name="1837" href="#1837" class="Bound">wfep</a><a name="1841"> </a><a name="1842" class="Symbol">{</a><a name="1843" href="#1843" class="Bound">A</a><a name="1844" class="Symbol">}{</a><a name="1846" href="#1846" class="Bound">B</a><a name="1847" class="Symbol">}{</a><a name="1849" href="#1849" class="Bound">f</a><a name="1850" class="Symbol">}{</a><a name="1852" href="#1852" class="Bound">g</a><a name="1853" class="Symbol">}</a><a name="1854"> </a><a name="1855" href="#1855" class="Bound">h</a><a name="1856"> </a><a name="1857" class="Symbol">=</a><a name="1858"> </a><a name="1859" href="#2784" class="Function">p</a><a name="1860">
</a><a name="1863" class="Keyword">where</a></code></pre>
<p>To prove that <span class="math">\(f\)</span> and <span class="math">\(g\)</span> are equal, we show that they both have values in the following dependent type, which we can think of as a subtype of <span class="math">\(B(x)\)</span> for all <span class="math">\(x : A\)</span>:</p>
<pre class="Agda"><code><a name="2047"> </a><a name="2066" href="#2066" class="Function">C</a><a name="2067"> </a><a name="2068" class="Symbol">:</a><a name="2069"> </a><a name="2070" href="#1843" class="Bound">A</a><a name="2071"> </a><a name="2072" class="Symbol">→</a><a name="2073"> </a><a name="2074" class="PrimitiveType">Set</a><a name="2077"> </a><a name="2078" href="#1834" class="Bound">j</a><a name="2079">
</a><a name="2084" href="#2066" class="Function">C</a><a name="2085"> </a><a name="2086" href="#2086" class="Bound">x</a><a name="2087"> </a><a name="2088" class="Symbol">=</a><a name="2089"> </a><a name="2090" href="http://paolocapriotti.com/agda-base/v0.0.99/sum.html#159" class="Record">Σ</a><a name="2091"> </a><a name="2092" class="Symbol">(</a><a name="2093" href="#1846" class="Bound">B</a><a name="2094"> </a><a name="2095" href="#2086" class="Bound">x</a><a name="2096" class="Symbol">)</a><a name="2097"> </a><a name="2098" class="Symbol">λ</a><a name="2099"> </a><a name="2100" href="#2100" class="Bound">y</a><a name="2101"> </a><a name="2102" class="Symbol">→</a><a name="2103"> </a><a name="2104" href="#1849" class="Bound">f</a><a name="2105"> </a><a name="2106" href="#2086" class="Bound">x</a><a name="2107"> </a><a name="2108" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#145" class="Datatype Operator">≡</a><a name="2109"> </a><a name="2110" href="#2100" class="Bound">y</a></code></pre>
<p>We denote by <span class="math">\(f'\)</span> and <span class="math">\(g'\)</span> the range restrictions of <span class="math">\(f\)</span> and <span class="math">\(g\)</span> to <span class="math">\(C\)</span>:</p>
<pre class="Agda"><code><a name="2196"> </a><a name="2215" href="#2215" class="Function">f'</a><a name="2217"> </a><a name="2218" href="#2218" class="Function">g'</a><a name="2220"> </a><a name="2221" class="Symbol">:</a><a name="2222"> </a><a name="2223" class="Symbol">(</a><a name="2224" href="#2224" class="Bound">x</a><a name="2225"> </a><a name="2226" class="Symbol">:</a><a name="2227"> </a><a name="2228" href="#1843" class="Bound">A</a><a name="2229" class="Symbol">)</a><a name="2230"> </a><a name="2231" class="Symbol">→</a><a name="2232"> </a><a name="2233" href="#2066" class="Function">C</a><a name="2234"> </a><a name="2235" href="#2224" class="Bound">x</a><a name="2236">
</a><a name="2241" href="#2215" class="Function">f'</a><a name="2243"> </a><a name="2244" href="#2244" class="Bound">x</a><a name="2245"> </a><a name="2246" class="Symbol">=</a><a name="2247"> </a><a name="2248" class="Symbol">(</a><a name="2249" href="#1849" class="Bound">f</a><a name="2250"> </a><a name="2251" href="#2244" class="Bound">x</a><a name="2252"> </a><a name="2253" href="http://paolocapriotti.com/agda-base/v0.0.99/sum.html#229" class="InductiveConstructor Operator">,</a><a name="2254"> </a><a name="2255" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#193" class="InductiveConstructor">refl</a><a name="2259" class="Symbol">)</a><a name="2260">
</a><a name="2265" href="#2218" class="Function">g'</a><a name="2267"> </a><a name="2268" href="#2268" class="Bound">x</a><a name="2269"> </a><a name="2270" class="Symbol">=</a><a name="2271"> </a><a name="2272" class="Symbol">(</a><a name="2273" href="#1852" class="Bound">g</a><a name="2274"> </a><a name="2275" href="#2268" class="Bound">x</a><a name="2276"> </a><a name="2277" href="http://paolocapriotti.com/agda-base/v0.0.99/sum.html#229" class="InductiveConstructor Operator">,</a><a name="2278"> </a><a name="2279" href="#1855" class="Bound">h</a><a name="2280"> </a><a name="2281" href="#2268" class="Bound">x</a><a name="2282" class="Symbol">)</a></code></pre>
<p>where we made use of the homotopy <span class="math">\(h\)</span> between <span class="math">\(f\)</span> and <span class="math">\(g\)</span> to show that <span class="math">\(g\)</span> has values in <span class="math">\(C\)</span>. Now, <span class="math">\(C(x)\)</span> is a singleton for all <span class="math">\(x : A\)</span>, so, by WFEP, <span class="math">\(f'\)</span> and <span class="math">\(g'\)</span> have the same contractible type, hence they are equal:</p>
<pre class="Agda"><code><a name="2516"> </a><a name="2535" href="#2535" class="Function">p'</a><a name="2537"> </a><a name="2538" class="Symbol">:</a><a name="2539"> </a><a name="2540" href="#2215" class="Function">f'</a><a name="2542"> </a><a name="2543" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#145" class="Datatype Operator">≡</a><a name="2544"> </a><a name="2545" href="#2218" class="Function">g'</a><a name="2547">
</a><a name="2552" href="#2535" class="Function">p'</a><a name="2554"> </a><a name="2555" class="Symbol">=</a><a name="2556"> </a><a name="2557" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.hlevel.core.html#1164" class="Function">contr⇒prop</a><a name="2567"> </a><a name="2568" class="Symbol">(</a><a name="2569" href="#1837" class="Bound">wfep</a><a name="2573"> </a><a name="2574" class="Symbol">(λ</a><a name="2576"> </a><a name="2577" href="#2577" class="Bound">x</a><a name="2578"> </a><a name="2579" class="Symbol">→</a><a name="2580"> </a><a name="2581" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.hlevel.core.html#1874" class="Function">singl-contr</a><a name="2592"> </a><a name="2593" class="Symbol">(</a><a name="2594" href="#1849" class="Bound">f</a><a name="2595"> </a><a name="2596" href="#2577" class="Bound">x</a><a name="2597" class="Symbol">)))</a><a name="2600"> </a><a name="2601" href="#2215" class="Function">f'</a><a name="2603"> </a><a name="2604" href="#2218" class="Function">g'</a></code></pre>
<p>The fact that <span class="math">\(f\)</span> and <span class="math">\(g\)</span> are equal then follows immediately by applying the first projection and (implicitly) using <span class="math">\(η\)</span> conversion for <span class="math">\(Π\)</span>-types:</p>
<pre class="Agda"><code><a name="2765"> </a><a name="2784" href="#2784" class="Function">p</a><a name="2785"> </a><a name="2786" class="Symbol">:</a><a name="2787"> </a><a name="2788" href="#1849" class="Bound">f</a><a name="2789"> </a><a name="2790" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#145" class="Datatype Operator">≡</a><a name="2791"> </a><a name="2792" href="#1852" class="Bound">g</a><a name="2793">
</a><a name="2798" href="#2784" class="Function">p</a><a name="2799"> </a><a name="2800" class="Symbol">=</a><a name="2801"> </a><a name="2802" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#364" class="Function">ap</a><a name="2804"> </a><a name="2805" class="Symbol">(λ</a><a name="2807"> </a><a name="2808" href="#2808" class="Bound">u</a><a name="2809"> </a><a name="2810" href="#2810" class="Bound">x</a><a name="2811"> </a><a name="2812" class="Symbol">→</a><a name="2813"> </a><a name="2814" href="http://paolocapriotti.com/agda-base/v0.0.99/sum.html#245" class="Function">proj₁</a><a name="2819"> </a><a name="2820" class="Symbol">(</a><a name="2821" href="#2808" class="Bound">u</a><a name="2822"> </a><a name="2823" href="#2810" class="Bound">x</a><a name="2824" class="Symbol">))</a><a name="2826"> </a><a name="2827" href="#2535" class="Function">p'</a></code></pre>
<p>In the book, the strong version of extensionality, i.e.</p>
<pre class="Agda"><code><a name="2912" href="#2912" class="Function">StrongFunext</a><a name="2924"> </a><a name="2925" class="Symbol">:</a><a name="2926"> </a><a name="2927" class="Symbol">∀</a><a name="2928"> </a><a name="2929" href="#2929" class="Bound">i</a><a name="2930"> </a><a name="2931" href="#2931" class="Bound">j</a><a name="2932"> </a><a name="2933" class="Symbol">→</a><a name="2934"> </a><a name="2935" class="PrimitiveType">Set</a><a name="2938"> </a><a name="2939" class="Symbol">_</a><a name="2940">
</a><a name="2941" href="#2912" class="Function">StrongFunext</a><a name="2953"> </a><a name="2954" href="#2954" class="Bound">i</a><a name="2955"> </a><a name="2956" href="#2956" class="Bound">j</a><a name="2957"> </a><a name="2958" class="Symbol">=</a><a name="2959"> </a><a name="2960" class="Symbol">{</a><a name="2961" href="#2961" class="Bound">A</a><a name="2962"> </a><a name="2963" class="Symbol">:</a><a name="2964"> </a><a name="2965" class="PrimitiveType">Set</a><a name="2968"> </a><a name="2969" href="#2954" class="Bound">i</a><a name="2970" class="Symbol">}{</a><a name="2972" href="#2972" class="Bound">B</a><a name="2973"> </a><a name="2974" class="Symbol">:</a><a name="2975"> </a><a name="2976" href="#2961" class="Bound">A</a><a name="2977"> </a><a name="2978" class="Symbol">→</a><a name="2979"> </a><a name="2980" class="PrimitiveType">Set</a><a name="2983"> </a><a name="2984" href="#2956" class="Bound">j</a><a name="2985" class="Symbol">}</a><a name="2986">
</a><a name="3004" class="Symbol">→</a><a name="3005"> </a><a name="3006" class="Symbol">{</a><a name="3007" href="#3007" class="Bound">f</a><a name="3008"> </a><a name="3009" href="#3009" class="Bound">g</a><a name="3010"> </a><a name="3011" class="Symbol">:</a><a name="3012"> </a><a name="3013" class="Symbol">(</a><a name="3014" href="#3014" class="Bound">x</a><a name="3015"> </a><a name="3016" class="Symbol">:</a><a name="3017"> </a><a name="3018" href="#2961" class="Bound">A</a><a name="3019" class="Symbol">)</a><a name="3020"> </a><a name="3021" class="Symbol">→</a><a name="3022"> </a><a name="3023" href="#2972" class="Bound">B</a><a name="3024"> </a><a name="3025" href="#3014" class="Bound">x</a><a name="3026" class="Symbol">}</a><a name="3027">
</a><a name="3045" class="Symbol">→</a><a name="3046"> </a><a name="3047" class="Symbol">((</a><a name="3049" href="#3049" class="Bound">x</a><a name="3050"> </a><a name="3051" class="Symbol">:</a><a name="3052"> </a><a name="3053" href="#2961" class="Bound">A</a><a name="3054" class="Symbol">)</a><a name="3055"> </a><a name="3056" class="Symbol">→</a><a name="3057"> </a><a name="3058" href="#3007" class="Bound">f</a><a name="3059"> </a><a name="3060" href="#3049" class="Bound">x</a><a name="3061"> </a><a name="3062" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#145" class="Datatype Operator">≡</a><a name="3063"> </a><a name="3064" href="#3009" class="Bound">g</a><a name="3065"> </a><a name="3066" href="#3049" class="Bound">x</a><a name="3067" class="Symbol">)</a><a name="3068">
</a><a name="3086" href="http://paolocapriotti.com/agda-base/v0.0.99/function.isomorphism.core.html#355" class="Record Operator">≅</a><a name="3087"> </a><a name="3088" class="Symbol">(</a><a name="3089" href="#3007" class="Bound">f</a><a name="3090"> </a><a name="3091" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#145" class="Datatype Operator">≡</a><a name="3092"> </a><a name="3093" href="#3009" class="Bound">g</a><a name="3094" class="Symbol">)</a></code></pre>
<p>is obtained directly using a more sophisticated, but very similar argument.</p>
<h3 id="proving-wfep">Proving WFEP</h3>
<p>Now we turn to proving WFEP itself. Most of the proofs I know use the fact that univalence implies a certain congruence rule for function-types, i.e. if <span class="math">\(B\)</span> and <span class="math">\(B'\)</span> are equivalent types, then <span class="math">\(A → B\)</span> and <span class="math">\(A → B'\)</span> are also equivalent, and furthermore the equivalence is given by precomposing with the equivalence between <span class="math">\(B\)</span> and <span class="math">\(B'\)</span>.</p>
<p>However, if we have η conversion for record types, there is a much simpler way to obtain WFEP from univalence.</p>
<p>The idea is as follows: since <span class="math">\(B(x)\)</span> is contractible for all <span class="math">\(x : A\)</span>, univalence implies that <span class="math">\(B(x) ≡ ⊤\)</span>, so the contractibility of <span class="math">\((x : A) → B(x)\)</span> is a consequence of the contractibility of <span class="math">\(A → ⊤\)</span>, which is itself an immediate consequence of the <a class="target" id="contr-exp-T">definitional <span class="math">\(η\)</span> rule for <span class="math">\(⊤\)</span></a>:</p>
<pre class="Agda"><code><a name="4029"></a><a name="4032" class="Keyword">record</a><a name="4038"> </a><a name="4039" href="#4039" class="Record">⊤</a><a name="4040"> </a><a name="4041" class="Symbol">:</a><a name="4042"> </a><a name="4043" class="PrimitiveType">Set</a><a name="4046"> </a><a name="4047" href="#4009" class="Bound">j</a><a name="4048"> </a><a name="4049" class="Keyword">where</a><a name="4054">
</a><a name="4059" class="Keyword">constructor</a><a name="4070"> </a><a name="4071" href="#4071" class="InductiveConstructor">tt</a><a name="4073">
</a><a name="4077" href="#4077" class="Function">⊤-contr</a><a name="4084"> </a><a name="4085" class="Symbol">:</a><a name="4086"> </a><a name="4087" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.hlevel.core.html#451" class="Function">contr</a><a name="4092"> </a><a name="4093" href="#4039" class="Record">⊤</a><a name="4094">
</a><a name="4097" href="#4077" class="Function">⊤-contr</a><a name="4104"> </a><a name="4105" class="Symbol">=</a><a name="4106"> </a><a name="4107" href="#4071" class="InductiveConstructor">tt</a><a name="4109"> </a><a name="4110" href="http://paolocapriotti.com/agda-base/v0.0.99/sum.html#229" class="InductiveConstructor Operator">,</a><a name="4111"> </a><a name="4112" class="Symbol">λ</a><a name="4113"> </a><a name="4114" class="Symbol">{</a><a name="4115"> </a><a name="4116" href="#4071" class="InductiveConstructor">tt</a><a name="4118"> </a><a name="4119" class="Symbol">→</a><a name="4120"> </a><a name="4121" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#193" class="InductiveConstructor">refl</a><a name="4125"> </a><a name="4126" class="Symbol">}</a><a name="4127">
</a><a name="4131" href="#4131" class="Function">contr-exp-⊤</a><a name="4142"> </a><a name="4143" class="Symbol">:</a><a name="4144"> </a><a name="4145" class="Symbol">∀</a><a name="4146"> </a><a name="4147" class="Symbol">{</a><a name="4148" href="#4148" class="Bound">i</a><a name="4149" class="Symbol">}{</a><a name="4151" href="#4151" class="Bound">A</a><a name="4152"> </a><a name="4153" class="Symbol">:</a><a name="4154"> </a><a name="4155" class="PrimitiveType">Set</a><a name="4158"> </a><a name="4159" href="#4148" class="Bound">i</a><a name="4160" class="Symbol">}</a><a name="4161"> </a><a name="4162" class="Symbol">→</a><a name="4163"> </a><a name="4164" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.hlevel.core.html#451" class="Function">contr</a><a name="4169"> </a><a name="4170" class="Symbol">(</a><a name="4171" href="#4151" class="Bound">A</a><a name="4172"> </a><a name="4173" class="Symbol">→</a><a name="4174"> </a><a name="4175" href="#4039" class="Record">⊤</a><a name="4176" class="Symbol">)</a><a name="4177">
</a><a name="4180" href="#4131" class="Function">contr-exp-⊤</a><a name="4191"> </a><a name="4192" class="Symbol">=</a><a name="4193"> </a><a name="4194" class="Symbol">(λ</a><a name="4196"> </a><a name="4197" href="#4197" class="Bound">_</a><a name="4198"> </a><a name="4199" class="Symbol">→</a><a name="4200"> </a><a name="4201" href="#4071" class="InductiveConstructor">tt</a><a name="4203" class="Symbol">)</a><a name="4204"> </a><a name="4205" href="http://paolocapriotti.com/agda-base/v0.0.99/sum.html#229" class="InductiveConstructor Operator">,</a><a name="4206"> </a><a name="4207" class="Symbol">(λ</a><a name="4209"> </a><a name="4210" href="#4210" class="Bound">f</a><a name="4211"> </a><a name="4212" class="Symbol">→</a><a name="4213"> </a><a name="4214" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#193" class="InductiveConstructor">refl</a><a name="4218" class="Symbol">)</a><a name="4219">
</a></code></pre>
<p>However, the proof sketch above is missing a crucial step: even though <span class="math">\(B(x)\)</span> is pointwise equal to <span class="math">\(⊤\)</span>, in order to substitute <span class="math">\(⊤\)</span> for <span class="math">\(B(x)\)</span> in the <span class="math">\(Π\)</span>-type, we need to show that <span class="math">\(B ≡ λ \_ → ⊤\)</span>, but we’re not allowed to use function extensionality, yet!</p>
<p>Fortunately, we only need a very special case of function extensionality. So the trick here is to apply the argument to this special case first, and then use it to prove the general result.</p>
<p>First we prove WFEP for non-dependent <span class="math">\(Π\)</span>-types, by formalising the above proof sketch.</p>
<pre class="Agda"><code><a name="4794" href="#4794" class="Function">nondep-wfep</a><a name="4805"> </a><a name="4806" class="Symbol">:</a><a name="4807"> </a><a name="4808" class="Symbol">∀</a><a name="4809"> </a><a name="4810" class="Symbol">{</a><a name="4811" href="#4811" class="Bound">i</a><a name="4812"> </a><a name="4813" href="#4813" class="Bound">j</a><a name="4814" class="Symbol">}{</a><a name="4816" href="#4816" class="Bound">A</a><a name="4817"> </a><a name="4818" class="Symbol">:</a><a name="4819"> </a><a name="4820" class="PrimitiveType">Set</a><a name="4823"> </a><a name="4824" href="#4811" class="Bound">i</a><a name="4825" class="Symbol">}{</a><a name="4827" href="#4827" class="Bound">B</a><a name="4828"> </a><a name="4829" class="Symbol">:</a><a name="4830"> </a><a name="4831" class="PrimitiveType">Set</a><a name="4834"> </a><a name="4835" href="#4813" class="Bound">j</a><a name="4836" class="Symbol">}</a><a name="4837">
</a><a name="4850" class="Symbol">→</a><a name="4851"> </a><a name="4852" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.hlevel.core.html#451" class="Function">contr</a><a name="4857"> </a><a name="4858" href="#4827" class="Bound">B</a><a name="4859">
</a><a name="4872" class="Symbol">→</a><a name="4873"> </a><a name="4874" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.hlevel.core.html#451" class="Function">contr</a><a name="4879"> </a><a name="4880" class="Symbol">(</a><a name="4881" href="#4816" class="Bound">A</a><a name="4882"> </a><a name="4883" class="Symbol">→</a><a name="4884"> </a><a name="4885" href="#4827" class="Bound">B</a><a name="4886" class="Symbol">)</a><a name="4887">
</a><a name="4888" href="#4794" class="Function">nondep-wfep</a><a name="4899"> </a><a name="4900" class="Symbol">{</a><a name="4901">A </a><a name="4903" class="Symbol">=</a><a name="4904"> </a><a name="4905" href="#4905" class="Bound">A</a><a name="4906" class="Symbol">}{</a><a name="4908">B </a><a name="4910" class="Symbol">=</a><a name="4911"> </a><a name="4912" href="#4912" class="Bound">B</a><a name="4913" class="Symbol">}</a><a name="4914"> </a><a name="4915" href="#4915" class="Bound">hB</a><a name="4917"> </a><a name="4918" class="Symbol">=</a><a name="4919"> </a><a name="4920" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#633" class="Function">subst</a><a name="4925"> </a><a name="4926" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.hlevel.core.html#451" class="Function">contr</a><a name="4931"> </a><a name="4932" href="#4992" class="Function">p</a><a name="4933"> </a><a name="4934" href="#4131" class="Function">contr-exp-⊤</a><a name="4945">
</a><a name="4948" class="Keyword">where</a><a name="4953">
</a><a name="4987"> </a><a name="4992" href="#4992" class="Function">p</a><a name="4993"> </a><a name="4994" class="Symbol">:</a><a name="4995"> </a><a name="4996" class="Symbol">(</a><a name="4997" href="#4905" class="Bound">A</a><a name="4998"> </a><a name="4999" class="Symbol">→</a><a name="5000"> </a><a name="5001" href="#4039" class="Record">⊤</a><a name="5002" class="Symbol">)</a><a name="5003"> </a><a name="5004" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#145" class="Datatype Operator">≡</a><a name="5005"> </a><a name="5006" class="Symbol">(</a><a name="5007" href="#4905" class="Bound">A</a><a name="5008"> </a><a name="5009" class="Symbol">→</a><a name="5010"> </a><a name="5011" href="#4912" class="Bound">B</a><a name="5012" class="Symbol">)</a><a name="5013">
</a><a name="5018" href="#4992" class="Function">p</a><a name="5019"> </a><a name="5020" class="Symbol">=</a><a name="5021"> </a><a name="5022" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#364" class="Function">ap</a><a name="5024"> </a><a name="5025" class="Symbol">(λ</a><a name="5027"> </a><a name="5028" href="#5028" class="Bound">X</a><a name="5029"> </a><a name="5030" class="Symbol">→</a><a name="5031"> </a><a name="5032" href="#4905" class="Bound">A</a><a name="5033"> </a><a name="5034" class="Symbol">→</a><a name="5035"> </a><a name="5036" href="#5028" class="Bound">X</a><a name="5037" class="Symbol">)</a><a name="5038"> </a><a name="5039" class="Symbol">(</a><a name="5040" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.hlevel.closure.core.html#997" class="Function">unique-contr</a><a name="5052"> </a><a name="5053" href="#4077" class="Function">⊤-contr</a><a name="5060"> </a><a name="5061" href="#4915" class="Bound">hB</a><a name="5063" class="Symbol">)</a></code></pre>
<p>Since <span class="math">\(B\)</span> is non-dependent in this case, the proof goes through without function extensionality, so we don’t get stuck in an infinite regression: two iterations are enough!</p>
<p>Now we can prove the special case of function extensionality that we will need for the proof of full WFEP:</p>
<pre class="Agda"><code><a name="5372" href="#5372" class="Function">funext'</a><a name="5379"> </a><a name="5380" class="Symbol">:</a><a name="5381"> </a><a name="5382" class="Symbol">∀</a><a name="5383"> </a><a name="5384" class="Symbol">{</a><a name="5385" href="#5385" class="Bound">i</a><a name="5386"> </a><a name="5387" href="#5387" class="Bound">j</a><a name="5388" class="Symbol">}{</a><a name="5390" href="#5390" class="Bound">A</a><a name="5391"> </a><a name="5392" class="Symbol">:</a><a name="5393"> </a><a name="5394" class="PrimitiveType">Set</a><a name="5397"> </a><a name="5398" href="#5385" class="Bound">i</a><a name="5399" class="Symbol">}{</a><a name="5401" href="#5401" class="Bound">B</a><a name="5402"> </a><a name="5403" class="Symbol">:</a><a name="5404"> </a><a name="5405" class="PrimitiveType">Set</a><a name="5408"> </a><a name="5409" href="#5387" class="Bound">j</a><a name="5410" class="Symbol">}</a><a name="5411">
</a><a name="5420" class="Symbol">→</a><a name="5421"> </a><a name="5422" class="Symbol">(</a><a name="5423" href="#5423" class="Bound">f</a><a name="5424"> </a><a name="5425" class="Symbol">:</a><a name="5426"> </a><a name="5427" href="#5390" class="Bound">A</a><a name="5428"> </a><a name="5429" class="Symbol">→</a><a name="5430"> </a><a name="5431" href="#5401" class="Bound">B</a><a name="5432" class="Symbol">)(</a><a name="5434" href="#5434" class="Bound">b</a><a name="5435"> </a><a name="5436" class="Symbol">:</a><a name="5437"> </a><a name="5438" href="#5401" class="Bound">B</a><a name="5439" class="Symbol">)(</a><a name="5441" href="#5441" class="Bound">h</a><a name="5442"> </a><a name="5443" class="Symbol">:</a><a name="5444"> </a><a name="5445" class="Symbol">(</a><a name="5446" href="#5446" class="Bound">x</a><a name="5447"> </a><a name="5448" class="Symbol">:</a><a name="5449"> </a><a name="5450" href="#5390" class="Bound">A</a><a name="5451" class="Symbol">)</a><a name="5452"> </a><a name="5453" class="Symbol">→</a><a name="5454"> </a><a name="5455" href="#5434" class="Bound">b</a><a name="5456"> </a><a name="5457" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#145" class="Datatype Operator">≡</a><a name="5458"> </a><a name="5459" href="#5423" class="Bound">f</a><a name="5460"> </a><a name="5461" href="#5446" class="Bound">x</a><a name="5462" class="Symbol">)</a><a name="5463">
</a><a name="5472" class="Symbol">→</a><a name="5473"> </a><a name="5474" class="Symbol">(λ</a><a name="5476"> </a><a name="5477" href="#5477" class="Bound">_</a><a name="5478"> </a><a name="5479" class="Symbol">→</a><a name="5480"> </a><a name="5481" href="#5434" class="Bound">b</a><a name="5482" class="Symbol">)</a><a name="5483"> </a><a name="5484" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#145" class="Datatype Operator">≡</a><a name="5485"> </a><a name="5486" href="#5423" class="Bound">f</a><a name="5487">
</a><a name="5488" href="#5372" class="Function">funext'</a><a name="5495"> </a><a name="5496" href="#5496" class="Bound">f</a><a name="5497"> </a><a name="5498" href="#5498" class="Bound">b</a><a name="5499"> </a><a name="5500" href="#5500" class="Bound">h</a><a name="5501"> </a><a name="5502" class="Symbol">=</a><a name="5503">
</a><a name="5506" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#364" class="Function">ap</a><a name="5508"> </a><a name="5509" class="Symbol">(λ</a><a name="5511"> </a><a name="5512" href="#5512" class="Bound">u</a><a name="5513"> </a><a name="5514" href="#5514" class="Bound">x</a><a name="5515"> </a><a name="5516" class="Symbol">→</a><a name="5517"> </a><a name="5518" href="http://paolocapriotti.com/agda-base/v0.0.99/sum.html#245" class="Function">proj₁</a><a name="5523"> </a><a name="5524" class="Symbol">(</a><a name="5525" href="#5512" class="Bound">u</a><a name="5526"> </a><a name="5527" href="#5514" class="Bound">x</a><a name="5528" class="Symbol">))</a><a name="5530">
</a><a name="5538" class="Symbol">(</a><a name="5539" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.hlevel.core.html#1164" class="Function">contr⇒prop</a><a name="5549"> </a><a name="5550" class="Symbol">(</a><a name="5551" href="#4794" class="Function">nondep-wfep</a><a name="5562"> </a><a name="5563" class="Symbol">(</a><a name="5564" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.hlevel.core.html#1874" class="Function">singl-contr</a><a name="5575"> </a><a name="5576" href="#5498" class="Bound">b</a><a name="5577" class="Symbol">))</a><a name="5579">
</a><a name="5600" class="Symbol">(λ</a><a name="5602"> </a><a name="5603" href="#5603" class="Bound">_</a><a name="5604"> </a><a name="5605" class="Symbol">→</a><a name="5606"> </a><a name="5607" class="Symbol">(</a><a name="5608" href="#5498" class="Bound">b</a><a name="5609"> </a><a name="5610" href="http://paolocapriotti.com/agda-base/v0.0.99/sum.html#229" class="InductiveConstructor Operator">,</a><a name="5611"> </a><a name="5612" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#193" class="InductiveConstructor">refl</a><a name="5616" class="Symbol">))</a><a name="5618">
</a><a name="5639" class="Symbol">(λ</a><a name="5641"> </a><a name="5642" href="#5642" class="Bound">x</a><a name="5643"> </a><a name="5644" class="Symbol">→</a><a name="5645"> </a><a name="5646" href="#5496" class="Bound">f</a><a name="5647"> </a><a name="5648" href="#5642" class="Bound">x</a><a name="5649"> </a><a name="5650" href="http://paolocapriotti.com/agda-base/v0.0.99/sum.html#229" class="InductiveConstructor Operator">,</a><a name="5651"> </a><a name="5652" href="#5500" class="Bound">h</a><a name="5653"> </a><a name="5654" href="#5642" class="Bound">x</a><a name="5655" class="Symbol">))</a></code></pre>
<p>Same proof as for <code>wfep-to-funext</code>, only written more succinctly.</p>
<p>Finally, we are ready to prove WFEP:</p>
<pre class="Agda"><code><a name="5788" href="#5788" class="Function">wfep</a><a name="5792"> </a><a name="5793" class="Symbol">:</a><a name="5794"> </a><a name="5795" class="Symbol">∀</a><a name="5796"> </a><a name="5797" class="Symbol">{</a><a name="5798" href="#5798" class="Bound">i</a><a name="5799"> </a><a name="5800" href="#5800" class="Bound">j</a><a name="5801" class="Symbol">}</a><a name="5802"> </a><a name="5803" class="Symbol">→</a><a name="5804"> </a><a name="5805" href="#1192" class="Function">WFEP</a><a name="5809"> </a><a name="5810" href="#5798" class="Bound">i</a><a name="5811"> </a><a name="5812" href="#5800" class="Bound">j</a><a name="5813">
</a><a name="5814" href="#5788" class="Function">wfep</a><a name="5818"> </a><a name="5819" class="Symbol">{</a><a name="5820" href="#5820" class="Bound">i</a><a name="5821" class="Symbol">}{</a><a name="5823" href="#5823" class="Bound">j</a><a name="5824" class="Symbol">}{</a><a name="5826" href="#5826" class="Bound">A</a><a name="5827" class="Symbol">}{</a><a name="5829" href="#5829" class="Bound">B</a><a name="5830" class="Symbol">}</a><a name="5831"> </a><a name="5832" href="#5832" class="Bound">hB</a><a name="5834"> </a><a name="5835" class="Symbol">=</a><a name="5836"> </a><a name="5837" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#633" class="Function">subst</a><a name="5842"> </a><a name="5843" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.hlevel.core.html#451" class="Function">contr</a><a name="5848"> </a><a name="5849" href="#5990" class="Function">p</a><a name="5850"> </a><a name="5851" href="#4131" class="Function">contr-exp-⊤</a><a name="5862">
</a><a name="5865" class="Keyword">where</a><a name="5870">
</a><a name="5904"> </a><a name="5909" href="#5909" class="Function">p₀</a><a name="5911"> </a><a name="5912" class="Symbol">:</a><a name="5913"> </a><a name="5914" class="Symbol">(λ</a><a name="5916"> </a><a name="5917" href="#5917" class="Bound">_</a><a name="5918"> </a><a name="5919" class="Symbol">→</a><a name="5920"> </a><a name="5921" href="#4039" class="Record">⊤</a><a name="5922" class="Symbol">)</a><a name="5923"> </a><a name="5924" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#145" class="Datatype Operator">≡</a><a name="5925"> </a><a name="5926" href="#5829" class="Bound">B</a><a name="5927">
</a><a name="5932" href="#5909" class="Function">p₀</a><a name="5934"> </a><a name="5935" class="Symbol">=</a><a name="5936"> </a><a name="5937" href="#5372" class="Function">funext'</a><a name="5944"> </a><a name="5945" href="#5829" class="Bound">B</a><a name="5946"> </a><a name="5947" href="#4039" class="Record">⊤</a><a name="5948"> </a><a name="5949" class="Symbol">(λ</a><a name="5951"> </a><a name="5952" href="#5952" class="Bound">x</a><a name="5953"> </a><a name="5954" class="Symbol">→</a><a name="5955"> </a><a name="5956" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.hlevel.closure.core.html#997" class="Function">unique-contr</a><a name="5968"> </a><a name="5969" href="#4077" class="Function">⊤-contr</a><a name="5976"> </a><a name="5977" class="Symbol">(</a><a name="5978" href="#5832" class="Bound">hB</a><a name="5980"> </a><a name="5981" href="#5952" class="Bound">x</a><a name="5982" class="Symbol">))</a><a name="5984">
</a><a name="5990" href="#5990" class="Function">p</a><a name="5991"> </a><a name="5992" class="Symbol">:</a><a name="5993"> </a><a name="5994" class="Symbol">(</a><a name="5995" href="#5826" class="Bound">A</a><a name="5996"> </a><a name="5997" class="Symbol">→</a><a name="5998"> </a><a name="5999" href="#4039" class="Record">⊤</a><a name="6000"> </a><a name="6001" class="Symbol">{</a><a name="6002" href="#5823" class="Bound">j</a><a name="6003" class="Symbol">})</a><a name="6005"> </a><a name="6006" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#145" class="Datatype Operator">≡</a><a name="6007"> </a><a name="6008" class="Symbol">((</a><a name="6010" href="#6010" class="Bound">x</a><a name="6011"> </a><a name="6012" class="Symbol">:</a><a name="6013"> </a><a name="6014" href="#5826" class="Bound">A</a><a name="6015" class="Symbol">)</a><a name="6016"> </a><a name="6017" class="Symbol">→</a><a name="6018"> </a><a name="6019" href="#5829" class="Bound">B</a><a name="6020"> </a><a name="6021" href="#6010" class="Bound">x</a><a name="6022" class="Symbol">)</a><a name="6023">
</a><a name="6028" href="#5990" class="Function">p</a><a name="6029"> </a><a name="6030" class="Symbol">=</a><a name="6031"> </a><a name="6032" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#364" class="Function">ap</a><a name="6034"> </a><a name="6035" class="Symbol">(λ</a><a name="6037"> </a><a name="6038" href="#6038" class="Bound">Z</a><a name="6039"> </a><a name="6040" class="Symbol">→</a><a name="6041"> </a><a name="6042" class="Symbol">(</a><a name="6043" href="#6043" class="Bound">x</a><a name="6044"> </a><a name="6045" class="Symbol">:</a><a name="6046"> </a><a name="6047" href="#5826" class="Bound">A</a><a name="6048" class="Symbol">)</a><a name="6049"> </a><a name="6050" class="Symbol">→</a><a name="6051"> </a><a name="6052" href="#6038" class="Bound">Z</a><a name="6053"> </a><a name="6054" href="#6043" class="Bound">x</a><a name="6055" class="Symbol">)</a><a name="6056"> </a><a name="6057" href="#5909" class="Function">p₀</a></code></pre>
<p>By putting it all together we get function extensionality:</p>
<pre class="Agda"><code><a name="6145" href="#6145" class="Function">funext</a><a name="6151"> </a><a name="6152" class="Symbol">:</a><a name="6153"> </a><a name="6154" class="Symbol">∀</a><a name="6155"> </a><a name="6156" class="Symbol">{</a><a name="6157" href="#6157" class="Bound">i</a><a name="6158"> </a><a name="6159" href="#6159" class="Bound">j</a><a name="6160" class="Symbol">}</a><a name="6161"> </a><a name="6162" class="Symbol">→</a><a name="6163"> </a><a name="6164" href="#1552" class="Function">Funext</a><a name="6170"> </a><a name="6171" href="#6157" class="Bound">i</a><a name="6172"> </a><a name="6173" href="#6159" class="Bound">j</a><a name="6174">
</a><a name="6175" href="#6145" class="Function">funext</a><a name="6181"> </a><a name="6182" class="Symbol">=</a><a name="6183"> </a><a name="6184" href="#1765" class="Function">wfep-to-funext</a><a name="6198"> </a><a name="6199" href="#5788" class="Function">wfep</a></code></pre>
<h3 id="avoiding-η-for-records">Avoiding η for records</h3>
<p>This proof can also be modified to work in a theory where <span class="math">\(⊤\)</span> does not have definitional η conversion.</p>
<p>The only point where η is used is in the proof of <code>contr-exp-⊤</code> <a href="#contr-exp-T">above</a>. So let’s define a version of <span class="math">\(⊤\)</span> without η, and prove <code>contr-exp-⊤</code> for it.</p>
<pre class="Agda"><code><a name="6572"></a><a name="6575" class="Keyword">data</a><a name="6579"> </a><a name="6580" href="#6580" class="Datatype">⊤</a><a name="6581"> </a><a name="6582" class="Symbol">:</a><a name="6583"> </a><a name="6584" class="PrimitiveType">Set</a><a name="6587"> </a><a name="6588" href="#6552" class="Bound">j</a><a name="6589"> </a><a name="6590" class="Keyword">where</a><a name="6595">
</a><a name="6600" href="#6600" class="InductiveConstructor">tt</a><a name="6602"> </a><a name="6603" class="Symbol">:</a><a name="6604"> </a><a name="6605" href="#6580" class="Datatype">⊤</a><a name="6606">
</a><a name="6610" href="#6610" class="Function">⊤-contr</a><a name="6617"> </a><a name="6618" class="Symbol">:</a><a name="6619"> </a><a name="6620" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.hlevel.core.html#451" class="Function">contr</a><a name="6625"> </a><a name="6626" href="#6580" class="Datatype">⊤</a><a name="6627">
</a><a name="6630" href="#6610" class="Function">⊤-contr</a><a name="6637"> </a><a name="6638" class="Symbol">=</a><a name="6639"> </a><a name="6640" href="#6600" class="InductiveConstructor">tt</a><a name="6642"> </a><a name="6643" href="http://paolocapriotti.com/agda-base/v0.0.99/sum.html#229" class="InductiveConstructor Operator">,</a><a name="6644"> </a><a name="6645" class="Symbol">λ</a><a name="6646"> </a><a name="6647" class="Symbol">{</a><a name="6648"> </a><a name="6649" href="#6600" class="InductiveConstructor">tt</a><a name="6651"> </a><a name="6652" class="Symbol">→</a><a name="6653"> </a><a name="6654" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#193" class="InductiveConstructor">refl</a><a name="6658"> </a><a name="6659" class="Symbol">}</a></code></pre>
<p>We begin by defining the automorphism <span class="math">\(k\)</span> of <span class="math">\(⊤\)</span> which maps everything to <span class="math">\(\mathsf{tt}\)</span>. Clearly, <span class="math">\(k\)</span> is going to be the identity, but we can’t prove that until we have function extensionality.</p>
<pre class="Agda"><code><a name="6867"></a><a name="6884" href="#6884" class="Function">k</a><a name="6885"> </a><a name="6886" class="Symbol">:</a><a name="6887"> </a><a name="6888" href="#6580" class="Datatype">⊤</a><a name="6889"> </a><a name="6890" class="Symbol">→</a><a name="6891"> </a><a name="6892" href="#6580" class="Datatype">⊤</a><a name="6893">
</a><a name="6896" href="#6884" class="Function">k</a><a name="6897"> </a><a name="6898" class="Symbol">_</a><a name="6899"> </a><a name="6900" class="Symbol">=</a><a name="6901"> </a><a name="6902" href="#6600" class="InductiveConstructor">tt</a><a name="6904">
</a><a name="6908" href="#6908" class="Function">k-we</a><a name="6912"> </a><a name="6913" class="Symbol">:</a><a name="6914"> </a><a name="6915" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.weak-equivalence.core.html#440" class="Function">weak-equiv</a><a name="6925"> </a><a name="6926" href="#6884" class="Function">k</a><a name="6927">
</a><a name="6930" href="#6908" class="Function">k-we</a><a name="6934"> </a><a name="6935" href="#6600" class="InductiveConstructor">tt</a><a name="6937"> </a><a name="6938" class="Symbol">=</a><a name="6939"> </a><a name="6940" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.hlevel.closure.core.html#505" class="Function">Σ-contr</a><a name="6947"> </a><a name="6948" href="#6610" class="Function">⊤-contr</a><a name="6955"> </a><a name="6956" class="Symbol">(λ</a><a name="6958"> </a><a name="6959" href="#6959" class="Bound">_</a><a name="6960"> </a><a name="6961" class="Symbol">→</a><a name="6962"> </a><a name="6963" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.hlevel.core.html#1297" class="Function">h↑</a><a name="6965"> </a><a name="6966" href="#6610" class="Function">⊤-contr</a><a name="6973"> </a><a name="6974" href="#6600" class="InductiveConstructor">tt</a><a name="6976"> </a><a name="6977" href="#6600" class="InductiveConstructor">tt</a><a name="6979" class="Symbol">)</a></code></pre>
<p>Now we apply the argument sketched above, based on the fact that univalence implies congruence rules for function types. We extract an equality out of <span class="math">\(k\)</span>, and then transport it to the exponentials:</p>
<pre class="Agda"><code><a name="7192"></a><a name="7209" href="#7209" class="Function">k-eq</a><a name="7213"> </a><a name="7214" class="Symbol">:</a><a name="7215"> </a><a name="7216" href="#6580" class="Datatype">⊤</a><a name="7217"> </a><a name="7218" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#145" class="Datatype Operator">≡</a><a name="7219"> </a><a name="7220" href="#6580" class="Datatype">⊤</a><a name="7221">
</a><a name="7224" href="#7209" class="Function">k-eq</a><a name="7228"> </a><a name="7229" class="Symbol">=</a><a name="7230"> </a><a name="7231" href="http://paolocapriotti.com/agda-base/v0.0.99/function.isomorphism.core.html#452" class="Function">≈⇒≡</a><a name="7234"> </a><a name="7235" class="Symbol">(</a><a name="7236" href="#6884" class="Function">k</a><a name="7237"> </a><a name="7238" href="http://paolocapriotti.com/agda-base/v0.0.99/sum.html#229" class="InductiveConstructor Operator">,</a><a name="7239"> </a><a name="7240" href="#6908" class="Function">k-we</a><a name="7244" class="Symbol">)</a><a name="7245">
</a><a name="7249" href="#7249" class="Function">k-exp-eq</a><a name="7257"> </a><a name="7258" class="Symbol">:</a><a name="7259"> </a><a name="7260" class="Symbol">∀</a><a name="7261"> </a><a name="7262" class="Symbol">{</a><a name="7263" href="#7263" class="Bound">i</a><a name="7264" class="Symbol">}(</a><a name="7266" href="#7266" class="Bound">A</a><a name="7267"> </a><a name="7268" class="Symbol">:</a><a name="7269"> </a><a name="7270" class="PrimitiveType">Set</a><a name="7273"> </a><a name="7274" href="#7263" class="Bound">i</a><a name="7275" class="Symbol">)</a><a name="7276"> </a><a name="7277" class="Symbol">→</a><a name="7278"> </a><a name="7279" class="Symbol">(</a><a name="7280" href="#7266" class="Bound">A</a><a name="7281"> </a><a name="7282" class="Symbol">→</a><a name="7283"> </a><a name="7284" href="#6580" class="Datatype">⊤</a><a name="7285" class="Symbol">)</a><a name="7286"> </a><a name="7287" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#145" class="Datatype Operator">≡</a><a name="7288"> </a><a name="7289" class="Symbol">(</a><a name="7290" href="#7266" class="Bound">A</a><a name="7291"> </a><a name="7292" class="Symbol">→</a><a name="7293"> </a><a name="7294" href="#6580" class="Datatype">⊤</a><a name="7295" class="Symbol">)</a><a name="7296">
</a><a name="7299" href="#7249" class="Function">k-exp-eq</a><a name="7307"> </a><a name="7308" href="#7308" class="Bound">A</a><a name="7309"> </a><a name="7310" class="Symbol">=</a><a name="7311"> </a><a name="7312" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#364" class="Function">ap</a><a name="7314"> </a><a name="7315" class="Symbol">(λ</a><a name="7317"> </a><a name="7318" href="#7318" class="Bound">X</a><a name="7319"> </a><a name="7320" class="Symbol">→</a><a name="7321"> </a><a name="7322" href="#7308" class="Bound">A</a><a name="7323"> </a><a name="7324" class="Symbol">→</a><a name="7325"> </a><a name="7326" href="#7318" class="Bound">X</a><a name="7327" class="Symbol">)</a><a name="7328"> </a><a name="7329" href="#7209" class="Function">k-eq</a></code></pre>
<p>If we were working in a theory with computational univalence, coercion along <code>k-exp-eq</code> would reduce to precomposition with <span class="math">\(k\)</span>. In any case, we can manually show that this is the case propositionally by using path induction and the computational rule for <code>≈⇒≡</code>:</p>
<pre class="Agda"><code><a name="7609"></a><a name="7626" href="#7626" class="Function">ap-comp</a><a name="7633"> </a><a name="7634" class="Symbol">:</a><a name="7635"> </a><a name="7636" class="Symbol">∀</a><a name="7637"> </a><a name="7638" class="Symbol">{</a><a name="7639" href="#7639" class="Bound">i</a><a name="7640"> </a><a name="7641" href="#7641" class="Bound">k</a><a name="7642" class="Symbol">}{</a><a name="7644" href="#7644" class="Bound">A</a><a name="7645"> </a><a name="7646" class="Symbol">:</a><a name="7647"> </a><a name="7648" class="PrimitiveType">Set</a><a name="7651"> </a><a name="7652" href="#7639" class="Bound">i</a><a name="7653" class="Symbol">}{</a><a name="7655" href="#7655" class="Bound">X</a><a name="7656"> </a><a name="7657" href="#7657" class="Bound">X'</a><a name="7659"> </a><a name="7660" class="Symbol">:</a><a name="7661"> </a><a name="7662" class="PrimitiveType">Set</a><a name="7665"> </a><a name="7666" href="#7641" class="Bound">k</a><a name="7667" class="Symbol">}</a><a name="7668">
</a><a name="7679" class="Symbol">→</a><a name="7680"> </a><a name="7681" class="Symbol">(</a><a name="7682" href="#7682" class="Bound">p</a><a name="7683"> </a><a name="7684" class="Symbol">:</a><a name="7685"> </a><a name="7686" href="#7655" class="Bound">X</a><a name="7687"> </a><a name="7688" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#145" class="Datatype Operator">≡</a><a name="7689"> </a><a name="7690" href="#7657" class="Bound">X'</a><a name="7692" class="Symbol">)</a><a name="7693">
</a><a name="7704" class="Symbol">→</a><a name="7705"> </a><a name="7706" class="Symbol">(</a><a name="7707" href="#7707" class="Bound">f</a><a name="7708"> </a><a name="7709" class="Symbol">:</a><a name="7710"> </a><a name="7711" href="#7644" class="Bound">A</a><a name="7712"> </a><a name="7713" class="Symbol">→</a><a name="7714"> </a><a name="7715" href="#7655" class="Bound">X</a><a name="7716" class="Symbol">)</a><a name="7717">
</a><a name="7728" class="Symbol">→</a><a name="7729"> </a><a name="7730" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.univalence.html#379" class="Function">coerce</a><a name="7736"> </a><a name="7737" class="Symbol">(</a><a name="7738" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#364" class="Function">ap</a><a name="7740"> </a><a name="7741" class="Symbol">(λ</a><a name="7743"> </a><a name="7744" href="#7744" class="Bound">X</a><a name="7745"> </a><a name="7746" class="Symbol">→</a><a name="7747"> </a><a name="7748" href="#7644" class="Bound">A</a><a name="7749"> </a><a name="7750" class="Symbol">→</a><a name="7751"> </a><a name="7752" href="#7744" class="Bound">X</a><a name="7753" class="Symbol">)</a><a name="7754"> </a><a name="7755" href="#7682" class="Bound">p</a><a name="7756" class="Symbol">)</a><a name="7757"> </a><a name="7758" href="#7707" class="Bound">f</a><a name="7759">
</a><a name="7770" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#145" class="Datatype Operator">≡</a><a name="7771"> </a><a name="7772" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.univalence.html#379" class="Function">coerce</a><a name="7778"> </a><a name="7779" href="#7682" class="Bound">p</a><a name="7780"> </a><a name="7781" href="http://paolocapriotti.com/agda-base/v0.0.99/function.core.html#912" class="Function Operator">∘</a><a name="7782"> </a><a name="7783" href="#7707" class="Bound">f</a><a name="7784">
</a><a name="7787" href="#7626" class="Function">ap-comp</a><a name="7794"> </a><a name="7795" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#193" class="InductiveConstructor">refl</a><a name="7799"> </a><a name="7800" href="#7800" class="Bound">f</a><a name="7801"> </a><a name="7802" class="Symbol">=</a><a name="7803"> </a><a name="7804" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#193" class="InductiveConstructor">refl</a><a name="7808">
</a><a name="7812" href="#7812" class="Function">k-exp-eq-comp'</a><a name="7826"> </a><a name="7827" class="Symbol">:</a><a name="7828"> </a><a name="7829" class="Symbol">∀</a><a name="7830"> </a><a name="7831" class="Symbol">{</a><a name="7832" href="#7832" class="Bound">i</a><a name="7833" class="Symbol">}{</a><a name="7835" href="#7835" class="Bound">A</a><a name="7836"> </a><a name="7837" class="Symbol">:</a><a name="7838"> </a><a name="7839" class="PrimitiveType">Set</a><a name="7842"> </a><a name="7843" href="#7832" class="Bound">i</a><a name="7844" class="Symbol">}(</a><a name="7846" href="#7846" class="Bound">f</a><a name="7847"> </a><a name="7848" class="Symbol">:</a><a name="7849"> </a><a name="7850" href="#7835" class="Bound">A</a><a name="7851"> </a><a name="7852" class="Symbol">→</a><a name="7853"> </a><a name="7854" href="#6580" class="Datatype">⊤</a><a name="7855" class="Symbol">)</a><a name="7856">
</a><a name="7874" class="Symbol">→</a><a name="7875"> </a><a name="7876" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.univalence.html#379" class="Function">coerce</a><a name="7882"> </a><a name="7883" class="Symbol">(</a><a name="7884" href="#7249" class="Function">k-exp-eq</a><a name="7892"> </a><a name="7893" href="#7835" class="Bound">A</a><a name="7894" class="Symbol">)</a><a name="7895"> </a><a name="7896" href="#7846" class="Bound">f</a><a name="7897">
</a><a name="7915" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#145" class="Datatype Operator">≡</a><a name="7916"> </a><a name="7917" class="Symbol">λ</a><a name="7918"> </a><a name="7919" href="#7919" class="Bound">_</a><a name="7920"> </a><a name="7921" class="Symbol">→</a><a name="7922"> </a><a name="7923" href="#6600" class="InductiveConstructor">tt</a><a name="7925">
</a><a name="7928" href="#7812" class="Function">k-exp-eq-comp'</a><a name="7942"> </a><a name="7943" href="#7943" class="Bound">f</a><a name="7944"> </a><a name="7945" class="Symbol">=</a><a name="7946"> </a><a name="7947" href="#7626" class="Function">ap-comp</a><a name="7954"> </a><a name="7955" href="#7209" class="Function">k-eq</a><a name="7959"> </a><a name="7960" href="#7943" class="Bound">f</a><a name="7961">
</a><a name="7981" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.groupoid.html#147" class="Function Operator">·</a><a name="7982"> </a><a name="7983" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#364" class="Function">ap</a><a name="7985"> </a><a name="7986" class="Symbol">(λ</a><a name="7988"> </a><a name="7989" href="#7989" class="Bound">c</a><a name="7990"> </a><a name="7991" class="Symbol">→</a><a name="7992"> </a><a name="7993" href="#7989" class="Bound">c</a><a name="7994"> </a><a name="7995" href="http://paolocapriotti.com/agda-base/v0.0.99/function.core.html#912" class="Function Operator">∘</a><a name="7996"> </a><a name="7997" href="#7943" class="Bound">f</a><a name="7998" class="Symbol">)</a><a name="7999">
</a><a name="8024" class="Symbol">(</a><a name="8025" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.univalence.html#1252" class="Function">uni-coherence</a><a name="8038"> </a><a name="8039" class="Symbol">(</a><a name="8040" href="#6884" class="Function">k</a><a name="8041"> </a><a name="8042" href="http://paolocapriotti.com/agda-base/v0.0.99/sum.html#229" class="InductiveConstructor Operator">,</a><a name="8043"> </a><a name="8044" href="#6908" class="Function">k-we</a><a name="8048" class="Symbol">))</a></code></pre>
<p>Now it’s easy to conclude that <span class="math">\(A → ⊤\)</span> is a mere proposition (hence contractible): given functions <span class="math">\(f g : A → ⊤\)</span>, precomposing them with <span class="math">\(k\)</span> makes them both equal to <span class="math">\(λ \_ → \mathsf{tt}\)</span>. Since precomposing with <span class="math">\(k\)</span> is an equivalence by the computational rule above, <span class="math">\(f\)</span> must be equal to <span class="math">\(g\)</span>.</p>
<pre class="Agda"><code><a name="8356"></a><a name="8373" href="#8373" class="Function">prop-exp-⊤</a><a name="8383"> </a><a name="8384" class="Symbol">:</a><a name="8385"> </a><a name="8386" class="Symbol">∀</a><a name="8387"> </a><a name="8388" class="Symbol">{</a><a name="8389" href="#8389" class="Bound">i</a><a name="8390" class="Symbol">}{</a><a name="8392" href="#8392" class="Bound">A</a><a name="8393"> </a><a name="8394" class="Symbol">:</a><a name="8395"> </a><a name="8396" class="PrimitiveType">Set</a><a name="8399"> </a><a name="8400" href="#8389" class="Bound">i</a><a name="8401" class="Symbol">}</a><a name="8402"> </a><a name="8403" class="Symbol">→</a><a name="8404"> </a><a name="8405" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.hlevel.core.html#546" class="Function">prop</a><a name="8409"> </a><a name="8410" class="Symbol">(</a><a name="8411" href="#8392" class="Bound">A</a><a name="8412"> </a><a name="8413" class="Symbol">→</a><a name="8414"> </a><a name="8415" href="#6580" class="Datatype">⊤</a><a name="8416" class="Symbol">)</a><a name="8417">
</a><a name="8420" href="#8373" class="Function">prop-exp-⊤</a><a name="8430"> </a><a name="8431" class="Symbol">{</a><a name="8432" href="#8432" class="Bound">i</a><a name="8433" class="Symbol">}{</a><a name="8435" href="#8435" class="Bound">A</a><a name="8436" class="Symbol">}</a><a name="8437"> </a><a name="8438" href="#8438" class="Bound">f</a><a name="8439"> </a><a name="8440" href="#8440" class="Bound">g</a><a name="8441"> </a><a name="8442" class="Symbol">=</a><a name="8443"> </a><a name="8444" href="http://paolocapriotti.com/agda-base/v0.0.99/equality.core.html#364" class="Function">ap</a><a name="8446"> </a><a name="8447" href="http://paolocapriotti.com/agda-base/v0.0.99/sum.html#245" class="Function">proj₁</a><a name="8452">
</a><a name="8457" class="Symbol">(</a><a name="8458"> </a><a name="8459" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.hlevel.core.html#1164" class="Function">contr⇒prop</a><a name="8469"> </a><a name="8470" class="Symbol">(</a><a name="8471" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.univalence.html#442" class="Function">coerce-equiv</a><a name="8483"> </a><a name="8484" class="Symbol">(</a><a name="8485" href="#7249" class="Function">k-exp-eq</a><a name="8493"> </a><a name="8494" href="#8435" class="Bound">A</a><a name="8495" class="Symbol">)</a><a name="8496"> </a><a name="8497" class="Symbol">(λ</a><a name="8499"> </a><a name="8500" href="#8500" class="Bound">_</a><a name="8501"> </a><a name="8502" class="Symbol">→</a><a name="8503"> </a><a name="8504" href="#6600" class="InductiveConstructor">tt</a><a name="8506" class="Symbol">))</a><a name="8508">
</a><a name="8517" class="Symbol">(</a><a name="8518" href="#8438" class="Bound">f</a><a name="8519"> </a><a name="8520" href="http://paolocapriotti.com/agda-base/v0.0.99/sum.html#229" class="InductiveConstructor Operator">,</a><a name="8521"> </a><a name="8522" href="#7812" class="Function">k-exp-eq-comp'</a><a name="8536"> </a><a name="8537" href="#8438" class="Bound">f</a><a name="8538" class="Symbol">)</a><a name="8539">
</a><a name="8548" class="Symbol">(</a><a name="8549" href="#8440" class="Bound">g</a><a name="8550"> </a><a name="8551" href="http://paolocapriotti.com/agda-base/v0.0.99/sum.html#229" class="InductiveConstructor Operator">,</a><a name="8552"> </a><a name="8553" href="#7812" class="Function">k-exp-eq-comp'</a><a name="8567"> </a><a name="8568" href="#8440" class="Bound">g</a><a name="8569" class="Symbol">)</a><a name="8570"> </a><a name="8571" class="Symbol">)</a><a name="8572">
</a><a name="8576" href="#8576" class="Function">contr-exp-⊤</a><a name="8587"> </a><a name="8588" class="Symbol">:</a><a name="8589"> </a><a name="8590" class="Symbol">∀</a><a name="8591"> </a><a name="8592" class="Symbol">{</a><a name="8593" href="#8593" class="Bound">i</a><a name="8594" class="Symbol">}{</a><a name="8596" href="#8596" class="Bound">A</a><a name="8597"> </a><a name="8598" class="Symbol">:</a><a name="8599"> </a><a name="8600" class="PrimitiveType">Set</a><a name="8603"> </a><a name="8604" href="#8593" class="Bound">i</a><a name="8605" class="Symbol">}</a><a name="8606"> </a><a name="8607" class="Symbol">→</a><a name="8608"> </a><a name="8609" href="http://paolocapriotti.com/agda-base/v0.0.99/hott.hlevel.core.html#451" class="Function">contr</a><a name="8614"> </a><a name="8615" class="Symbol">(</a><a name="8616" href="#8596" class="Bound">A</a><a name="8617"> </a><a name="8618" class="Symbol">→</a><a name="8619"> </a><a name="8620" href="#6580" class="Datatype">⊤</a><a name="8621" class="Symbol">)</a><a name="8622">
</a><a name="8625" href="#8576" class="Function">contr-exp-⊤</a><a name="8636"> </a><a name="8637" class="Symbol">=</a><a name="8638"> </a><a name="8639" class="Symbol">(λ</a><a name="8641"> </a><a name="8642" href="#8642" class="Bound">_</a><a name="8643"> </a><a name="8644" class="Symbol">→</a><a name="8645"> </a><a name="8646" href="#6600" class="InductiveConstructor">tt</a><a name="8648" class="Symbol">)</a><a name="8649"> </a><a name="8650" href="http://paolocapriotti.com/agda-base/v0.0.99/sum.html#229" class="InductiveConstructor Operator">,</a><a name="8651"> </a><a name="8652" href="#8373" class="Function">prop-exp-⊤</a><a name="8662"> </a><a name="8663" class="Symbol">_</a></code></pre>
</div>
</article>
<article>
<header>
<h1 class="entry-title"><a href="/blog/2013/04/03/free-applicative-functors/">Free Applicative Functors</a></h1>
<p class="meta">
<time datetime="2013-04-03" pubdate>Apr 3<span>rd</span>, 2013</time>
</p>
</header>
<div class="entry-content">
<p>After my post on <a href="/blog/2012/04/27/applicative-option-parser/">option parsers</a> with applicative functors, I’ve been working on a paper to develop the idea of “free applicative” contained in that post.</p>
<p>A draft of the paper, joint work with <a href="http://akaposi.web.elte.hu/">Ambrus Kaposi</a>, has been submitted to <a href="http://www.icfpconference.org/icfp2013/">ICFP 2013</a>, and is available <a href="/assets/applicative.pdf">here</a>.</p>
</div>
</article>
<article>
<header>
<h1 class="entry-title"><a href="/blog/2013/02/20/families-and-fibrations/">Families and fibrations</a></h1>
<p class="meta">
<time datetime="2013-02-20" pubdate>Feb 20<span>th</span>, 2013</time>
</p>
</header>
<div class="entry-content">
<h2 id="introduction">Introduction</h2>
<p>The notion of family of “objects” indexed over an object of the same type is ubiquitous is mathematics and computer science.</p>
<p>It appears everywhere in topology and algebraic geometry, in the form of <em>bundles</em>, <em>covering maps</em>, or, more generally, <em>fibrations</em>.</p>
<p>In type theory, it is the fundamental idea captured by the notion of <em>dependent type</em>, on which Martin-Löf intuitionistic type theory is based.</p>
<h2 id="definition">Definition</h2>
<p>Restricting ourselves to <span class="math">\(\mathrm{Set}\)</span>, the category of sets, for the time being (and ignoring issues of size), it is straightforward to give a formal definition of what a <em>family</em> of sets is:</p>
<p>Given a set <code>A</code>, a family over <code>A</code> is a function from <code>A</code> to the objects of the category of sets (or equivalently, on the other side of the adjunction, a functor from <code>A</code> regarded as a discrete category to <span class="math">\(\mathrm{Set}\)</span>).</p>
<p>This is a perfectly valid definition, but it has two problems:</p>
<ol style="list-style-type: decimal">
<li><p>It can be awkward to work with functions between objects of different “sorts” (like sets and universes).</p></li>
<li><p>It is not clear how to generalize the idea to other categories, like <span class="math">\(\mathrm{Top}\)</span> (the category of topological spaces and continuous maps), for example. In fact, we would like a family of spaces to be “continuous” in some sense, but in order for that to make sense, we would need to define a topology on the class of topological spaces.</p></li>
</ol>
<h2 id="display-maps">Display maps</h2>
<p>Fortunately, there is a very simple construction that helps bringing this definition to a form which is much easier to work with.</p>
<p>Let’s start with a family of sets <code>B</code> over <code>A</code>, defined as above: <code>B : A → Set</code>.</p>
<p>Define the “total space” of the family as the disjoint union (or dependent sum) of all the sets of the family (I’ll use type theoretic notation from now on):</p>
<pre><code>E = Σ (a : A) . B a</code></pre>
<p>The <em>fibration</em> (or <em>display map</em>) associated to the family <code>B</code> is defined to be the first projection:</p>
<pre><code>proj₁ : E → A</code></pre>
<p>So far, we haven’t done very much. The interesting observation is that we can always recover a family of sets from any function <code>E → A</code>.</p>
<p>In fact, suppose that now <code>E</code> is any set, and <code>p : E → A</code> any function. We can define a family of sets:</p>
<pre><code>B : A → Set
B a = p ⁻¹ a</code></pre>
<p>as the function that associates to each point in <code>A</code>, its inverse image (or fiber) in <code>E</code>.</p>
<p>It is now straightforward to check that these two mappings between families and fibrations are inverses of one another.</p>
<p>Intuitively, given a family <code>B</code>, the corresponding fibration maps each element of all possible sets in the family to its “index” in <code>A</code>. Viceversa, given a fibration <code>p : E → A</code>, the corresponding family is just the family of fibers of <code>p</code>.</p>
<p><a href="/pages/display/display.html">Here</a> is formalization in Agda of this correspondence as an isomorphism between families and fibrations. This uses <a href="https://github.com/pcapriotti/agda-base">agda-base</a> instead of the standard library, as it needs univalence in order to make the isomorphism explicit.</p>
<h2 id="examples-of-constructions">Examples of constructions</h2>
<p>Once we understand how families and fibrations are really two views of the same concept, we can look at a number of constructions for families, and check how they look like in the world of fibrations.</p>
<h3 id="dependent-sum">Dependent sum</h3>
<p>The simplest construction is the total space:</p>
<pre><code>E = Σ (x : A). B x</code></pre>
<p>As we already know, this corresponds to the domain of the associated fibration.</p>
<h3 id="dependent-product">Dependent product</h3>
<p>Given a family of sets <code>B</code> over <code>A</code>, a <em>choice function</em> is a function that assigns to each element <code>x</code> of <code>A</code>, an element <code>y</code> of <code>B x</code>. This is called a <em>dependent function</em> in type theory.</p>
<p>The corresponding notion for a fibration <code>p : E → A</code> is a function <code>s : A → E</code> such that for each <code>x : A</code>, the index of <code>s x</code> is exactly <code>x</code>. In other words, <code>p ∘ s ≡ id</code>, i.e. <code>s</code> is a <em>section</em> of <code>p</code>.</p>
<p>The set of such sections is called the dependent product of the family <code>B</code>.</p>
<h3 id="pullbacks">Pullbacks</h3>
<p>Let <code>A</code> and <code>A'</code> be two sets, and <code>B</code> a family over <code>A</code>. Suppose we have a function</p>
<pre><code>r : A' → A</code></pre>
<p>We can easily define a family <code>B'</code> over <code>A'</code> by composing with <code>r</code>:</p>
<pre><code>B' : A' → Set
B' x = B (r x)</code></pre>
<p>What does the fibration <code>p' : E' → A'</code> associated to <code>B'</code> look like in terms of the fibration <code>p : E → A</code> associated to <code>B</code>?</p>
<p>Well, given an element <code>b</code> in the total space of <code>B'</code>, <code>b</code> is going to be in <code>B' x</code> for some <code>x : A'</code>. Since <code>B' x ≡ B (r x)</code> by definition, <code>b</code> can also be regarded as an element of the total space of <code>B</code>. So we have a map <code>s : E' → E</code>, and we can draw the following diagram:</p>
<p><span class="math">\[
\newcommand{\ra}[1]{\kern-1.5ex\xrightarrow{\ \ #1\ \ }\phantom{}\kern-1.5ex}
\newcommand{\ras}[1]{\kern-1.5ex\xrightarrow{\ \ \smash{#1}\ \ }\phantom{}\kern-1.5ex}
\newcommand{\da}[1]{\bigg\downarrow\raise.5ex\rlap{\scriptstyle#1}}
\begin{array}{c}
E' &amp; \ra{s} &amp; E \\
\da{p'} &amp; &amp; \da{p} \\
A' &amp; \ra{r} &amp; A \\
\end{array}
\]</span></p>
<p>The commutativity of this diagram follows from the immediate observation that the index above <code>s b</code> is exactly <code>r x</code>.</p>
<p>Now, given elements <code>x : A'</code>, and <code>b : E</code>, saying that <code>p b ≡ r x</code> is equivalent to saying that <code>b</code> is in <code>B (r x)</code>. In that case, <code>b</code> can be regarded as an element of <code>B' x</code>, which means that there exists a <code>b'</code> in <code>E'</code> such that <code>p' b' ≡ x</code> and <code>s b' ≡ b</code>.</p>
<p>What this says is that the above diagram is a pullback square.</p>
<h2 id="adjoints">Adjoints</h2>
<p>It is important to note that the previous constructions are related in interesting ways.</p>
<p>Let’s look at a simple special case of the pullback construction, i.e. when <code>B</code> is a trivial family of just one element. That means that the display map <code>p</code> associated to <code>B</code> is the canonical map</p>
<pre><code>p : B → 1</code></pre>
<p>So, if <code>A'</code> is any other type, we get that the pullback of <code>p</code> along the unique map <code>r : A' → 1</code> is the product <code>B × A</code>.</p>
<p>This defines a functor</p>
<p><span class="math">\[
A^\ast : \mathrm{Set} → \mathrm{Set}/A
\]</span></p>
<p>where <span class="math">\(\mathrm{Set}/A\)</span> denotes the slice category of sets over <code>A</code>. Furthermore, the dependent product and dependent sum constructions defined above give rise to functors:</p>
<p><span class="math">\[
Σ_A, Π_A : \mathrm{Set}/A → \mathrm{Set}
\]</span></p>
<p>Now, it is clear that, given a fibration <code>p : X → A</code> and a set <code>Y</code>, functions <code>X → Y</code> are the same as morphisms <code>X → Y × A</code> in the slice category. So <span class="math">\(Σ_A\)</span> is left adjoint to <span class="math">\(A^\ast\)</span>.</p>
<p>Dually, functions from <code>Y</code> to the set of sections of <code>p</code> correspond to functions <code>Y × A → X</code> in the slice category, thus giving an adjuction between <span class="math">\(A^*\)</span> and <span class="math">\(Π_A\)</span>.</p>
<p>So we have the following chain of adjunctions:</p>
<p><span class="math">\[
Σ_A \vdash A^* \vdash Π_A
\]</span></p>
<h2 id="conclusion">Conclusion</h2>
<p>The correspondence between indexed families and fibrations exemplified here extends well beyond the category of sets, and can be abstracted using the notions of Cartesian morphisms and fibred categories.</p>
<p>In type theory, it is useful to think of this correspondence when working with models of dependently typed theories in locally cartesian closed categories, and I hope that the examples given here show why slice categories and pullback functors play an important role in that setting.</p>
</div>
</article>
<article>
<header>
<h1 class="entry-title"><a href="/blog/2012/06/04/continuation-based-relative-time-frp/">Continuation-based relative-time FRP</a></h1>
<p class="meta">
<time datetime="2012-06-04" pubdate>Jun 4<span>th</span>, 2012</time>
</p>
</header>
<div class="entry-content">
<p>In a <a href="http://paolocapriotti.com/blog/2012/01/18/reinversion-of-control/">previous post</a> I showed how it is possible to write asynchronous code in a direct style using the <code>ContT</code> monad. Here, I’ll extend the idea further and present an implementation of a very simple FRP library based on continuations.</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt;</span> <span class="ot">{-# LANGUAGE DoRec, BangPatterns #-}</span>
<span class="ot">&gt;</span> <span class="kw">import </span><span class="dt">Control.Applicative</span>
<span class="ot">&gt;</span> <span class="kw">import </span><span class="dt">Control.Monad</span>
<span class="ot">&gt;</span> <span class="kw">import </span><span class="dt">Control.Monad.IO.Class</span>
<span class="ot">&gt;</span> <span class="kw">import </span><span class="dt">Data.IORef</span>
<span class="ot">&gt;</span> <span class="kw">import </span><span class="dt">Data.Monoid</span>
<span class="ot">&gt;</span> <span class="kw">import </span><span class="dt">Data.Void</span></code></pre>
<h2 id="monadic-events">Monadic events</h2>
<p>Let’s start by defining a callback-based <code>Event</code> type:</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt;</span> <span class="kw">newtype</span> <span class="dt">Event</span> a <span class="fu">=</span> <span class="dt">Event</span> {<span class="ot"> on ::</span> (a <span class="ot">-&gt;</span> <span class="dt">IO</span> ()) <span class="ot">-&gt;</span> <span class="dt">IO</span> <span class="dt">Dispose</span> }</code></pre>
<p>A value of type <code>Event a</code> represents a stream of values of type <code>a</code>, each occurring some time in the future. The <code>on</code> function connects a callback to an event, and returns an object of type <code>Dispose</code>, which can be used to disconnect from the event:</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt;</span> <span class="kw">newtype</span> <span class="dt">Dispose</span> <span class="fu">=</span> <span class="dt">Dispose</span> {<span class="ot"> dispose ::</span> <span class="dt">IO</span> () }
<span class="ot">&gt;</span>
<span class="ot">&gt;</span> <span class="kw">instance</span> <span class="dt">Monoid</span> <span class="dt">Dispose</span> <span class="kw">where</span>
<span class="ot">&gt;</span> mempty <span class="fu">=</span> <span class="dt">Dispose</span> (return ())
<span class="ot">&gt;</span> mappend d1 d2 <span class="fu">=</span> <span class="dt">Dispose</span> <span class="fu">$</span> <span class="kw">do</span>
<span class="ot">&gt;</span> dispose d1
<span class="ot">&gt;</span> dispose d2</code></pre>
<p>The interesting thing about this <code>Event</code> type is that, like the simpler variant we defined in the above post, it forms a monad:</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt;</span> <span class="kw">instance</span> <span class="dt">Monad</span> <span class="dt">Event</span> <span class="kw">where</span></code></pre>
<p>First of all, given a value of type <code>a</code>, we can create an event occurring “now” and never again:</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt;</span> return x <span class="fu">=</span> <span class="dt">Event</span> <span class="fu">$</span> \k <span class="ot">-&gt;</span> k x <span class="fu">&gt;&gt;</span> return mempty</code></pre>
<p>Note that the notion of “time” for an <code>Event</code> is relative.</p>
<p>All time-dependent notions about <code>Events</code> are formulated in terms of a particular “zero” time, but this origin of times is not explicitly specified.</p>
<p>This makes sense, because, even though the definition of <code>Event</code> uses the <code>IO</code> monad, an <code>Event</code> object, in itself, is an immutable value, and can be reused multiple times, possibly with different starting times.</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt;</span> e <span class="fu">&gt;&gt;=</span> f <span class="fu">=</span> <span class="dt">Event</span> <span class="fu">$</span> \k <span class="ot">-&gt;</span> <span class="kw">do</span>
<span class="ot">&gt;</span> dref <span class="ot">&lt;-</span> newIORef mempty
<span class="ot">&gt;</span> addD dref e <span class="fu">$</span> \x <span class="ot">-&gt;</span>
<span class="ot">&gt;</span> addD dref (f x) k
<span class="ot">&gt;</span> return <span class="fu">.</span> <span class="dt">Dispose</span> <span class="fu">$</span>
<span class="ot">&gt;</span> readIORef dref <span class="fu">&gt;&gt;=</span> dispose
<span class="ot">&gt;</span>
<span class="ot">&gt; addD ::</span> <span class="dt">IORef</span> <span class="dt">Dispose</span> <span class="ot">-&gt;</span> <span class="dt">Event</span> a <span class="ot">-&gt;</span> (a <span class="ot">-&gt;</span> <span class="dt">IO</span> ()) <span class="ot">-&gt;</span> <span class="dt">IO</span> ()
<span class="ot">&gt;</span> addD d e act <span class="fu">=</span> <span class="kw">do</span>
<span class="ot">&gt;</span> d' <span class="ot">&lt;-</span> on e act
<span class="ot">&gt;</span> modifyIORef d (<span class="ot">`mappend`</span> d')</code></pre>
<p>The definition of <code>&gt;&gt;=</code> is slightly more involved.</p>
<p>We call the function <code>f</code> every time an event occurs, and we connect to the resulting event each time using the helper function <code>addD</code>, accumulating the corresponding <code>Dispose</code> object in an <code>IORef</code>.</p>
<p>The resulting <code>Dispose</code> object is a function that reads the <code>IORef</code> accumulator and calls <code>dispose</code> on that.</p>
<div class="figure">
<img src="/images/event_bind.png" alt="Monadic bind" /><p class="caption">Monadic bind</p>
</div>
<p>As the diagram shows, the resulting event <code>e &gt;&gt;= f</code> includes occurrences of all the events originating from the occurrences of the initial event <code>e</code>.</p>
<h2 id="event-union">Event union</h2>
<p>Classic FRP comes with a number of combinators to manipulate event streams. One of the most important is event union, which consists in merging two or more event streams into a single one.</p>
<p>In our case, event union can be implemented very easily as an <code>Alternative</code> instance:</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt;</span> <span class="kw">instance</span> <span class="dt">Functor</span> <span class="dt">Event</span> <span class="kw">where</span>
<span class="ot">&gt;</span> fmap <span class="fu">=</span> liftM
<span class="ot">&gt;</span>
<span class="ot">&gt;</span> <span class="kw">instance</span> <span class="dt">Applicative</span> <span class="dt">Event</span> <span class="kw">where</span>
<span class="ot">&gt;</span> pure <span class="fu">=</span> return
<span class="ot">&gt;</span> (<span class="fu">&lt;*&gt;</span>) <span class="fu">=</span> ap
<span class="ot">&gt;</span>
<span class="ot">&gt;</span> <span class="kw">instance</span> <span class="dt">Alternative</span> <span class="dt">Event</span> <span class="kw">where</span>
<span class="ot">&gt;</span> empty <span class="fu">=</span> <span class="dt">Event</span> <span class="fu">$</span> \_ <span class="ot">-&gt;</span> return mempty
<span class="ot">&gt;</span> e1 <span class="fu">&lt;|&gt;</span> e2 <span class="fu">=</span> <span class="dt">Event</span> <span class="fu">$</span> \k <span class="ot">-&gt;</span> <span class="kw">do</span>
<span class="ot">&gt;</span> d1 <span class="ot">&lt;-</span> on e1 k
<span class="ot">&gt;</span> d2 <span class="ot">&lt;-</span> on e2 k
<span class="ot">&gt;</span> return <span class="fu">$</span> d1 <span class="fu">&lt;&gt;</span> d2</code></pre>
<p>An empty <code>Event</code> never invokes its callback, and the union of two events is implemented by connecting a callback to both events simultaneously.</p>
<h2 id="other-combinators">Other combinators</h2>
<p>We need an extra primitive combinator in terms of which all other FRP combinators can be implemented using the <code>Monad</code> and <code>Alternative</code> instances.</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt; once ::</span> <span class="dt">Event</span> a <span class="ot">-&gt;</span> <span class="dt">Event</span> a
<span class="ot">&gt;</span> once e <span class="fu">=</span> <span class="dt">Event</span> <span class="fu">$</span> \k <span class="ot">-&gt;</span> <span class="kw">do</span>
<span class="ot">&gt;</span> rec d <span class="ot">&lt;-</span> on e <span class="fu">$</span> \x <span class="ot">-&gt;</span> <span class="kw">do</span>
<span class="ot">&gt;</span> dispose d
<span class="ot">&gt;</span> k x
<span class="ot">&gt;</span> return d</code></pre>
<p>The <code>once</code> combinator truncates an event stream at its first occurrence. It can be used to implement a number of different combinators by recursion.</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt; accumE ::</span> a <span class="ot">-&gt;</span> <span class="dt">Event</span> (a <span class="ot">-&gt;</span> a) <span class="ot">-&gt;</span> <span class="dt">Event</span> a
<span class="ot">&gt;</span> accumE x e <span class="fu">=</span> <span class="kw">do</span>
<span class="ot">&gt;</span> f <span class="ot">&lt;-</span> once e
<span class="ot">&gt;</span> <span class="kw">let</span> <span class="fu">!</span>x' <span class="fu">=</span> f x
<span class="ot">&gt;</span> pure x' <span class="fu">&lt;|&gt;</span> accumE x' e
<span class="ot">&gt;</span>
<span class="ot">&gt; takeE ::</span> <span class="dt">Int</span> <span class="ot">-&gt;</span> <span class="dt">Event</span> a <span class="ot">-&gt;</span> <span class="dt">Event</span> a
<span class="ot">&gt;</span> takeE <span class="dv">0</span> _ <span class="fu">=</span> empty
<span class="ot">&gt;</span> takeE <span class="dv">1</span> e <span class="fu">=</span> once e
<span class="ot">&gt;</span> takeE n e <span class="fu">|</span> n <span class="fu">&gt;</span> <span class="dv">1</span> <span class="fu">=</span> <span class="kw">do</span>
<span class="ot">&gt;</span> x <span class="ot">&lt;-</span> once e
<span class="ot">&gt;</span> pure x <span class="fu">&lt;|&gt;</span> takeE (n <span class="fu">-</span> <span class="dv">1</span>) e
<span class="ot">&gt;</span> takeE _ _ <span class="fu">=</span> error <span class="st">&quot;takeE: n must be non-negative&quot;</span>
<span class="ot">&gt;</span>
<span class="ot">&gt; dropE ::</span> <span class="dt">Int</span> <span class="ot">-&gt;</span> <span class="dt">Event</span> a <span class="ot">-&gt;</span> <span class="dt">Event</span> a
<span class="ot">&gt;</span> dropE n e <span class="fu">=</span> replicateM_ n (once e) <span class="fu">&gt;&gt;</span> e</code></pre>
<h2 id="behaviors-and-side-effects">Behaviors and side effects</h2>
<p>We address behaviors and side effects the same way, using <code>IO</code> actions, and a <code>MonadIO</code> instance for <code>Event</code>:</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt;</span> <span class="kw">instance</span> <span class="dt">MonadIO</span> <span class="dt">Event</span> <span class="kw">where</span>
<span class="ot">&gt;</span> liftIO m <span class="fu">=</span> <span class="dt">Event</span> <span class="fu">$</span> \k <span class="ot">-&gt;</span> <span class="kw">do</span>
<span class="ot">&gt;</span> m <span class="fu">&gt;&gt;=</span> k
<span class="ot">&gt;</span> return mempty
<span class="ot">&gt;</span>
<span class="ot">&gt;</span> <span class="kw">newtype</span> <span class="dt">Behavior</span> a <span class="fu">=</span> <span class="dt">Behavior</span> {<span class="ot"> valueB ::</span> <span class="dt">IO</span> a }
<span class="ot">&gt;</span>
<span class="ot">&gt; getB ::</span> <span class="dt">Behavior</span> a <span class="ot">-&gt;</span> <span class="dt">Event</span> a
<span class="ot">&gt;</span> getB <span class="fu">=</span> liftIO <span class="fu">.</span> valueB</code></pre>
<p>Now we can implement something like the <code>apply</code> combinator in <a href="http://www.haskell.org/haskellwiki/Reactive-banana">reactive-banana</a>:</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt; apply ::</span> <span class="dt">Behavior</span> (a <span class="ot">-&gt;</span> b) <span class="ot">-&gt;</span> <span class="dt">Event</span> a <span class="ot">-&gt;</span> <span class="dt">Event</span> b
<span class="ot">&gt;</span> apply b e <span class="fu">=</span> <span class="kw">do</span>
<span class="ot">&gt;</span> x <span class="ot">&lt;-</span> e
<span class="ot">&gt;</span> f <span class="ot">&lt;-</span> getB b
<span class="ot">&gt;</span> return <span class="fu">$</span> f x</code></pre>
<p>Events can also perform arbitrary <code>IO</code> actions, which is necessary to actually connect an <code>Event</code> to user-visible effects:</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt; log ::</span> <span class="dt">Show</span> a <span class="ot">=&gt;</span> <span class="dt">Event</span> a <span class="ot">-&gt;</span> <span class="dt">Event</span> ()
<span class="ot">&gt;</span> log e <span class="fu">=</span> e <span class="fu">&gt;&gt;=</span> liftIO <span class="fu">.</span> print</code></pre>
<h2 id="executing-event-descriptions">Executing event descriptions</h2>
<p>An entire GUI program can be expressed as an <code>Event</code> value, usually by combining a number of basic events using the <code>Alternative</code> instance.</p>
<p>A complete program can be run with:</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt; runEvent ::</span> <span class="dt">Event</span> <span class="dt">Void</span> <span class="ot">-&gt;</span> <span class="dt">IO</span> ()
<span class="ot">&gt;</span> runEvent e <span class="fu">=</span> void <span class="fu">$</span> on e absurd
<span class="ot">&gt;</span>
<span class="ot">&gt; runEvent_ ::</span> <span class="dt">Event</span> a <span class="ot">-&gt;</span> <span class="dt">IO</span> ()
<span class="ot">&gt;</span> runEvent_ <span class="fu">=</span> runEvent <span class="fu">.</span> (<span class="fu">&gt;&gt;</span> empty)</code></pre>
<h2 id="underlying-assumptions">Underlying assumptions</h2>
<p>For this simple system to work, events need to possess certain properties that guarantee that our implementations of the basic combinators make sense.</p>
<p>First of all, callbacks must be invoked sequentially, in the order of occurrence of their respective events.</p>
<p>Furthermore, we assume that callbacks for the same event (or simultaneous events) will be called in the order of connection.</p>
<p>Many event-driven frameworks provide those guarantees directly. For those that do not, a driver can be written converting underlying events to <code>Event</code> values satisfying the required ordering properties.</p>
<h2 id="conclusion">Conclusion</h2>
<p>It’s not immediately clear whether this approach can scale to real-world GUI applications.</p>
<p>Although the implementation presented here is quite simplistic, it could certainly be made more efficient by, for example, making <code>Dispose</code> stricter, or adding more information to <code>Event</code> to simplify some common special cases.</p>
<p>This continuation-based API is a lot more powerful than the usual FRP combinator set. The <code>Event</code> type combines the functionalities of both the classic <code>Event</code> and <code>Behavior</code> types, and it offers a wider interface (<code>Monad</code> rather than only <code>Applicative</code>).</p>
<p>On the other hand, it is a lot less safe, in a way, since it allows to freely mix <code>IO</code> actions with event descriptions, and doesn’t enforce a definite separation between the two. Libraries like reactive-banana do so by distinguishing beween “network descriptions” and events/behaviors.</p>
<p>Finally, there is really no sharing of intermediate events, so expensive computations occurring, say, inside an <code>accumE</code> can end up being unnecessarily performed more than once.</p>
<p>This is not just an implementation issue, but a consequence of the strict equality model that this FRP formulation employs. Even if two events are identical, they might not actually behave the same when they are used, because they are going to be “activated” at different times.</p>
</div>
</article>
<article>
<header>
<h1 class="entry-title"><a href="/blog/2012/05/29/pipes-2.0-vs-pipes-core/">Pipes 2.0 vs pipes-core</a></h1>
<p class="meta">
<time datetime="2012-05-29" pubdate>May 29<span>th</span>, 2012</time>
</p>
</header>
<div class="entry-content">
<p>With the release of <a href="http://hackage.haskell.org/package/pipes-2.0.0">pipes 2.0</a> by <a href="http://www.haskellforall.com/">Gabriel Gonzalez</a>, I feel it’s time to address the question of whether my fork will eventually be merged or not.</p>
<p>The short answer is no, I will continue to maintain my separate incarnation <a href="http://hackage.haskell.org/package/pipes-core">pipes-core</a>. In this post, I will discuss the reasoning behind this decision, and hopefully explain the various trade-offs that the two libraries make.</p>
<h2 id="the-issue-with-termination">The issue with termination</h2>
<p><a href="http://hackage.haskell.org/package/pipes-1.0.2">pipes 1.0</a> can be quite accurately described as “composable monadic stream processors”. “Composable” alludes to horizontal composition (i.e. the <code>Category</code> instance), while “monadic” refers to vertical composition.</p>
<p>The existence of a <code>Monad</code> instance has a number of consequences, the most important being the fact that pipes can carry a “return value”, and, in particular, they can terminate.</p>
<p>The fact that pipes can terminate poses the greatest challenge when reasoning about the properties of (horizontal) composition, but termination is also one of the nicest features of pipes, so we want to deal with this difficulty appropriately.</p>
<p>Termination implies that any pipe has to deal somehow with the fact that its upstream pipe can exit before yielding a value, which basically means that an <code>await</code> can fail.</p>
<p>Gabriel’s pipes address this issue by simply “propagating termination downstream”. A pipe awaiting on a terminated pipe is forcibly terminated itself, and the upstream return value is returned.</p>
<p>My <a href="http://paolocapriotti.com/blog/2012/02/02/guarded-pipes/">guarded pipes</a> idea (later integrated into pipes-core), proposes a new primitive</p>
<pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="ot">tryAwait ::</span> <span class="dt">Pipe</span> a b m (<span class="dt">Maybe</span> a)</code></pre>
<p>that returns <code>Nothing</code> when upstream terminates before providing a value.</p>
<p>Using <code>tryAwait</code>, a pipe can then <em>handle</em> a failure caused by termination, and either return a value, or use the upstream value (the latter can be accomplished by simply awaiting again).</p>
<h2 id="exception-handling">Exception handling</h2>
<p>Once you realize that pipes should be able to handle failure on <code>await</code>, it becomes very natural to extend the idea to other kinds of failure.</p>
<p>That’s exactly the rationale behind pipes-core. It introduces slightly more involved primitives that take into account the fact that actions in the base monad, as well as pipes themselves, can throw an exception at any time.</p>
<p>One very interesting consequence of built-in exception handling is that the “guarded pipes” concept can be integrated seamlessly by introducing a special <code>BrokenPipe</code> exception.</p>
<p>The exception handling implementation in pipes-core works in any monad, and deals with asynchronous exceptions correctly. Of course, actual exceptions thrown from Haskell code can only be caught when the base monad is <code>IO</code>.</p>
<h2 id="what-about-finalization">What about finalization?</h2>
<p>Since all the finalization primitives in <code>Control.Exception</code> are implemented on top of exception handling primitives like <code>catch</code> and <code>mask</code>, I initially believed that finalization would follow automatically from exception handling capabilities in pipes.</p>
<p>Unfortunately, there is a fundamental operational difference between <code>IO</code> and <code>Pipe</code>, which makes exception handling alone insufficient to guarantee finalization of resources.</p>
<p>The problem is that some of the pipes in a pipeline are not guaranteed to be executed at all. In fact, a pipe only plays a role in pipeline execution if its downstream pipe awaits at some point (or if it is the last one).</p>
<p>The same applies to “portions” of pipes, so a pipe can execute partially, and then be completely forgotten, even if no exceptional condition occurs.</p>
<p>After a number of failed attempts (including the broken <a href="http://hackage.haskell.org/package/pipes-core-0.0.1">0.0.1</a> release of pipes-core), I realized that Gabriel’s <a href="http://www.haskellforall.com/2012/03/haskell-for-purists-pipe-finalization.html">finalizer passing</a> idea was the right one, and used it to replace my flawed <code>ensure</code> primitive.</p>
<h2 id="balancing-safety-and-dynamicity">Balancing safety and dynamicity</h2>
<p>The question remains of how to guarantee that a pipe never awaits again after its upstream terminated.</p>
<p>My solution is <strong>dynamic</strong>: if upstream terminated because of an exception (that has been handled), just throw the exception again on await; if upstream terminated normally, throw a <code>BrokenPipe</code> exception.</p>
<p>Gabriel’s solution is <strong>static</strong>: a pipe is not allowed to await again after termination, and the invariant is enforced by the types.</p>
<p>The static solution has obvious advantages, but, on closer inspection, it reveals a number of downsides:</p>
<ol style="list-style-type: decimal">
<li>It prevents <code>Pipe</code> from forming a <code>Monad</code>; the solution implemented in <code>pipes</code> 2.0 is to separate the <code>Monad</code> instance from the <code>Category</code> instance, and suggesting that the <code>Monad</code> instance should actually be replaced with an <a href="http://hackage.haskell.org/package/indexed">indexed monad</a>.</li>
<li>It doesn’t provide any exception handling mechanism, and doesn’t guarantee that finalizers will be called in case any exception occurs. I imagine that some sort of exception support could be layered on top of the current solution, but I’m guessing it’s not going to be straightforward.</li>
<li>Folds are not compositional. This can be clearly seen in the tutorial, where <code>strict</code> is not defined in terms of <code>toList</code>. With pipes-core, you would simply have:</li>
</ol>
<pre class="sourceCode haskell"><code class="sourceCode haskell">strict <span class="fu">=</span> consume <span class="fu">&gt;&gt;=</span> mapM yield
<span class="co">-- note that toList is called consume in pipes-core</span></code></pre>
<h2 id="whats-next-for-pipes-core">What’s next for pipes-core</h2>
<p>The current version of pipes-core already provides exception handling and guaranteed finalization in the face of asynchronous exceptions. Things that could be improved in its finalization support are:</p>
<ol style="list-style-type: decimal">
<li>Finalization is currently guaranteed, but not always prompt. When an exception handler is provided, upstream finalization gets delayed unnecessarily.</li>
<li>It is not possible to prematurely force finalization. I haven’t yet seen an example where this would be useful, but it would be nice to have it for completeness.</li>
</ol>
<p>I think I know how these points can be addressed, and hopefully they will make it into the next release.</p>
<p>For future releases, I’d like to focus on performance. Aside from micro-optimizations, I can see two main areas that would benefit from improvements: the <code>Monad</code> instance and the <code>Category</code> instance.</p>
<p>The current monadic bind unfortunately displays a quadratic behavior, since it basically works like a naive list concatenation function. The <code>Codensity</code> transformation should address that.</p>
<p>For the <code>Category</code> instance, it would be interesting to explore whether it is possible to achieve some form of fusion of intermediate data structures, similarly to classic <a href="http://www.cse.unsw.edu.au/~rl/publications/stream-fusion.html">stream fusion</a> for lists.</p>
<p>This is probably going to be more of a challenge, and will likely require some significant restructuring, but the prospective benefits are enormous. There is <a href="http://bentnib.org/induction-with-effects.html">some</a> <a href="http://bentnib.org/posts/2012-01-06-streams.html">research</a> on this topic and an <a href="https://github.com/michaelt/pipes-atkey-fusion">initial attempt</a> I plan to draw ideas from.</p>
<p>My last point is about the absence of an <code>unawait</code> primitive for <code>Pipe</code>. There has been quite a lot of discussion on this topic, but I remain unconvinced that having builtin parsing capabilities is a good thing.</p>
<p>Whenever there is a need to chain unconsumed input, there are a few viable options already:</p>
<ol style="list-style-type: decimal">
<li>Return leftover data, and add some manual wiring so that it’s passed to the “next” pipe.</li>
<li>Use <a href="https://github.com/pcapriotti/pipes-extra/blob/2caecb41705d335db80ce1c16a6d02134ed6a619/pipes-extra/Control/Pipe/PutbackPipe.hs"><code>PutbackPipe</code></a> from <a href="http://hackage.haskell.org/package/pipes-extra">pipes-extra</a>.</li>
<li>Use an actual parser library and convert the parser to a <code>Pipe</code> (see <a href="http://hackage.haskell.org/package/pipes-attoparsec">pipes-attoparsec</a>).</li>
</ol>
<p>In all the examples I have seen, however, pipes are composable enough that all the special logic to deal with boundaries of chunked streams can be implemented in a single “filter” pipe, and the rest of the pipeline can ignore the issue altogether.</p>
</div>
</article>
<article>
<header>
<h1 class="entry-title"><a href="/blog/2012/04/27/applicative-option-parser/">Applicative option parser</a></h1>
<p class="meta">
<time datetime="2012-04-27" pubdate>Apr 27<span>th</span>, 2012</time>
</p>
</header>
<div class="entry-content">
<p>There are quite a few option parsing libraries on Hackage already, but they either depend on Template Haskell, or require some boilerplate. Although I have nothing against the use of Template Haskell in general, I’ve always found its use in this case particularly unsatisfactory, and I’m convinced that a more idiomatic solution should exist.</p>
<p>In this post, I present a proof of concept implementation of a library that allows you to define type-safe option parsers in Applicative style.</p>
<p>The only extension that we actually need is <code>GADT</code>, since, as will be clear in a moment, our definition of <code>Parser</code> requires existential quantification.</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt;</span> <span class="ot">{-# LANGUAGE GADTs #-}</span>
<span class="ot">&gt;</span> <span class="kw">import </span><span class="dt">Control.Applicative</span></code></pre>
<p>Let’s start by defining the <code>Option</code> type, corresponding to a concrete parser for a single option:</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt;</span> <span class="kw">data</span> <span class="dt">Option</span> a <span class="fu">=</span> <span class="dt">Option</span>
<span class="ot">&gt;</span> {<span class="ot"> optName ::</span> <span class="dt">String</span>
<span class="ot">&gt;</span> ,<span class="ot"> optParser ::</span> <span class="dt">String</span> <span class="ot">-&gt;</span> <span class="dt">Maybe</span> a
<span class="ot">&gt;</span> }
<span class="ot">&gt;</span>
<span class="ot">&gt;</span> <span class="kw">instance</span> <span class="dt">Functor</span> <span class="dt">Option</span> <span class="kw">where</span>
<span class="ot">&gt;</span> fmap f (<span class="dt">Option</span> name p) <span class="fu">=</span> <span class="dt">Option</span> name (fmap f <span class="fu">.</span> p)
<span class="ot">&gt;</span>
<span class="ot">&gt; optMatches ::</span> <span class="dt">Option</span> a <span class="ot">-&gt;</span> <span class="dt">String</span> <span class="ot">-&gt;</span> <span class="dt">Bool</span>
<span class="ot">&gt;</span> optMatches opt s <span class="fu">=</span> s <span class="fu">==</span> <span class="ch">'-'</span> <span class="fu">:</span> <span class="ch">'-'</span> <span class="fu">:</span> optName opt</code></pre>
<p>For simplicity, we only support “long” options with exactly 1 argument. The <code>optMatches</code> function checks if an option matches a string given on the command line.</p>
<p>We can now define the main <code>Parser</code> type:</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt;</span> <span class="kw">data</span> <span class="dt">Parser</span> a <span class="kw">where</span>
<span class="ot">&gt;</span> <span class="dt">NilP</span><span class="ot"> ::</span> a <span class="ot">-&gt;</span> <span class="dt">Parser</span> a
<span class="ot">&gt;</span> <span class="dt">ConsP</span><span class="ot"> ::</span> <span class="dt">Option</span> (a <span class="ot">-&gt;</span> b)
<span class="ot">&gt;</span> <span class="ot">-&gt;</span> <span class="dt">Parser</span> a <span class="ot">-&gt;</span> <span class="dt">Parser</span> b
<span class="ot">&gt;</span>
<span class="ot">&gt;</span> <span class="kw">instance</span> <span class="dt">Functor</span> <span class="dt">Parser</span> <span class="kw">where</span>
<span class="ot">&gt;</span> fmap f (<span class="dt">NilP</span> x) <span class="fu">=</span> <span class="dt">NilP</span> (f x)
<span class="ot">&gt;</span> fmap f (<span class="dt">ConsP</span> opt rest) <span class="fu">=</span> <span class="dt">ConsP</span> (fmap (f<span class="fu">.</span>) opt) rest
<span class="ot">&gt;</span>
<span class="ot">&gt;</span> <span class="kw">instance</span> <span class="dt">Applicative</span> <span class="dt">Parser</span> <span class="kw">where</span>
<span class="ot">&gt;</span> pure <span class="fu">=</span> <span class="dt">NilP</span>
<span class="ot">&gt;</span> <span class="dt">NilP</span> f <span class="fu">&lt;*&gt;</span> p <span class="fu">=</span> fmap f p
<span class="ot">&gt;</span> <span class="dt">ConsP</span> opt rest <span class="fu">&lt;*&gt;</span> p <span class="fu">=</span>
<span class="ot">&gt;</span> <span class="dt">ConsP</span> (fmap uncurry opt) ((,) <span class="fu">&lt;$&gt;</span> rest <span class="fu">&lt;*&gt;</span> p)</code></pre>
<p>The <code>Parser</code> GADT resembles a heterogeneous list, with two constructors.</p>
<p>The <code>NilP r</code> constructor represents a “null” parser that doesn’t consume any arguments, and always returns <code>r</code> as a result.</p>
<p>The <code>ConsP</code> constructor is the combination of an <code>Option</code> returning a function, and an arbitrary parser returning an argument for that function. The combined parser applies the function to the argument and returns a result.</p>
<p>The definition of <code>(&lt;*&gt;)</code> probably needs some clarification. The variables involved have types:</p>
<pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="ot">opt ::</span> <span class="dt">Option</span> (a <span class="ot">-&gt;</span> b <span class="ot">-&gt;</span> c)
<span class="ot">rest ::</span> <span class="dt">Parser</span> a
<span class="ot">p ::</span> <span class="dt">Parser</span> b</code></pre>
<p>and we want to obtain a parser of type <code>Parser c</code>. So we <code>uncurry</code> the option, obtaining:</p>
<pre class="sourceCode haskell"><code class="sourceCode haskell">fmap uncurry<span class="ot"> opt ::</span> <span class="dt">Option</span> ((a, b) <span class="ot">-&gt;</span> c)</code></pre>
<p>and compose it with a parser for the <code>(a, b)</code> pair, obtained by applying the <code>(&lt;*&gt;)</code> operator recursively:</p>
<pre class="sourceCode haskell"><code class="sourceCode haskell">(,) <span class="fu">&lt;$&gt;</span> rest <span class="fu">&lt;*&gt;</span><span class="ot"> p ::</span> <span class="dt">Parser</span> (a, b)</code></pre>
<p>This is already enough to define some example parsers. Let’s first add a couple of convenience functions to help us create basic parsers:</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt; option ::</span> <span class="dt">String</span> <span class="ot">-&gt;</span> (<span class="dt">String</span> <span class="ot">-&gt;</span> <span class="dt">Maybe</span> a) <span class="ot">-&gt;</span> <span class="dt">Parser</span> a
<span class="ot">&gt;</span> option name p <span class="fu">=</span> <span class="dt">ConsP</span> (fmap const (<span class="dt">Option</span> name p)) (<span class="dt">NilP</span> ())</code></pre>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt; optionR ::</span> <span class="dt">Read</span> a <span class="ot">=&gt;</span> <span class="dt">String</span> <span class="ot">-&gt;</span> <span class="dt">Parser</span> a
<span class="ot">&gt;</span> optionR name <span class="fu">=</span> option name p
<span class="ot">&gt;</span> <span class="kw">where</span>
<span class="ot">&gt;</span> p arg <span class="fu">=</span> <span class="kw">case</span> reads arg <span class="kw">of</span>
<span class="ot">&gt;</span> [(r, <span class="st">&quot;&quot;</span>)] <span class="ot">-&gt;</span> <span class="dt">Just</span> r
<span class="ot">&gt;</span> _ <span class="ot">-&gt;</span> <span class="dt">Nothing</span></code></pre>
<p>And a record to contain the result of our parser:</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt;</span> <span class="kw">data</span> <span class="dt">User</span> <span class="fu">=</span> <span class="dt">User</span>
<span class="ot">&gt;</span> {<span class="ot"> userName ::</span> <span class="dt">String</span>
<span class="ot">&gt;</span> ,<span class="ot"> userId ::</span> <span class="dt">Integer</span>
<span class="ot">&gt;</span> } <span class="kw">deriving</span> <span class="dt">Show</span></code></pre>
<p>A parser for <code>User</code> is easily defined in applicative style:</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt; parser ::</span> <span class="dt">Parser</span> <span class="dt">User</span>
<span class="ot">&gt;</span> parser <span class="fu">=</span> <span class="dt">User</span> <span class="fu">&lt;$&gt;</span> option <span class="st">&quot;name&quot;</span> <span class="dt">Just</span> <span class="fu">&lt;*&gt;</span> optionR <span class="st">&quot;id&quot;</span></code></pre>
<p>To be able to actually use this parser, we need a “run” function:</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt; runParser ::</span> <span class="dt">Parser</span> a <span class="ot">-&gt;</span> [<span class="dt">String</span>] <span class="ot">-&gt;</span> <span class="dt">Maybe</span> (a, [<span class="dt">String</span>])
<span class="ot">&gt;</span> runParser (<span class="dt">NilP</span> x) args <span class="fu">=</span> <span class="dt">Just</span> (x, args)
<span class="ot">&gt;</span> runParser (<span class="dt">ConsP</span> _ _) [] <span class="fu">=</span> <span class="dt">Nothing</span>
<span class="ot">&gt;</span> runParser p (arg <span class="fu">:</span> args) <span class="fu">=</span>
<span class="ot">&gt;</span> <span class="kw">case</span> stepParser p arg args <span class="kw">of</span>
<span class="ot">&gt;</span> <span class="dt">Nothing</span> <span class="ot">-&gt;</span> <span class="dt">Nothing</span>
<span class="ot">&gt;</span> <span class="dt">Just</span> (p', args') <span class="ot">-&gt;</span> runParser p' args'
<span class="ot">&gt;</span>
<span class="ot">&gt; stepParser ::</span> <span class="dt">Parser</span> a <span class="ot">-&gt;</span> <span class="dt">String</span> <span class="ot">-&gt;</span> [<span class="dt">String</span>] <span class="ot">-&gt;</span> <span class="dt">Maybe</span> (<span class="dt">Parser</span> a, [<span class="dt">String</span>])
<span class="ot">&gt;</span> stepParser p arg args <span class="fu">=</span> <span class="kw">case</span> p <span class="kw">of</span>
<span class="ot">&gt;</span> <span class="dt">NilP</span> _ <span class="ot">-&gt;</span> <span class="dt">Nothing</span>
<span class="ot">&gt;</span> <span class="dt">ConsP</span> opt rest
<span class="ot">&gt;</span> <span class="fu">|</span> optMatches opt arg <span class="ot">-&gt;</span> <span class="kw">case</span> args <span class="kw">of</span>
<span class="ot">&gt;</span> [] <span class="ot">-&gt;</span> <span class="dt">Nothing</span>
<span class="ot">&gt;</span> (value <span class="fu">:</span> args') <span class="ot">-&gt;</span> <span class="kw">do</span>
<span class="ot">&gt;</span> f <span class="ot">&lt;-</span> optParser opt value
<span class="ot">&gt;</span> return (fmap f rest, args')
<span class="ot">&gt;</span> <span class="fu">|</span> otherwise <span class="ot">-&gt;</span> <span class="kw">do</span>
<span class="ot">&gt;</span> (rest', args') <span class="ot">&lt;-</span> stepParser rest arg args
<span class="ot">&gt;</span> return (<span class="dt">ConsP</span> opt rest', args')</code></pre>
<p>The idea is very simple: we take the first argument, and we go over each option of the parser, check if it matches, and if it does, we replace it with a <code>NilP</code> parser wrapping the result, consume the option and its argument from the argument list, then call <code>runParser</code> recursively.</p>
<p>Here is an example of <code>runParser</code> in action:</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt; ex1 ::</span> <span class="dt">Maybe</span> <span class="dt">User</span>
<span class="ot">&gt;</span> ex1 <span class="fu">=</span> fst <span class="fu">&lt;$&gt;</span> runParser parser [<span class="st">&quot;--name&quot;</span>, <span class="st">&quot;fry&quot;</span>, <span class="st">&quot;--id&quot;</span>, <span class="st">&quot;1&quot;</span>]
<span class="ot">&gt;</span> <span class="co">{- Just (User {userName = &quot;fry&quot;, userId = 1}) -}</span></code></pre>
<p>The order of arguments doesn’t matter:</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt; ex2 ::</span> <span class="dt">Maybe</span> <span class="dt">User</span>
<span class="ot">&gt;</span> ex2 <span class="fu">=</span> fst <span class="fu">&lt;$&gt;</span> runParser parser [<span class="st">&quot;--id&quot;</span>, <span class="st">&quot;2&quot;</span>, <span class="st">&quot;--name&quot;</span>, <span class="st">&quot;bender&quot;</span>]
<span class="ot">&gt;</span> <span class="co">{- Just (User {userName = &quot;bender&quot;, userId = 2}) -}</span></code></pre>
<p>Missing arguments will result in a parse error (i.e. <code>Nothing</code>). We don’t support default values but they are pretty easy to add.</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt; ex3 ::</span> <span class="dt">Maybe</span> <span class="dt">User</span>
<span class="ot">&gt;</span> ex3 <span class="fu">=</span> fst <span class="fu">&lt;$&gt;</span> runParser parser [<span class="st">&quot;--name&quot;</span>, <span class="st">&quot;leela&quot;</span>]
<span class="ot">&gt;</span> <span class="co">{- Nothing -}</span></code></pre>
<p>I think the above <code>Parser</code> type represents a pretty clean and elegant solution to the option parsing problem. To make it actually usable, I would need to add a few more features (boolean flags, default values, a help generator) and improve error handling and performance (right now parsing a single option is quadratic in the size of the <code>Parser</code>), but it looks like a fun project.</p>
<p>Does anyone think it’s worth adding yet another option parser to Hackage?</p>
</div>
</article>
<article>
<header>
<h1 class="entry-title"><a href="/blog/2012/02/04/monoidal-instances-for-pipes/">Monoidal instances for pipes</a></h1>
<p class="meta">
<time datetime="2012-02-04" pubdate>Feb 4<span>th</span>, 2012</time>
</p>
</header>
<div class="entry-content">
<p>In this post, I’m going to introduce a new class of combinators for pipes, with an interesting categorical interpretation. I will be using the pipe implementation of my <a href="http://pcapriotti.wordpress.com/2012/02/02/an-introduction-to-guarded-pipes/">previous post</a>.</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt;</span> <span class="ot">{-# LANGUAGE MultiParamTypeClasses #-}</span>
<span class="ot">&gt;</span> <span class="ot">{-# LANGUAGE FlexibleInstances #-}</span>
<span class="ot">&gt;</span> <span class="ot">{-# LANGUAGE TypeFamilies #-}</span>
<span class="ot">&gt;</span> <span class="ot">{-# LANGUAGE GeneralizedNewtypeDeriving #-}</span>
<span class="ot">&gt;</span> <span class="kw">module</span> <span class="dt">Blog.Pipes.MonoidalInstances</span> <span class="kw">where</span>
<span class="ot">&gt;</span>
<span class="ot">&gt;</span> <span class="kw">import </span><span class="dt">Blog.Pipes.Guarded</span> <span class="kw">hiding</span> (groupBy)
<span class="ot">&gt;</span> <span class="kw">import qualified</span> <span class="dt">Control.Arrow</span> <span class="kw">as</span> <span class="dt">A</span>
<span class="ot">&gt;</span> <span class="kw">import </span><span class="dt">Control.Category</span>
<span class="ot">&gt;</span> <span class="kw">import </span><span class="dt">Control.Categorical.Bifunctor</span>
<span class="ot">&gt;</span> <span class="kw">import </span><span class="dt">Control.Category.Associative</span>
<span class="ot">&gt;</span> <span class="kw">import </span><span class="dt">Control.Category.Braided</span>
<span class="ot">&gt;</span> <span class="kw">import </span><span class="dt">Control.Category.Monoidal</span>
<span class="ot">&gt;</span> <span class="kw">import </span><span class="dt">Control.Monad</span> (forever)
<span class="ot">&gt;</span> <span class="kw">import </span><span class="dt">Control.Monad.Free</span>
<span class="ot">&gt;</span> <span class="kw">import </span><span class="dt">Data.Maybe</span>
<span class="ot">&gt;</span> <span class="kw">import </span><span class="dt">Data.Void</span>
<span class="ot">&gt;</span> <span class="kw">import </span><span class="dt">Prelude</span> <span class="kw">hiding</span> ((.), id, filter, until)</code></pre>
<p>When pipes were first released, some people noticed the lack of an <code>Arrow</code> instance. In fact, it is not hard to show that, even identifying pipes modulo some sort of observational equality, there is no <code>Arrow</code> instance that satisfies the arrow laws.</p>
<p>The problem, of course, is with <code>first</code>, because we already have a simple implementation of <code>arr</code>. If we try to implement <code>first</code> we immediately discover that there’s a problem with the <code>Yield</code> case:</p>
<pre class="sourceCode haskell"><code class="sourceCode haskell">first (<span class="dt">Yield</span> x c) <span class="fu">=</span> yield (x, <span class="fu">???</span>) <span class="fu">&gt;&gt;</span> first c</code></pre>
<p>Since ??? can be of any type, the only possible value is bottom, which of course we don’t want to introduce. Alternative definitions of <code>first</code> that alter the structure of a yielding pipe are not possible if we want to satisfy the law:</p>
<pre class="sourceCode haskell"><code class="sourceCode haskell">first p <span class="fu">&gt;+&gt;</span> pipe fst <span class="fu">==</span> pipe fst <span class="fu">&gt;+&gt;</span> p</code></pre>
<p>Concretely, the problem is that the cartesian product in the type of <code>first</code> forces a sort of “synchronization point” that doesn’t necessarily exist. This is better understood if we look at the type of <code>(***)</code>, of which <code>first</code> can be thought of as a special case:</p>
<pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="ot">(***) ::</span> <span class="dt">Arrow</span> k <span class="ot">=&gt;</span> k a b <span class="ot">-&gt;</span> k a' b' <span class="ot">-&gt;</span> k (a, a') (b, b')
first <span class="fu">=</span> (<span class="fu">***</span> id)</code></pre>
<p>If the two input pipes yield at different times, there is no way to faithfully match their yielded values into a pair. There are hacks around that, but they don’t behave well compositionally, and exhibit either arbitrarily large space leaks or data loss.</p>
<p>This has been addressed before: stream processors, like those of the <a href="http://www.altocumulus.org/Fudgets/">Fudgets</a> library, being very similar to Pipes, have the same problem, and <a href="http://www.google.ie/url?sa=t&amp;rct=j&amp;q=prodarrow+ps&amp;source=web&amp;cd=1&amp;ved=0CB8QFjAA&amp;url=http%3A%2F%2Fwww.carlssonia.org%2Fogi%2Fpapers%2Farrows.ps.gz&amp;ei=WXgqT-6pK5CzhAfZ_9DWCg&amp;usg=AFQjCNESuOahh6WeEsPTJoHHUbO8J858mQ&amp;sig2=Kffi1WwxedHlbogGNdUFRg">some resolutions</a> have been proposed, although not entirely satisfactory.</p>
<h2 id="arrows-as-monoidal-categories">Arrows as monoidal categories</h2>
<p>It is well known within the Haskell community that Arrows correspond to so called Freyd categories, i.e. premonoidal categories with some extra structures.</p>
<p>Using the <code>Monoidal</code> class by Edward Kmett (now in the <code>categories</code> package on Hackage), we can try to make this idea precise.</p>
<p>Unfortunately, we have to use a newtype to avoid overlapping instances in the case of the Hask category:</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt;</span> <span class="kw">newtype</span> <span class="dt">ACat</span> a b c <span class="fu">=</span> <span class="dt">ACat</span> {<span class="ot"> unACat ::</span> a b c }
<span class="ot">&gt;</span> <span class="kw">deriving</span> (<span class="dt">Category</span>, <span class="dt">A.Arrow</span>)</code></pre>
<p>First, cartesian products are a bifunctor in the category determined by an Arrow.</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt;</span> <span class="kw">instance</span> <span class="dt">A.Arrow</span> a <span class="ot">=&gt;</span> <span class="dt">PFunctor</span> (,) (<span class="dt">ACat</span> a) (<span class="dt">ACat</span> a) <span class="kw">where</span>
<span class="ot">&gt;</span> first <span class="fu">=</span> <span class="dt">ACat</span> <span class="fu">.</span> A.first <span class="fu">.</span> unACat
<span class="ot">&gt;</span> <span class="kw">instance</span> <span class="dt">A.Arrow</span> a <span class="ot">=&gt;</span> <span class="dt">QFunctor</span> (,) (<span class="dt">ACat</span> a) (<span class="dt">ACat</span> a) <span class="kw">where</span>
<span class="ot">&gt;</span> second <span class="fu">=</span> <span class="dt">ACat</span> <span class="fu">.</span> A.second <span class="fu">.</span> unACat
<span class="ot">&gt;</span> <span class="kw">instance</span> <span class="dt">A.Arrow</span> a
<span class="ot">&gt;</span> <span class="ot">=&gt;</span> <span class="dt">Bifunctor</span> (,) (<span class="dt">ACat</span> a) (<span class="dt">ACat</span> a) (<span class="dt">ACat</span> a) <span class="kw">where</span>
<span class="ot">&gt;</span> bimap (<span class="dt">ACat</span> f) (<span class="dt">ACat</span> g) <span class="fu">=</span> <span class="dt">ACat</span> <span class="fu">$</span> f <span class="fu">A.***</span> g</code></pre>
<p>Now we can say that products are associative, using the associativity of products in Hask:</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt;</span> <span class="kw">instance</span> <span class="dt">A.Arrow</span> a <span class="ot">=&gt;</span> <span class="dt">Associative</span> (<span class="dt">ACat</span> a) (,) <span class="kw">where</span>
<span class="ot">&gt;</span> associate <span class="fu">=</span> <span class="dt">ACat</span> <span class="fu">$</span> A.arr associate
<span class="ot">&gt;</span> <span class="kw">instance</span> <span class="dt">A.Arrow</span> a <span class="ot">=&gt;</span> <span class="dt">Disassociative</span> (<span class="dt">ACat</span> a) (,) <span class="kw">where</span>
<span class="ot">&gt;</span> disassociate <span class="fu">=</span> <span class="dt">ACat</span> <span class="fu">$</span> A.arr disassociate</code></pre>
<p>Where we use the <code>Disassociative</code> instance to express the inverse of the associator. And finally, the Monoidal instance:</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt;</span> <span class="kw">type</span> <span class="kw">instance</span> <span class="dt">Id</span> (<span class="dt">ACat</span> a) (,) <span class="fu">=</span> ()
<span class="ot">&gt;</span> <span class="kw">instance</span> <span class="dt">A.Arrow</span> a <span class="ot">=&gt;</span> <span class="dt">Monoidal</span> (<span class="dt">ACat</span> a) (,) <span class="kw">where</span>
<span class="ot">&gt;</span> idl <span class="fu">=</span> <span class="dt">ACat</span> <span class="fu">$</span> A.arr idl
<span class="ot">&gt;</span> idr <span class="fu">=</span> <span class="dt">ACat</span> <span class="fu">$</span> A.arr idr
<span class="ot">&gt;</span> <span class="kw">instance</span> <span class="dt">A.Arrow</span> a <span class="ot">=&gt;</span> <span class="dt">Comonoidal</span> (<span class="dt">ACat</span> a) (,) <span class="kw">where</span>
<span class="ot">&gt;</span> coidl <span class="fu">=</span> <span class="dt">ACat</span> <span class="fu">$</span> A.arr coidl
<span class="ot">&gt;</span> coidr <span class="fu">=</span> <span class="dt">ACat</span> <span class="fu">$</span> A.arr coidr</code></pre>
<p>Where, again, the duals are actually inverses. Also, products are symmetric:</p>
<pre class="sourceCode literate literatehaskell"><code class="sourceCode literatehaskell"><span class="ot">&gt;</span> <span class="kw">instance</span> <span class="dt">A.Arrow</span> a <span class="ot">=&gt;</span> <span class="dt">Braided</span> (<span class="dt">ACat</span> a) (,) <span class="kw">where</span>
<span class="ot">&gt;</span> braid <span class="fu">=</span