In a previous post I introduced the TTIE language, along with a type checker and interpreter . My motivation for writing that (aside from it being fun!) was to explore the type system. At the time I started this project, formalizing this system as a shallow embedding in Agda was not easy. But with the addition of a rewriting mechanism, it has become much easier to use Agda without going insane…
When working with syntax trees (such as in a type theory interpreter ) you often want to apply some operation to all subtrees of a node, or to all nodes of a certain type. Of course you can do this easily by writing a recursive function. But then you would need to have a case for every constructor, and there can be many constructors. Instead of writing a big recursive function for each operation,…
In this post I would like to present the type theory I have been working on, where the usual equality is replaced by an equality type indexed by the homotopy interval. This results in ideas very similar to those from the cubical system. I have a prototype implementation of this system in Haskell, which you can find on github . The system is unimaginatively called TTIE, a type theory with indexed…
I recently came accross the streaming library . This library defines a type Stream ( Of a ) m b for computations that produce zero or more values of type a in a monad m , and eventually produce a value of type b . This stream type can be used for efficient IO without having to load whole files into memory. The streaming library touts bechmark results showing superior performance compared to other…
Warning: evil ahead! A while ago Neil Mitchell wrote about a different implementation of sequence for the IO monad . The issue with the usual definition is that it is not tail recursive. Neil's version uses some hacks to essentially break out of the IO monad. But the solution does require two traversals of the list. Now in any language other than Haskell this IO monad wouldn't exist at all, and…
Here is a way to represent heterogeneous or dependent equalities, based on an interval type. In Homotopy Type Theory the interval is usually presented as a Higher Inductive Type with two constructors and a path between them. Here I will just give the two constructors, the path is implicit data I : Set where i₁ : I i₂ : I -- there is usually a path, i-edge : i₁ ≡ i₂ The eliminator is i-elim : ∀ { a…
This is a follow up on last week's post . There I showed that in a univalent Observational Type Theory, you can derive subst from cong . Now I am going to go one step further. Suppose we change the definition of paths for functions from Path (A → B) f g ≡ ∀ x → f x ≡ g x to Path (A → B) f g ≡ ∀ { x y } → x ≡ y → f x ≡ g y Then for a function f , refl f is actually the same thing as cong f !. So…
In this post I will show that in an univalence style observational type theory, it is enough to take congruence as a primitive, rather than the more complicated substitution or J axioms. This post is literate Agda, so here are some boring import declarations module subst-from-cong where open import Level open import Function open import Data.Unit open import Data.Bool open import Data.Empty open…
A while ago I set out to prove the correctness of merge sort in Agda. Of course this has been done before. But most proofs you find are far from complete. All they prove is a lemma such as is-sorted : ∀ ( xs : List A) → IsSortedList ( sort xs ) Maybe even restricted to lists of natural numbers. While it is nice that a sort function indeed produces a sorted output, that is only half of the story.…
Today Dan Burton remarked that Pipe is a category-like thing, and to express it we would need "type bundling". I myself said something similar a while ago. More formally, rather than a category where the objects are Haskell types, we have a category where the objects are pairs of types. It turns out that with a bunch of recent Ghc extensions we can actually write this in Haskell. {-# LANGUAGE…
Inspired by a discussion on the ghc mailing list , I wondered how much performance can be gained by specializing and unboxing certain data types. In particular, I looked at Data.Map . Suppose that you have a map from ints to ints. First of all, you should be using Data.IntMap instead, but that is besides the point. If you know that the keys and values are always strict integers, then the data type…
In this post I show another way to implement pipes, by combining a producer and consumer monad transformer. This implementation is for educational and entertainment purposes only: you probably shouldn't try to use it in production software. To quote Donald Knuth: I have only proved it correct, not tried it. One obvious thing that is missing is finalization, but that could be added by passing along…
In the pipes library, the type of the composition operator is ( >+> ) :: Pipe m a b r -> Pipe m b c r -> Pipe m a c r If you look closely, then you will notice that all three pipes have result type r . How does this work? Simple: whichever pipe stops first provides the final result. In my opinion this is wrong. The upstream pipe produces values, and the downstream pipe does something with them.…
In this post I will explain the software behind my blog, since several visitors have asked about it. But I will have to disappoint those of you hoping for fancy Haskell code: it is written in PHP. So no pandoc, no hakyll, no happstack and no Yesod. Some reasons for picking php are: PHP works pretty much everywhere, and PHP hosting is very cheap. I already had much of the code laying around from…
Michael Snoyman released conduit-0.3 this week. The conduit package provides three datatypes that can be chained together: Source, Counduit and Sink. If you were to look at the source code, you will notice that there is a lot of overlap between these datatypes. In this post I'll show how these types can be combined into a single one, which is the idea used by the pipes package. Compare: data Sink…
A colleague of mine recently needed to represent DAGs (directed acyclic graphs) in Coq, and asked around for ideas. Since Coq is not a nice language to program in, I decided to use Haskell instead. Something close to dependently typed programming is possible in Haskell thanks to GADTs. And other extensions will be helpful too, {-# LANGUAGE GADTs, TypeOperators, Rank2Types #-} My idea is to…
In part 2 of this series , I looked at finding axis aligned rectangles in binary images. I left you hanging with a hint of a more efficient algorithm than the O(n 3 ) one from that post. Formally, the problem we were trying to solve was: Given a binary image, find the largest axis aligned rectangle with a 1 pixel wide border that consists entirely of foreground pixels. Here is the same example as…
Binary search trees are used quite often for storing or finding values. Like a binary search, they essentially work by sorting the items. In this post I will describe a search tree that does not require that the items be sorted. Hence, the tree can support some interesting queries. The queries will always be correct, but they will only be fast in some cases. Bounds Usually, to make searching fast,…
In the previous post , we looked at finding axis aligned rectangles in a binary image. Today I am going to solve a variation of that problem: Given a binary image, find the largest axis aligned rectangle with a 1 pixel wide border that consists entirely of foreground pixels. Here is an example: , where white pixels are the background and blue is the foreground. The rectangle with the largest area…
This post is based on a part of my masters thesis . The topic of my thesis was OCR of historical documents. A problem that came up there was the following: Given a binary image, find the largest axis aligned rectangle that consists only of foreground pixels. These largest rectangles can be used, for instance, to find columns in a page of text. Although in that case one would use large rectangles…
Warning: rant ahead. This week I submitted for review the second revision of what will hopefully become my first scientific publication. Together with my supervisor I spent countless hours on this article. But does that mean that it is now the best text that I have ever written? I don't think so. While a lot of effort did go into improving the clarity, structure, etc.; there are several competing…
In the past I have blogged about functional references . From now on I will conform to most of the rest of the world, and call these things lenses. Giving a presentation on these objects has forced me to think about them some more. As a result of this thinking I have a new favorite representation, at least from a theory point of view: A lens from type a to b is a bijection between a and a pair of…
Two days ago I gave a talk on lenses at the Radboud Unviersity (where I work on my PhD on machine learning). I put the slides online for your enjoyment, although it might be hard to follow, since it is light on explanatory text. This talk includes information from at least three different earlier blog posts , as well as Russel O'Connor's recent paper on multiplate . There is no new information in…
I am moving my website from ">http://twan.home.fmf.nl/ to ">http://twanvl.nl/ . The moves comes with a fancy new design, as well as rewritten backend code.
Here is an idea for some more function composition operators, beyond just ( . ) : ( f .$ g ) x = ( f ) . ( g $ x ) ( f $. g ) x = ( f $ x ) . ( g ) ( f .$$ g ) x y = ( f ) . ( g $ x $ y ) ( f $.$ g ) x y = ( f $ x ) . ( g $ y ) ( f $$. g ) x y = ( f $ x $ y ) . ( g ) -- etc. infixl 8 .$ , $. , .$$ , $.$ , $$. -- slightly less tight than (.) The .$ name is supposed suggests that an extra argument…
As most Haskell programmers know, there are two ways to fold a list: from the right with foldr and from the left with foldl . foldr is corecursive (productive), which is great when the output can be produced lazily. foldl (or better, its strict cousin foldl' ) is tail recursive, preventing stack overflows. We can define analogous operations for other data structures like 1-dimensional arrays.…
I have recently come up with a new way of representing functional references. As you might recall, functional references (also called lenses) are like a pointer into a field of some data structure. The value of this field can be extracted and modified. For example: GHCi> get fstF ( 123 , "hey" ) 123 GHCi> set fstF 456 ( 123 , "hey" ) ( 456 , "hey" ) GHCi> modify fstF ( * 2 ) ( 123 , "hey" ) ( 246…
Friday I wrote about the type data FunList a b = Done b | More a ( FunList a ( a -> b )) Where did this type come from? What can you use it for? The story starts with another way of constructing FunList s, besides pure . For contrast I will call it 'impure'. impure :: a -> FunList a a impure a = More a ( Done id ) I claim that any FunList can be written in the form pure b <*> impure a 1 <*> impure…
While playing around with generalized functional references I encountered the following list-like data type: data FunList a b = Done b | More a ( FunList a ( a -> b )) This is a non-regular data type, meaning that inside the FunList a b there is a FunList a not-b . So, what does a value of this type look like? Well, it can be Done ( x :: b ) , or More a 1 ( Done ( x :: a -> b )) , or More a 1 (…
Previously in this series: part 1: moves part 2: combinatorics part 3: rings Welcome to the fourth installement of the Knight in n series. In part 3 we talked about the direct product of rings, and how they helped us solve the knight moves problem. This time yet another type of product is going to help in decomposing the algorithm to allow faster parts to be put in. The tensor product of rings In…
Previously in this series: part 1: moves part 2: combinatorics In this third installment, we will look at how to use various types as numbers, i.e. how to make them an instance of the Num type class. The solution the Knight-moves-problem will emerge at the end, almost as if by magic. :) Tangent: Things as numbers Many types can be used as if they are numbers. Haskell-wise this means they can be an…
Previously in this series: part 1: moves In my previous post I introduced the 'knight moves problem': How many ways are there for a chess knight to reach cell (i,j) in exactly n moves? The recursive solution from last time is horribly inefficient for larger values of n . Today I will show some more efficient solutions. Ignoring the order of moves If the knight first makes a move (-1,2) and then a…
Consider the following problem: A knight is placed at the origin of a chessboard that is infinite in all directions. How many ways are there for that knight to reach cell (i,j) in exactly n moves? This knight moves problem is not hard, nor does it have any real life applications. The problem is still interesting because there are many different ways to solve it, ranging from very simple to quite…
Regular old arrays have a size; you can't just have an infinite array. On the other hand, a lazy language such as Haskell does allow infinite lists. The idea behind the UnboundedArray module is to combine the O(1) access of arrays with the unbounded size of lazy lists. module UnboundedArray where This data type is built on top of ordinary arrays and unsafe IO operations: import Data.Array import…
When working with sorted lists you often come to the point where you want to combine two or more of them. This merge procedure forms the heart of merge sort it works something like: merge [ 1 , 3 , 4 , 5 ] [ 2 , 3 , 4 ] = [ 1 , 2 , 3 , 3 , 4 , 4 , 5 ] This merge function is not in the Haskell standard library, and even if there were, it might not be very useful. The problem is that when you need…
In this post I will show how to solve nonograms automatically using a computer. The code has been on the Haskell wiki for over year, but I have never taken the time to explain how it works. This post is literate haskell ( download the source here ), so we need to start with some imports: import qualified Data.Set as Set import qualified Data.Map as Map import Data.Set ( Set ) import Data.List…
This blog post is inspired by a message from Cale on #haskell yesterday. He came up with an amazing way to show how foldr and foldl work: <Cale> > foldr ( \ x y -> concat [ "(f " , x , " " , y , ")" ] ) "z" ( map show [ 1 .. 5 ] ) <lambdabot> "(f 1 (f 2 (f 3 (f 4 (f 5 z)))))" While the output looks great, the call itself could be clearer, especially for beginners. Through a combination of…
Recap: functional references Last time (okay, it was over two months ago) I talked about overloading functional references so that they can be used both as regular functions and as references. The data type of references I used was data FRef s a = FRef { get :: s -> a , set :: a -> s -> s } While I arrived at the type class, class Ref r where ref :: ( a -> b ) -> ( b -> a -> a ) -> r a b ( . ) ::…
Recently there have been some blog post and mailing list messages about "functional references". In this message I will look into ways to improve upon that concept. The above links should give you an idea of what a functional reference is, but I will explain it here in my own words. You can skip this introduction if you already know what functional references are. What are functional references? A…
A request that comes up regularly on the Haskell mailing list is for a function to determine whether one string (the needle) is a substring of another one (the haystack). While there is no such function in the Haskell standard library † , it is easy enough to implement: import Data.List as `isSubstringOf` bs = any ( as `isPrefixOf` ) ( tails bs ) Unfortunatly, this function has a worst case…