Carview!

CARVIEW

MOTORHOMES

Select Language

HTTP/2 200 cross-origin-resource-policy: cross-origin etag: W/"36a5025a6034931b9c85b712fe92b1ac50aa8deef63a393fcf6f68b74d82cf26" date: Sun, 18 Jan 2026 07:09:58 GMT content-type: application/atom+xml; charset=UTF-8 server: blogger-renderd expires: Sun, 18 Jan 2026 07:09:59 GMT cache-control: public, must-revalidate, proxy-revalidate, max-age=1 x-content-type-options: nosniff x-xss-protection: 0 last-modified: Wed, 28 Aug 2024 04:13:34 GMT content-encoding: gzip content-length: 13964 x-frame-options: SAMEORIGIN alt-svc: h3=":443"; ma=2592000,h3-29=":443"; ma=2592000 tag:blogger.com,1999:blog-66082365615176585572024-08-28T04:13:34.709+00:00Auke Booij's programming and logicAukehttps://www.blogger.com/profile/12557099016349698408noreply@blogger.comBlogger5125tag:blogger.com,1999:blog-6608236561517658557.post-59037955697363926962021-02-09T18:51:00.000+00:002021-02-09T18:56:03.495+00:00-XFunctorialDotl;dr: <code>ApplicativeDo</code> is useful also for functors. However, use laziness when pattern matching. The GHC manual remains a fantastic resource for learning about language extensions. By default, <code>do</code> blocks are associated with <code>Monad</code> constraints. You might know that by enabling the <code>ApplicativeDo</code> language extension, we can write <code>do</code> blocks for unary type constructors that are not monads, but only applicatives. (Recall that <code>Monad</code> is a subclass of <code>Applicative</code> <a href="https://wiki.haskell.org/Functor-Applicative-Monad_Proposal">since GHC 7.10.1</a>.) <div class="sourceCode" id="cb1"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb1-1" aria-hidden="true"></a>{-# LANGUAGE ApplicativeDo #-}</code></pre></div> <div class="sourceCode" id="cb2"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb2-1" aria-hidden="true"></a>showAnInt :: Applicative f => f Int -> f String <a href="#cb2-2" aria-hidden="true"></a>showAnInt action = do <a href="#cb2-3" aria-hidden="true"></a> n <- action <a href="#cb2-4" aria-hidden="true"></a> return $ show n</code></pre></div> But did you know that we can also write <code>do</code> blocks for <code>Functor</code>s? <div class="sourceCode" id="cb3"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb3-1" aria-hidden="true"></a>-- Note the 'Functor' constraint rather than 'Applicative'. <a href="#cb3-2" aria-hidden="true"></a>showAnIntFunctor :: Functor f => f Int -> f String <a href="#cb3-3" aria-hidden="true"></a>showAnIntFunctor action = do <a href="#cb3-4" aria-hidden="true"></a> n <- action <a href="#cb3-5" aria-hidden="true"></a> return $ show n</code></pre></div> I encountered this accidentally while writing code for <a href="https://hasura.io/">Hasura</a>: I wrote a <code>do</code> block for something that I suspected might have an <code>Applicative</code> instance. It compiled, and everything was fine, but at a later stage I could not track down where that instance was defined. <h1 id="origins">Origins</h1> At first, I suspected that the GHC rewriting mechanism was kicking in just in time to compile (the equivalent of) <code>showAnIntFunctor</code> down to something like <code>(show <$>)</code>. In retrospect, this was a bad suspicion: it would be terribly confusing if the rewriting mechanism would arbitrarily change the type of things. Put differently, the motto should be: terms that are well-typed with rewriting should also be well-typed without rewriting. So why does it work? Certainly, <code>ApplicativeDo</code> does not simply relax the <code>Monad</code> constraint on <code>do</code> blocks to <code>Applicative</code>, since some <code>do</code> blocks cannot be desugared to code in terms of the <code>Applicative</code> methods. A very simple example of that is: <div class="sourceCode" id="cb4"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb4-1" aria-hidden="true"></a>applyToPackage box action = do <a href="#cb4-2" aria-hidden="true"></a> x <- box <a href="#cb4-3" aria-hidden="true"></a> action x</code></pre></div> The above doesn’t work for <code>Applicative</code>s, because it implements exactly the <code>(>>=)</code> operator that distinguishes <code>Monad</code>s from <code>Applicative</code>s. Hence: <div class="sourceCode" id="cb5"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb5-1" aria-hidden="true"></a>-- Note the 'Monad' constraint despite us having switched on 'ApplicativeDo' <a href="#cb5-2" aria-hidden="true"></a>applyToPackage :: Monad f => f a -> (a -> f b) -> f b</code></pre></div> So how does the appropriate constraint on a given <code>do</code> block arise? The constraint is not generated directly by GHC. Rather, normally, a <code>do</code> block is desugared into applications of <code>(>>=)</code>, and it is through these operators that a <code>Monad</code> constraint normally arises. In fact, already without <code>ApplicativeDo</code>, the following compiles: <div class="sourceCode" id="cb6"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb6-1" aria-hidden="true"></a>-- NB: No constraints on 'f' are required. <a href="#cb6-2" aria-hidden="true"></a>justDoIt :: f Int -> f Int <a href="#cb6-3" aria-hidden="true"></a>justDoIt action = do <a href="#cb6-4" aria-hidden="true"></a> action</code></pre></div> The logic that <code>ApplicativeDo</code> adds is that it does a syntactic analysis of the code inside the <code>do</code> block, in order to make use of <code>(<$>)</code> and <code>(<*>)</code> rather than <code>(>>=)</code> where possible. This syntactic analysis works out to a single application of <code>(<$>)</code> for the above example of <code>showAnIntFunctor</code>. But this analysis is imperfect and does not always produce the expected result. For instance, all of the following four methods can be “desugared” to <code>pure :: Applicative f => a -> f a</code>: <div class="sourceCode" id="cb7"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb7-1" aria-hidden="true"></a>pure1 = return</code></pre></div> <div class="sourceCode" id="cb8"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb8-1" aria-hidden="true"></a>pure2 x = do <a href="#cb8-2" aria-hidden="true"></a> return x</code></pre></div> <div class="sourceCode" id="cb9"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb9-1" aria-hidden="true"></a>pure3 x = do <a href="#cb9-2" aria-hidden="true"></a> y <- pure x <a href="#cb9-3" aria-hidden="true"></a> return x</code></pre></div> <div class="sourceCode" id="cb10"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb10-1" aria-hidden="true"></a>pure4 x = do <a href="#cb10-2" aria-hidden="true"></a> y <- return x <a href="#cb10-3" aria-hidden="true"></a> return x</code></pre></div> However, only the third item is considered to be <code>Applicative</code> by the <code>ApplicativeDo</code> extension. <div class="sourceCode" id="cb11"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb11-1" aria-hidden="true"></a>pure1 :: Monad f => a -> f a <a href="#cb11-2" aria-hidden="true"></a>pure2 :: Monad f => a -> f a <a href="#cb11-3" aria-hidden="true"></a>pure3 :: Applicative f => a -> f a <a href="#cb11-4" aria-hidden="true"></a>pure4 :: Monad f => a -> f a</code></pre></div> Perhaps, if <code>return</code> becomes an alias for <code>pure</code>, i.e. after the <a href="https://gitlab.haskell.org/ghc/ghc/-/wikis/proposal/monad-of-no-return">monad of no return</a> GHC proposal is implemented, all four can be generalized to <code>Applicative</code>. Similarly, one can write convoluted <code>do</code> blocks that can be implemented by <code>id :: f a -> f a</code>, which requires no constraints on <code>f</code>, but regardless <code>ApplicativeDo</code> desugars those <code>do</code> blocks to code that has constraints on <code>f</code>. <div class="sourceCode" id="cb12"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb12-1" aria-hidden="true"></a>constrainedId xM = do <a href="#cb12-2" aria-hidden="true"></a> x <- xM <a href="#cb12-3" aria-hidden="true"></a> pure x <a href="#cb12-4" aria-hidden="true"></a>constrainedId :: Functor f => f a -> f a</code></pre></div> <h1 id="pattern-matching">Pattern matching</h1> One further oddity arises when pattern matching. Perhaps surprisingly, the code <div class="sourceCode" id="cb13"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb13-1" aria-hidden="true"></a>unpackAndApply1 gM xyF = do <a href="#cb13-2" aria-hidden="true"></a> (i, _) <- xyF <a href="#cb13-3" aria-hidden="true"></a> g <- gM <a href="#cb13-4" aria-hidden="true"></a> return $ g i <a href="#cb13-5" aria-hidden="true"></a>unpackAndApply1 :: Monad f => f (Int -> a) -> f (Int, String) -> f a</code></pre></div> gets a <code>Monad</code> constraint, despite the code seemingly only requiring <code>Applicative</code>: just capture the result of the monadic action and unpack it with <code>fst</code>, avoiding <code>(>>=)</code>. <div class="sourceCode" id="cb14"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb14-1" aria-hidden="true"></a>unpackAndApply2 gM xyF = <a href="#cb14-2" aria-hidden="true"></a> gM <*> (fst <$> xyF) <a href="#cb14-3" aria-hidden="true"></a>unpackAndApply2 :: Applicative f => f (Int -> a) -> f (Int, String) -> f a</code></pre></div> So why the <code>Monad</code> constraint? Again I originally started with an incorrect suspicion, namely that this was because the pattern match might fail (think of a <code>Left</code> pattern match on an <code>Either</code> value), and was hence injecting a call to <code>fail</code>. But, in retrospect, that doesn’t make sense, since the constraint is <code>Monad f</code>, not <code>MonadFail f</code>. Born in the wrong generation, I guess… The answer is that there’s a semantic difference between <ul> <li><code>unpackAndApply1 (const 'a') (pure undefined)</code> (which is <code>undefined</code>) and</li> <li><code>unpackAndApply2 (const 'a') (pure undefined)</code> (which is <code>pure 'a'</code>).</li> </ul> Hence, <code>ApplicativeDo</code> does not desuger <code>unpackAndApply1</code> into <code>unpackAndApply2</code> since it would change the strictness of the <code>do</code> block. We can convince <code>ApplicativeDo</code> otherwise by flagging the pattern match as being lazy: <div class="sourceCode" id="cb15"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb15-1" aria-hidden="true"></a>unpackAndApply3 gM xyF = do <a href="#cb15-2" aria-hidden="true"></a> ~(i, _) <- xyF <a href="#cb15-3" aria-hidden="true"></a> g <- gM <a href="#cb15-4" aria-hidden="true"></a> return $ g i <a href="#cb15-5" aria-hidden="true"></a>unpackAndApply3 :: Applicative f => f (Int -> a) -> f (Int, String) -> f a</code></pre></div> This moves the goalpost by allowing the tuple to be unpacked on an as-needed basis. Another way to resolve it is by manually moving the pattern match to a point where it doesn’t interfere with an applicative desugaring of the <code>do</code> block: <div class="sourceCode" id="cb16"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb16-1" aria-hidden="true"></a>unpackAndApply4 gM xyF = do <a href="#cb16-2" aria-hidden="true"></a> x'y <- xyF <a href="#cb16-3" aria-hidden="true"></a> g <- gM <a href="#cb16-4" aria-hidden="true"></a> return $ g (fst x'y) -- now the unpacking happens here <a href="#cb16-5" aria-hidden="true"></a>unpackAndApply4 :: Applicative f => f (Int -> a) -> f (Int, String) -> f a</code></pre></div> <code>unpackAndApply2</code>, <code>unpackAndApply3</code> and <code>unpackAndApply4</code> should be semantically equal. <h1 id="parallelism">Parallelism</h1> The <a href="https://www.microsoft.com/en-us/research/publication/desugaring-haskells-do-notation-into-applicative-operations/">original motivation</a> for <code>ApplicativeDo</code> was to speed up certain code written in <code>do</code> blocks, even when a <code>Monad</code> instance is in scope. The idea was that <code>(<$>)</code> and <code>(<*>)</code> allowed for more efficient implementations than the default ones arising from <code>(>>=)</code> and <code>return</code>. The final desugaring of a <code>do</code> block might be a mixture of all of <code>(<$>)</code>, <code>(<*>)</code> and <code>(>>=)</code>, where parts of the applicative-based may be executed “in parallel”, and parts which are necessarily monadic are executed “sequentially”, whatever those two terms mean in the domain of the code. In order to make optimal use of this, it is important to organize <code>do</code> blocks in such a way that the functorial and applicative operators can kick in. For instance, the first block can be optimized better than the second block: (this example comes straight from the paper linked above) (both require a <code>Monad</code>) <div class="sourceCode" id="cb17"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb17-1" aria-hidden="true"></a>variant1 xM xM' f f' = do <a href="#cb17-2" aria-hidden="true"></a> x <- xM <a href="#cb17-3" aria-hidden="true"></a> y <- f x <a href="#cb17-4" aria-hidden="true"></a> x' <- xM' <a href="#cb17-5" aria-hidden="true"></a> y' <- f' x' <a href="#cb17-6" aria-hidden="true"></a> return (y, y')</code></pre></div> <div class="sourceCode" id="cb18"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb18-1" aria-hidden="true"></a>variant2 xM xM' f f' = do <a href="#cb18-2" aria-hidden="true"></a> x <- xM <a href="#cb18-3" aria-hidden="true"></a> x' <- xM' -- note this line being executed earlier, <a href="#cb18-4" aria-hidden="true"></a> y <- f x -- ... before the call to 'f' <a href="#cb18-5" aria-hidden="true"></a> y' <- f' x' <a href="#cb18-6" aria-hidden="true"></a> return (y, y')</code></pre></div> The problem is that the call to <code>xM'</code> in the second variant prevents <code>f</code> from starting execution, whereas in the first version the computation of <code>y</code> and <code>y'</code> are fully independent. Algebraically, we can say that <code>ApplicativeDo</code> only applies those transformations that follow the laws of functors/applicatives/monads, and reordering monadic actions is not allowed in general (and in fact, not well-typed in general). So when writing monadic code that can potentially be desugared into more efficient code using applicative combinators (even partially), the motto to keep in mind is “related things go together”. This is somewhat opposed to low-level machine code, where one tries to maximize the number of instructions between, for instance, fetching data from memory and using that data, so that high-performance processor architectures such as pipelining and out-of-order-execution work optimally. <h1 id="ghc-users-guide">GHC User’s Guide</h1> I haven’t said anything fundamentally new in this blog post. Most of this content can also be found in the <a href="https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/applicative_do.html">GHC User’s Guide</a>, and indeed that was my main source. I found the documentation there very readable, and it answered exactly the questions that I found myself asking. Aukehttps://www.blogger.com/profile/12557099016349698408noreply@blogger.com0tag:blogger.com,1999:blog-6608236561517658557.post-72243356699382640842020-08-31T18:52:00.000+00:002020-08-31T18:52:40.388+00:00Property testing property testers<details> <summary> Show the Haskell imports </summary> <div class="sourceCode" id="cb1"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb1-1" aria-hidden="true"></a>import Numeric.Natural <a href="#cb1-2" aria-hidden="true"></a>import Data.Maybe</code></pre></div> </details> Property testers such as QuickCheck are used to search for inputs that invalidate a given property. We focus on properties that are implemented in Haskell as a function <code>a -> Bool</code>. In the context of QuickCheck, the type <code>a</code> is assumed to be an instance of the <code>Arbitrary</code> type class, allowing to randomly generate values of <code>a</code>. Because of its random nature, QuickCheck might not find any offending element of <code>a</code> even if it exists. <div class="sourceCode" id="cb2"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb2-1" aria-hidden="true"></a>type Property a = a -> Bool</code></pre></div> If the property tester managed to invalidate the property, it returns the offending element of <code>a</code>. Otherwise, it simply succeeds. <div class="sourceCode" id="cb3"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb3-1" aria-hidden="true"></a>data Result counterexample <a href="#cb3-2" aria-hidden="true"></a> = Success <a href="#cb3-3" aria-hidden="true"></a> | Failure counterexample <a href="#cb3-4" aria-hidden="true"></a>instance Show (Result counterexample) where <a href="#cb3-5" aria-hidden="true"></a> show Success = "Success" <a href="#cb3-6" aria-hidden="true"></a> show (Failure _) = "Failure"</code></pre></div> <div class="sourceCode" id="cb4"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb4-1" aria-hidden="true"></a>type Tester a = Property a -> Result a</code></pre></div> It is quite well-known in the functional programming community that there exist infinite exhaustively testable types. That is, in finite time we can exhaustively test whether a given property holds for all input values of type <code>a</code>, even, in some cases, when <code>a</code> is infinite. A prototypical infinite exhaustively testable type, and the one we’ll focus on in this blog post, is the Cantor space of functions from the natural numbers to the Booleans. <div class="sourceCode" id="cb5"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb5-1" aria-hidden="true"></a>type Cantor = Natural -> Bool</code></pre></div> Expanding the above definition, exhaustive testability of Cantor space means that we can write a testing process of type <code>Tester Cantor = Property Cantor -> Result Cantor</code> that, for any property on Cantor space, succeeds when the property holds for all values of type <code>Cantor</code>, and returns a counterexample when there is a value of type <code>Cantor</code> for which it fails. <div class="sourceCode" id="cb6"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb6-1" aria-hidden="true"></a>(#) :: Bool -> Cantor -> Cantor <a href="#cb6-2" aria-hidden="true"></a>b # f = \i -> if i == 0 then b else f (i-1)</code></pre></div> <div class="sourceCode" id="cb7"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb7-1" aria-hidden="true"></a>-- Try to find a probe that invalidates the property. <a href="#cb7-2" aria-hidden="true"></a>find :: Property Cantor -> Cantor <a href="#cb7-3" aria-hidden="true"></a>find prop = h # find (\a -> prop (h # a)) <a href="#cb7-4" aria-hidden="true"></a> where h = prop (False # find (\a -> prop (False # a)))</code></pre></div> <div class="sourceCode" id="cb8"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb8-1" aria-hidden="true"></a>-- Exhaustively test a property on Cantor space <a href="#cb8-2" aria-hidden="true"></a>exhaustiveCheck :: Tester Cantor <a href="#cb8-3" aria-hidden="true"></a>exhaustiveCheck prop = <a href="#cb8-4" aria-hidden="true"></a> if prop probe <a href="#cb8-5" aria-hidden="true"></a> -- The property holds on all inputs <a href="#cb8-6" aria-hidden="true"></a> then Success <a href="#cb8-7" aria-hidden="true"></a> -- The property fails; 'probe' is a counterexample <a href="#cb8-8" aria-hidden="true"></a> else Failure probe <a href="#cb8-9" aria-hidden="true"></a> where probe = find prop</code></pre></div> The above fact has seen little application outside of papers and blog posts. This text, being a blog post, is no different. The raison d’être of this post is merely to, once again, observe this surprising fact, and to do something fun with it, as appears <a href="https://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/">to</a> <a href="https://math.andrej.com/2008/11/21/a-haskell-monad-for-infinite-search-in-finite-time/">be</a> <a href="https://lukepalmer.wordpress.com/2008/12/07/compact-data-types/">done</a> <a href="https://lukepalmer.wordpress.com/2010/11/17/searchable-data-types/">every</a> <a href="https://math.andrej.com/2011/12/06/how-to-make-the-impossible-functionals-run-even-faster/">couple</a> <a href="https://math.andrej.com/2014/05/08/seemingly-impossible-proofs/">of</a> <a href="https://julesh.com/2016/09/22/abusing-the-continuation-monad/">years</a>. So what might we do with an exhaustive testing process <code>Property Cantor -> Result Cantor</code>? What property of Cantor space might we wish to exhaustively test? Such a property might test input-output behavior of a function that takes elements of Cantor space as input (though not necessarily returning Booleans). However, when we are thinking of QuickCheck-able programs, we normally think of types that are isomorphic to the natural numbers, such as strings and binary trees. “Oh, but that type is isomorphic to Cantor space!” is not the one-liner it could be among Haskellers. Here’s the key observation of this blog post: <code>Cantor = Property Natural</code>. So here’s a proposal for program we might want to phrase properties about: the QuickCheck-style property tester itself. After all, we may see a property tester for natural numbers as a map <code>Cantor -> Result Natural</code>, that takes a property of natural numbers (e.g. whether taking the square of a natural always results in an even number) and tells us whether it managed to find any inputs for which the property returns <code>False</code> (in this case, one might hope so). Here are some sample implementations of property testers for us to play around with, which have some intentional shortcomings. <div class="sourceCode" id="cb9"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb9-1" aria-hidden="true"></a>-- A property tester that doesn't check the property against any <a href="#cb9-2" aria-hidden="true"></a>-- inputs and simply always succeeds <a href="#cb9-3" aria-hidden="true"></a>testNothing :: Tester Natural <a href="#cb9-4" aria-hidden="true"></a>-- A property tester that only tests the input 0 <a href="#cb9-5" aria-hidden="true"></a>testZero :: Tester Natural <a href="#cb9-6" aria-hidden="true"></a>-- A property tester that tests the property on inputs 0 through 100 <a href="#cb9-7" aria-hidden="true"></a>test100 :: Tester Natural <a href="#cb9-8" aria-hidden="true"></a>-- A property tester that tests the property on inputs 100 through 200 <a href="#cb9-9" aria-hidden="true"></a>testNext100 :: Tester Natural <a href="#cb9-10" aria-hidden="true"></a>-- A property tester that reports an incorrect witness of failure <a href="#cb9-11" aria-hidden="true"></a>testWrongWitness :: Tester Natural <a href="#cb9-12" aria-hidden="true"></a>-- A property tester that sometimes reports an incorrect witness: <a href="#cb9-13" aria-hidden="true"></a>-- only when the property holds for [0..100] and 100000, <a href="#cb9-14" aria-hidden="true"></a>-- but fails at 12345 and 26535 <a href="#cb9-15" aria-hidden="true"></a>testWrongWitnessSubtle :: Tester Natural</code></pre></div> <details> <summary> Show the implementations of these testers </summary> <div class="sourceCode" id="cb10"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb10-1" aria-hidden="true"></a>testNothing _ = Success</code></pre></div> <div class="sourceCode" id="cb11"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb11-1" aria-hidden="true"></a>testZero prop = <a href="#cb11-2" aria-hidden="true"></a> if prop 0 <a href="#cb11-3" aria-hidden="true"></a> then Success <a href="#cb11-4" aria-hidden="true"></a> else Failure 0</code></pre></div> <div class="sourceCode" id="cb12"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb12-1" aria-hidden="true"></a>test100 prop = case tests of <a href="#cb12-2" aria-hidden="true"></a> [] -> Success <a href="#cb12-3" aria-hidden="true"></a> i:_ -> Failure i <a href="#cb12-4" aria-hidden="true"></a> where <a href="#cb12-5" aria-hidden="true"></a> tests = mapMaybe (\i -> if prop i then Nothing else Just i) [0..100]</code></pre></div> <div class="sourceCode" id="cb13"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb13-1" aria-hidden="true"></a>testNext100 prop = case tests of <a href="#cb13-2" aria-hidden="true"></a> [] -> Success <a href="#cb13-3" aria-hidden="true"></a> i:_ -> Failure i <a href="#cb13-4" aria-hidden="true"></a> where <a href="#cb13-5" aria-hidden="true"></a> tests = mapMaybe (\i -> if prop i then Nothing else Just i) [100..200]</code></pre></div> <div class="sourceCode" id="cb14"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb14-1" aria-hidden="true"></a>testWrongWitness prop = <a href="#cb14-2" aria-hidden="true"></a> if prop 12345 <a href="#cb14-3" aria-hidden="true"></a> then Success <a href="#cb14-4" aria-hidden="true"></a> else Failure 9876</code></pre></div> <div class="sourceCode" id="cb15"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb15-1" aria-hidden="true"></a>testWrongWitnessSubtle prop = case test100 prop of <a href="#cb15-2" aria-hidden="true"></a> Success -> <a href="#cb15-3" aria-hidden="true"></a> if prop 100000 <a href="#cb15-4" aria-hidden="true"></a> then case (prop 26535, prop 12345) of <a href="#cb15-5" aria-hidden="true"></a> (True, True) -> Success <a href="#cb15-6" aria-hidden="true"></a> (False, True) -> Failure 26535 <a href="#cb15-7" aria-hidden="true"></a> (True, False) -> Failure 12345 <a href="#cb15-8" aria-hidden="true"></a> (False, False) -> Failure 9876 -- Wrong witness! <a href="#cb15-9" aria-hidden="true"></a> else Failure 100000 <a href="#cb15-10" aria-hidden="true"></a> Failure i -> Failure i</code></pre></div> </details> So what property can we phrase for a given property tester to satisfy? We can require that the property tester always tests the property at input 0. More precisely, if the property passes testing, then the property itself needs to hold at 0. We would expect <code>testNothing</code> to fail this test, but <code>testZero</code> and <code>test100</code> to satisfy it. <div class="sourceCode" id="cb16"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb16-1" aria-hidden="true"></a>prop_alwaysTestZero :: Tester Natural -> Property (Property Natural) <a href="#cb16-2" aria-hidden="true"></a>prop_alwaysTestZero tester prop = <a href="#cb16-3" aria-hidden="true"></a> case tester prop of <a href="#cb16-4" aria-hidden="true"></a> Success -> prop 0 <a href="#cb16-5" aria-hidden="true"></a> Failure _ -> True</code></pre></div> Note that we can’t directly check whether the property tester actually evaluated the property at 0: we only observe input-output behavior of the property tester. So in the case of a test failure, we can’t say anything about the required behavior of the property tester, since it might still fail because the property is false at another input. However, this is not reducing the power of our test at all, since we’re exhaustively testing over all properties of the naturals. Just to drive this point home: for a given property tester <code>tester</code>, the property <code>prop_alwaysTestZero tester</code> isn’t just QuickCheck-able, in the sense that we can generate 100 inputs and see whether the property holds for those 100 inputs. It is exhaustively checkable, despite it stating a property of an infinite space. If the exhaustive check succeeds, we know that <code>prop_alwaysTestZero tester</code> holds for all properties on the naturals. At this point, it is important to realize that, in the context of property testing, properties must in fact be decidable, rather than being arbitrary formulae in first-order logic (say). This restricts what we can test. In particular, we can’t test the claim “if the property always holds, then the property tester always succeeds”: because it is not decidable whether the input property always holds, so this claim itself is not a decidable property. But, since if the property tester fails, it also outputs a witness of this, we can test the contrapositive. So here is an exhaustively testable property expressing that if a property fails the property tester, then the witness provided by the property tester is actually an input for which the property is <code>False</code>. We would expect <code>testNothing</code>, <code>testZero</code> and <code>test100</code> to satisfy it, but <code>testWrongWitness</code> and <code>testWrongWitnessSubtle</code> to fail it. <div class="sourceCode" id="cb17"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb17-1" aria-hidden="true"></a>prop_failureActuallyFails :: Tester Natural -> Property (Property Natural) <a href="#cb17-2" aria-hidden="true"></a>prop_failureActuallyFails tester prop = <a href="#cb17-3" aria-hidden="true"></a> case tester prop of <a href="#cb17-4" aria-hidden="true"></a> Success -> True <a href="#cb17-5" aria-hidden="true"></a> -- The property tester found a counterexample, so that better be one <a href="#cb17-6" aria-hidden="true"></a> Failure n -> not (prop n)</code></pre></div> This, I think, is a key property of property testers that is currently untested for QuickCheck. To be clear, I would expect QuickCheck to satisfy it, but strictly speaking it’s essential behavior that ought to be in the test suite. QuickCheck attempts to shrinks counterexamples: so once it has randomly encountered a counterexample, it tries to find another which is intended to be smaller or simpler, in a sense specified by the implementation of <code>shrink</code> as part of the <code>Arbitrary</code> type class. We might therefore expect that if a tester finds a counterexample, that it picks a minimal one, in the sense that applying <code>shrink</code> to it does not yield any counterexamples that are smaller. For the natural numbers, this means that when we obtain a <code>Failure i</code>, then any natural smaller than <code>i</code> should not be a counterexample. <div class="sourceCode" id="cb18"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb18-1" aria-hidden="true"></a>prop_failureMinimal :: Tester Natural -> Property (Property Natural) <a href="#cb18-2" aria-hidden="true"></a>prop_failureMinimal tester prop = <a href="#cb18-3" aria-hidden="true"></a> case tester prop of <a href="#cb18-4" aria-hidden="true"></a> Success -> True <a href="#cb18-5" aria-hidden="true"></a> Failure i -> all prop (init [0..i])</code></pre></div> Here’s how we can run the exhaustive testing: <div class="sourceCode" id="cb19"><pre class="sourceCode haskell literate"><code class="sourceCode haskell"><a href="#cb19-1" aria-hidden="true"></a>main :: IO () <a href="#cb19-2" aria-hidden="true"></a>main = do <a href="#cb19-3" aria-hidden="true"></a> putStr "Testing whether testNothing tests 0 (expecting Failure): " <a href="#cb19-4" aria-hidden="true"></a> print $ exhaustiveCheck (prop_alwaysTestZero testNothing) <a href="#cb19-5" aria-hidden="true"></a> putStr "Testing whether testZero tests 0 (expecting Success): " <a href="#cb19-6" aria-hidden="true"></a> print $ exhaustiveCheck (prop_alwaysTestZero testZero) <a href="#cb19-7" aria-hidden="true"></a> putStr "Testing whether test100 tests 0 (expecting Success): " <a href="#cb19-8" aria-hidden="true"></a> print $ exhaustiveCheck (prop_alwaysTestZero test100) <a href="#cb19-9" aria-hidden="true"></a> putStr "Testing whether test100 yields minimal failure witnesses (expecting Success): " <a href="#cb19-10" aria-hidden="true"></a> print $ exhaustiveCheck (prop_failureMinimal test100) <a href="#cb19-11" aria-hidden="true"></a> putStr "Testing whether testNext100 yields minimal failure witnesses (expecting Failure): " <a href="#cb19-12" aria-hidden="true"></a> print $ exhaustiveCheck (prop_failureMinimal testNext100) <a href="#cb19-13" aria-hidden="true"></a> putStr "Testing whether test100 gives valid failure witnesses (expecting Success): " <a href="#cb19-14" aria-hidden="true"></a> print $ exhaustiveCheck (prop_failureActuallyFails test100) <a href="#cb19-15" aria-hidden="true"></a> putStr "Testing whether testWrongWitness gives valid failure witnesses (expecting Failure): " <a href="#cb19-16" aria-hidden="true"></a> print $ exhaustiveCheck (prop_failureActuallyFails testWrongWitness) <a href="#cb19-17" aria-hidden="true"></a> putStr "Testing whether testWrongWitnessSubtle gives valid failure witnesses (expecting Failure): " <a href="#cb19-18" aria-hidden="true"></a> print $ exhaustiveCheck (prop_failureActuallyFails testWrongWitnessSubtle)</code></pre></div> I think the last test case best demonstrates the power of this approach. Normal <code>Arbitrary</code>-based property testing has no chance to catch the subtle bug in the implementation of the property tester <code>testWrongWitnessSubtle</code>. It would take deep inspection of the code of <code>testWrongWitnessSubtle</code> to write a counterexample manually. But this exhaustive technique finds a counterexample within 0.3 seconds on my machine, without any static analysis. So why is this just a blog post rather than a pull request? In reality, QuickCheck uses the IO monad to print additional information to the terminal, and to generate randomness, so that in this instance the true type of <code>quickCheck</code> would be closer to <code>(Natural -> Bool) -> IO (Result Natural)</code>. But we may imagine a pure variant of QuickCheck whose random number generator can be pre-seeded, and which computes a result purely without writing anything to the terminal. I’m not sure the above idea is adequate motivation to refactor QuickCheck in such a fundamental way. But, if anybody wants to work on this, do let me know. Good luck to the next person writing a blog post about infinite searchable types!Aukehttps://www.blogger.com/profile/12557099016349698408noreply@blogger.com0tag:blogger.com,1999:blog-6608236561517658557.post-1623975073600538062020-06-22T08:00:00.001+00:002020-07-22T13:21:21.598+00:00Extensional constructive real analysis via locators<div>This is an announcement of a paper in the areas of constructive mathematics, (univalent) type theory, and exact real arithmetic. </div><div> </div><div>Abstract: Real numbers do not admit an extensional procedure for observing discrete information, such as the first digit of its decimal expansion, because every extensional, computable map from the reals to the integers is constant, as is well known. We overcome this by considering real numbers equipped with additional structure, which we call a locator. With this structure, it is possible, for instance, to construct a signed-digit representation or a Cauchy sequence, and conversely these intensional representations give rise to a locator. Although the constructions are reminiscent of computable analysis, instead of working with a notion of computability, we simply work constructively to extract observable information, and instead of working with representations, we consider a certain locatedness structure on real numbers. </div><div> </div><div>To appear in the MSCS <a href="https://hott-uf.github.io/special-issue-17-18/">Special Issue on Homotopy Type Theory and Univalent Foundations</a> (<a href="https://export.arxiv.org/abs/1805.06781">preprint on the arXiv</a>). This work is also discussed in some more generality in my <a href="https://abooij.blogspot.com/p/phd-thesis.html">PhD thesis</a>. </div>Aukehttps://www.blogger.com/profile/12557099016349698408noreply@blogger.com2tag:blogger.com,1999:blog-6608236561517658557.post-84930214577063211762017-06-20T08:00:00.003+00:002020-07-22T13:21:59.479+00:00The HoTT book reals coincide with the Escardó-Simpson realsThis is an announcement of a paper in the area of univalent type theory and exact real arithmetic.Escardó and Simpson defined a notion of interval object by a universal property in any category with binary products. The Homotopy Type Theory book defines a higher-inductive notion of reals, and suggests that the interval may satisfy this universal property. We show that this is indeed the case in the category of sets of any universe. We also show that the type of HoTT book reals is the least Cauchy complete subset of the Dedekind reals containing the rationals. Preprint is on the <a href="https://arxiv.org/abs/1706.05956">arXiv</a>.Somewhat stronger results can be found in Chapter 5 of my <a href="https://abooij.blogspot.com/p/phd-thesis.html">PhD thesis</a>. I intend to publish these results at a later stage. Aukehttps://www.blogger.com/profile/12557099016349698408noreply@blogger.com0tag:blogger.com,1999:blog-6608236561517658557.post-11940254781783918382016-12-01T09:00:00.001+00:002020-07-22T13:21:19.674+00:00Parametricity, automorphisms of the universe, and excluded middle<div>This is an announcement of a paper in the area of type theory and parametricity. </div><div> </div><div>Specific violations of parametricity, or existence of non-identity automorphisms of the universe, can be used to prove classical axioms. The former was <a href="https://homotopytypetheory.org/2016/02/24/parametricity-and-excluded-middle/">previously featured</a> on the Homotopy Type Theory blog, and the latter is part of <a href="https://groups.google.com/forum/#!searchin/homotopytypetheory/automorphisms|sort:relevance/homotopytypetheory/8CV0S2DuOI8/0XibNKHou1EJ">a discussion on the HoTT mailing list</a>. In a cooperation between Martín Escardó, Peter Lumsdaine, Mike Shulman, and myself, we have strengthened these results and recorded them in a <a href="https://doi.org/10.4230/LIPIcs.TYPES.2016.7">paper that is published in the post-proceedings of TYPES 2016</a> (see also the <a href="https://arxiv.org/abs/1701.05617">preprint on arXiv</a>).</div>Aukehttps://www.blogger.com/profile/12557099016349698408noreply@blogger.com0

Original Source | Taken Source