tag:blogger.com,1999:blog-33049444Mon, 05 Mar 2018 18:18:08 +0000SubstratelogicgitbookmarkletfirefoxgmailgreasemonkeyAgileHaskellagdacomonadsdependent typesinductionjoblanguagesmonadsrantshellbeamercodatacommutativitycurry-howard isomorphismequalityfree theoremgodgoodnessgooglekernellambda calculuslatexlispmethodologyphilosophyrequirementsxulBloggy BadgerCode and ideas in computer science. And maybe a short story or two.http://gelisam.blogspot.com/noreply@blogger.com (gelisam)Blogger78125tag:blogger.com,1999:blog-33049444.post-5697600434780172295Mon, 01 Jan 2018 00:47:00 +00002018-01-07T16:56:55.476-05:00N-ary Functorsupdate: Now available on hackage as n-ary-functor.
Functor and Bifunctor are both in base, but what about Trifunctor? Quadrifunctor? There must be a better solution than creating an infinite tower of typeclasses. Here's the API I managed to implement:
> nmap <#> (+1) <#> (+2) $ (0, 0)
(1,2)
> nmap <#> (+1) <#> (+2) <#> (+3) $ (0, 0, 0)
(1,2,3)
> nmap <#> (+1) <#> (+2) <#> (+3) <#> (+4) $ (0, 0,http://gelisam.blogspot.com/2017/12/n-ary-functors.htmlnoreply@blogger.com (gelisam)2tag:blogger.com,1999:blog-33049444.post-70450598687523530Sat, 04 Nov 2017 03:26:00 +00002017-11-04T11:16:39.214-04:00Computing with Impossible TypesEdward Kmett recently posted a puzzling gist seemingly showing that at the type level, the () kind has more than one inhabitant. The goal of this post is to explain what's going on.
Stuck Type Expressions
Here is a simple type family.
{-# LANGUAGE TypeFamilies, UndecidableInstances #-}
type family F a where
F (Maybe a) = [F a]
F a = a
Since F (Maybe Int) and [F Int] both evaluate to http://gelisam.blogspot.com/2017/11/computing-with-impossible-types.htmlnoreply@blogger.com (gelisam)0tag:blogger.com,1999:blog-33049444.post-3794144156584456310Sat, 14 Oct 2017 19:33:00 +00002017-11-03T22:12:45.855-04:00Composing Declarations in Template HaskellI have recently tried to use Template Haskell to generate both a datatype and lenses for accessing the fields of this datatype, and it was harder than it should have been. In this post, I will demonstrate the problem, I will pinpoint its cause, and I will propose a solution.
The Problem
Consider the following code. I'm using a simple, contrived example instead of a more realistic one because it http://gelisam.blogspot.com/2017/10/composing-declarations-in-template.htmlnoreply@blogger.com (gelisam)0tag:blogger.com,1999:blog-33049444.post-5465803009265016595Sat, 26 Dec 2015 21:32:00 +00002015-12-26T16:32:35.790-05:00A whirlwind tour of Haskell, day 8Day 8, functionally: pattern-matchingToday's puzzle involves parsing: we are given a string literal containing escape sequences, and we must interpret those escape sequences into the characters they represent. Or at least into the correct number of characters, whatever.In my puzzle solutions so far, I have always pattern-matched at most one level deep, meaning that the pattern if any was always http://gelisam.blogspot.com/2015/12/a-whirlwind-tour-of-haskell-day-8.htmlnoreply@blogger.com (gelisam)1tag:blogger.com,1999:blog-33049444.post-6807121049758094375Fri, 25 Dec 2015 21:03:00 +00002015-12-26T16:34:08.312-05:00A whirlwind tour of Haskell, day 7Day 7, functionally: bit fiddling, Map, and recursionToday's puzzle is quite interesting, and will allow me to demonstrate several Haskell techniques! We're given the description of an electronic circuit consisting of a bunch of constants and bitwise operations, and we need to simulate it. The bitwise operations are fairly standard, here's what they look like in Haskell:import Data.Word
import http://gelisam.blogspot.com/2015/12/a-whirlwind-tour-of-haskell-day-7.htmlnoreply@blogger.com (gelisam)0tag:blogger.com,1999:blog-33049444.post-1913077512702269773Sun, 20 Dec 2015 15:42:00 +00002015-12-25T16:05:07.507-05:00A whirlwind tour of Haskell, day 6Day 6: precise types, arrays, and STThis puzzle asks us to parse and execute a sequence of instructions. The instructions are represented as text strings, so in a dynamic language I would probably use regular expressions to determine which instruction I'm looking at, using capturing groups like the following to extract the instruction's parameters./^command1 ([0-9]+) ([0-9]+)$/
In Haskell, http://gelisam.blogspot.com/2015/12/a-whirlwind-tour-of-haskell-day-6.htmlnoreply@blogger.com (gelisam)0tag:blogger.com,1999:blog-33049444.post-8714199868166618838Sat, 19 Dec 2015 22:15:00 +00002015-12-20T10:44:14.236-05:00A whirlwind tour of Haskell, day 5Day 5: infix notation and list comprehensionsThis puzzle lists a bunch of nonsense conditions on the characters of a string, and we must check whether the string satisfies all of them. This should be quite easy in any language, so it doesn't give me the opportunity to demonstrate another powerful Haskell library. Instead, I think I will try to make my implementation as readable as possible:-- |
-http://gelisam.blogspot.com/2015/12/a-whirlwind-tour-of-haskell-day-5.htmlnoreply@blogger.com (gelisam)1tag:blogger.com,1999:blog-33049444.post-6952423420049317039Sat, 19 Dec 2015 20:42:00 +00002015-12-19T17:31:48.280-05:00A whirlwind tour of Haskell, day 4Day 4: process and conduitFor the next puzzle, we need to compute a sequence of md5 hashes and to return the first one which satisfies a given property. Haskell does have a few libraries implementing md5 hashing, but using such a function wouldn't teach us anything new about Haskell. Instead, let's delegate the task to an external program.$ echo -n "abcdef609043" | md5sum
http://gelisam.blogspot.com/2015/12/a-whirlwind-tour-of-haskell-day-4.htmlnoreply@blogger.com (gelisam)0tag:blogger.com,1999:blog-33049444.post-650164331075525477Sat, 19 Dec 2015 18:10:00 +00002015-12-19T17:31:31.915-05:00A whirlwind tour of Haskell, day 3Day 3: linear and containersIn this puzzle, we need to move a cursor in 2D space and count the number of distinct coordinates we visited.import qualified Data.Set as Set
import Linear.V2
direction :: Char -> V2 Int
direction '<' = V2 (-1) 0
direction '>' = V2 1 0
direction '^' = V2 0 1
direction 'v' = V2 0 (-1)
direction _ = V2 0 0
-- |
-- >>> day3 ">"
-- 2
-- >>> day3 "^>v<"
-- 4
-- >>> day3http://gelisam.blogspot.com/2015/12/a-whirlwind-tour-of-haskell-day-3.htmlnoreply@blogger.com (gelisam)0tag:blogger.com,1999:blog-33049444.post-2992185598031745990Sat, 19 Dec 2015 18:10:00 +00002015-12-19T17:31:18.314-05:00A whirlwind tour of Haskell, day 2Day 2: extra, type inference, and type classesThe next puzzle involves computing the area of the faces of a box. The equation to compute the area is provided, so the only slight complication is that the area of the smallest face needs to be added to the final answer.import Data.List.Extra
-- |
-- >>> day2 "2x3x4"
-- 58
-- >>> day2 "1x1x10"
-- 43
day2 = wordsBy (== 'x')
>>> map read
>>> (\[http://gelisam.blogspot.com/2015/12/a-whirlwind-tour-of-haskell-day-2.htmlnoreply@blogger.com (gelisam)0tag:blogger.com,1999:blog-33049444.post-3279303883953049766Sat, 19 Dec 2015 18:10:00 +00002015-12-19T17:30:58.754-05:00A whirlwind tour of Haskell, day 1Day 1, imperatively: transformers and monadsThe first puzzle asks us to increment and decrement a floor number every time an opening or closing parenthesis is encountered. In an imperative language, we'd probably begin by initializing a counter, then we'd iterate over the characters of the input string, incrementing or decrementing the counter depending on which character we encounted. http://gelisam.blogspot.com/2015/12/a-whirlwind-tour-of-haskell-day-1.htmlnoreply@blogger.com (gelisam)0tag:blogger.com,1999:blog-33049444.post-7123783646926109048Tue, 08 Dec 2015 00:28:00 +00002015-12-27T23:28:13.775-05:00A whirlwind tour of Haskell, via Advent of code solutionsAdvent of Code is a website listing 50 small programming challenges, revealing two per day from December 1st to December 25th. I'm currently going through the puzzles which have been revealed so far using my favorite programming language, Haskell. As the puzzles become slightly harder, I'm reaching for more and more sophisticated Haskell libraries, and this made me realize that the solutions to http://gelisam.blogspot.com/2015/12/a-whirlwind-tour-of-haskell-via-advent.htmlnoreply@blogger.com (gelisam)3tag:blogger.com,1999:blog-33049444.post-1466130336839313221Mon, 07 Sep 2015 04:46:00 +00002017-01-30T11:02:08.299-05:00Two kinds of backtrackingI sometimes write my own parser combinators. I sometimes make mistakes while implementing my own parser combinators. In this post, I describe a mistake I made a few times: using the wrong kind of backtracking effect.2015-08-11 update: it turns out everything in this post is already well-known in the litterature, see the Reddit discussion for links.Two ways to order effectsSo, like I said, I http://gelisam.blogspot.com/2015/09/two-kinds-of-backtracking.htmlnoreply@blogger.com (gelisam)1tag:blogger.com,1999:blog-33049444.post-1766458994893329491Fri, 19 Jun 2015 02:54:00 +00002015-06-20T09:31:05.445-04:00Will it memoize?In this post, I will try several variants of a simple memoizing Haskell program and test whether the program actually memoizes or not. This will give us a better grasp on sharing.
FibonacciIf you've been studying Haskell for any length of time, you have probably already stumbled upon the following unusual definition of the Fibonacci sequence.
fibs = 1 : 1 : zipWith (+) fibs (tail fibs)
If I printhttp://gelisam.blogspot.com/2015/06/will-it-memoize.htmlnoreply@blogger.com (gelisam)0tag:blogger.com,1999:blog-33049444.post-8480677191550117466Sun, 14 Jun 2015 15:57:00 +00002015-06-14T11:57:34.171-04:00Querying type specializationsObtaining the most general type of a Haskell expression is easy. But how do you figure out the more specialized types which your expression also has?DiagramsLet's draw a simple balloon using the diagrams library.import Diagrams.Prelude
import Diagrams.Backend.Cairo.CmdLine
diagram :: Diagram B
diagram = circle 1
===
vrule 1
I want to make the length of the string http://gelisam.blogspot.com/2015/06/querying-type-specializations.htmlnoreply@blogger.com (gelisam)0tag:blogger.com,1999:blog-33049444.post-5956477247752866710Sat, 02 May 2015 19:53:00 +00002015-05-02T18:09:53.752-04:00Strongly-typed ghci commandsThe ghci documentation explains how to implement conditional breakpoints by conditionally generating ghci commands depending on the values of variables which are in scope at the breakpoint. The approach works, but is hard to implement correctly because ghci's commands are stringly-typed. In this post, I will present a strongly-typed DSL for writing such commands in a type safe way, and I will usehttp://gelisam.blogspot.com/2015/05/strongly-typed-ghci-commands.htmlnoreply@blogger.com (gelisam)0tag:blogger.com,1999:blog-33049444.post-7007878312567995351Wed, 28 Jan 2015 19:38:00 +00002015-12-23T06:48:45.056-05:00Haxl anti-tutorialIt's time for another anti-tutorial! Whereas a tutorial is an advanced user giving step-by-step instructions to help newbies, an anti-tutorial is a new user describing their path to enlightenment. My approach is usually to follow the types, so my anti-tutorials are also examples of how to do that.Previously in the series:pipes anti-tutorial
reactive-banana anti-tutorial
netwire anti-tutorial
http://gelisam.blogspot.com/2015/01/haxl-anti-tutorial.htmlnoreply@blogger.com (gelisam)2tag:blogger.com,1999:blog-33049444.post-3485986852585654878Sun, 21 Dec 2014 18:14:00 +00002014-12-21T13:14:55.180-05:00The "99 Bottles of Beers" of Type Systems"Hello World" is a good first example program because it is small, but also because it encourages the reader to get into the driver's seat and take control of the program. Copy-paste the "Hello World" listing from a website, and you're just blindly following instructions. Change it to print "Hello Mom", and you're boldly taking your first step towards the unknown, into a world where it is now youhttp://gelisam.blogspot.com/2014/12/the-99-bottles-of-beers-of-type-systems_21.htmlnoreply@blogger.com (gelisam)2tag:blogger.com,1999:blog-33049444.post-140698832124330995Tue, 09 Dec 2014 04:38:00 +00002014-12-08T23:41:56.052-05:00How to package up binaries for distributionThis weekend, I wrote a game (in Haskell of course!) for Ludum Dare, an event in which you have 48h or 72h to create a game matching an imposed theme. It was really challenging!
Once the event was over, it was time to package my game in a form which others could play. Since the packaging procedure wasn't obvious, I'm documenting it here for future reference. The procedure isn't specific to http://gelisam.blogspot.com/2014/12/how-to-package-up-binaries-for.htmlnoreply@blogger.com (gelisam)0tag:blogger.com,1999:blog-33049444.post-311076093125616184Wed, 29 Oct 2014 03:15:00 +00002014-10-28T23:15:29.057-04:00Understanding "Strongly-typed Bound", part 1First, giving credits where credit is due. The Bound library is written by Edward Kmett, and so is the strongly-typed variant I want to explore in this series. I learned about the strongly-typed version via a comment by geezusfreeek, in response to a question by _skp.I have a lot to say about this script, and since the first thing I want to say about it involves writing down some typing rules, I http://gelisam.blogspot.com/2014/10/understanding-strongly-typed-bound-part.htmlnoreply@blogger.com (gelisam)0tag:blogger.com,1999:blog-33049444.post-9169788900624199506Sun, 07 Sep 2014 03:59:00 +00002014-09-15T09:11:26.494-04:00Prisms lead to typeclasses for subtractive typesIn my last post, I identified some issues with subtractive types, namely that math identities such as ∀ a. a + -a = 0, once they are translated into Haskell, would not be valid for all a. More precisely, the existence of a function of typecancelSub :: forall a. (a :+: Negative a) -> Zero
would make it easy to implement a contradiction, regardless of the way in which we represent Negative a:type ahttp://gelisam.blogspot.com/2014/09/prisms-lead-to-typeclasses-for.htmlnoreply@blogger.com (gelisam)0tag:blogger.com,1999:blog-33049444.post-6899101066445599289Fri, 29 Aug 2014 23:30:00 +00002014-08-29T19:30:25.356-04:00Edward Kmett likes my library :)I have be re-listening to old episodes of the Haskell Cast, and it turns out I missed something really, shall we say, relevant to my interests.
In the very first episode, Edward Kmett talks about lens and a few of his other libraries. Then, near the end, he is asked about interesting Haskell stuff aside from his libraries. His answer, at 59:45:
"There was a really cool Commutativity monad [..http://gelisam.blogspot.com/2014/08/edward-kmett-likes-my-library.htmlnoreply@blogger.com (gelisam)0tag:blogger.com,1999:blog-33049444.post-1319149472997335256Mon, 18 Aug 2014 04:33:00 +00002014-08-18T14:22:54.236-04:00Issues with subtractive typesI tried to expand on my earlier attempt at understanding root types, but I hit several obstacles. Here is a summary of those obstacles, in case future-me or someone else feels like trying again.
GoalsThe conversation began with Naperian types, and the way in which they satisfy the same laws as mathematical logarithms, except at the type level. For example, the law logb xy = logb x + logb y wouldhttp://gelisam.blogspot.com/2014/08/issues-with-subtractive-types.htmlnoreply@blogger.com (gelisam)0tag:blogger.com,1999:blog-33049444.post-2050784977939885063Sat, 16 Aug 2014 16:23:00 +00002014-08-16T12:23:59.919-04:00Homemade FRP: mystery leakThe mystery leak is back, and this time it's personal: the bug is clearly in my code somewhere.
My first hypothesis is that since I am emulating reactive-banana's API, and I now have the same kind of leak as I had with the real reactive-banana, maybe it's the same bug with the same solution? Nope, adding a <* stepper undefined events for each kind of event does not plug the leak.
My next http://gelisam.blogspot.com/2014/08/homemade-frp-mystery-leak.htmlnoreply@blogger.com (gelisam)0tag:blogger.com,1999:blog-33049444.post-3039758365514040065Tue, 29 Jul 2014 03:50:00 +00002014-07-28T23:50:07.987-04:00Homemade FRP: a study in following the typesI wonder how FRP is implemented? Since I only know about a small part of reactive-banana so far, this is the interface I am currently thinking of when I think of FRP:
data Event t a
data Behavior t a
instance Functor (Event t)
instance Functor (Behavior t)
instance Monoid (Event t)
instance Applicative (Behavior t)
filterE :: (a -> Bool) -> Event t a -> Event t a
accumE :: a -> Event t (a -> ahttp://gelisam.blogspot.com/2014/07/homemade-frp-study-in-following-types.htmlnoreply@blogger.com (gelisam)0