Auke Booij's programming and logic

tl;dr: ApplicativeDo 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, do blocks are associated with Monad constraints. You might know that by enabling the ApplicativeDo language extension, we can write do blocks for unary type constructors that are not monads, but only applicatives. (Recall that Monad is a subclass of Applicative since GHC 7.10.1 .) {-# LANGUAGE ApplicativeDo #-} showAnInt :: Applicative f => f Int -> f String showAnInt action = do n <- action return $ show n But did you know that we can also write do blocks for Functor s? -- Note the 'Functor' constraint rather than 'Applicative'. showAnIntFunctor :: Functor f => f Int -> f String showAnIntFunctor action = do n <- action return $ show n I encountered this accidentally while writing code for Hasura : I wrote a do bloc...

Show the Haskell imports import Numeric.Natural import Data.Maybe 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 a -> Bool . In the context of QuickCheck, the type a is assumed to be an instance of the Arbitrary type class, allowing to randomly generate values of a . Because of its random nature, QuickCheck might not find any offending element of a even if it exists. type Property a = a -> Bool If the property tester managed to invalidate the property, it returns the offending element of a . Otherwise, it simply succeeds. data Result counterexample = Success | Failure counterexample instance Show ( Result counterexample) where show Success = "Success" show ( Failure _) = "Failure" type Tester a = Property a -> Result a It is quite well-known in the functional programming community that...

This is an announcement of a paper in the areas of constructive mathematics, (univalent) type theory, and exact real arithmetic. 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. To appear in the MSCS Special Issue ...

This 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 arXiv . Somewhat stronger results can be found in Chapter 5 of my PhD thesis . I intend to publish these results at a later stage.

This is an announcement of a paper in the area of type theory and parametricity. Specific violations of parametricity, or existence of non-identity automorphisms of the universe, can be used to prove classical axioms. The former was  previously featured on the Homotopy Type Theory blog, and the latter is part of  a discussion on the HoTT mailing list . In a cooperation between Martín Escardó, Peter Lumsdaine, Mike Shulman, and myself, we have strengthened these results and recorded them in a paper that is published in the post-proceedings of TYPES 2016 (see also the preprint on arXiv ).