Skip to content

Instantly share code, notes, and snippets.

View serras's full-sized avatar

Alejandro Serrano serras

View GitHub Profile

Program Analysis, a Big Happy Family

The idea behind program analysis is simple, right? You just want to know stuff about your program before it runs, usually because you don't want unexpected problems to arise (those are better in movies.) Then why looking at Wikipedia gives you headaches? Just so many approaches, tools, languages 🤯

In this article I would like to give a glimpse of an overarching approach to program analysis, based on ideas from abstract interpretation. My goal is not to pinpoint a specific technique, but rather show how they have common core concepts, the differences being due mostly to algorithmic challenges. In other words, static analysis have a shared goal, but it's a challenge to make them precise and performant.

Code is meant to be executed by a computer. Take the following very simple function:

fun cantulupe(x) = {
serras /
Created December 15, 2020 09:04
Advent of Haskell 2020

Talking about Toys

Every year Santa 🎅 brings joy (and presents 🎁) to all the kids in the world. Well, not when I was a child! Following the usual Spanish traditions, the Three Reyes Magos brought me presents in their camels 🐫 following the Star 💫 Nowadays, it's Sinterklaas who puts pepernoten in my shoes 👞. Because in fact there's not one, but a group of present-bringing people, distributed across the globe 🌐, each with their own part of the world to cover (or you really thought just one man and eight reindeers could do it all by their own?)

In order to communicate, they need a way to exchange information about presents. Since they are all very wise, they've agreed to use Haskell, so this information is represented using algebraic data types. Here are some types related to building blocks:

data Block = Block BlockBrand String Color
data BlockBrand = LegoKNex



  • Alejando Serrano (47 Degrees)


  • Searching for one ;)
serras /
Created September 30, 2020 19:01
Better mutations for GraphQL

Better mutations for GraphQL

GraphQL is great. The first time I read about it I remember thinking that it had everything: a powerful schema language, a way to describe exactly the data you want, even an appealing syntax. With time, though, the second of those sentenced have been bugging me: it's great to describe data you want, but for modifications, it doesn't feel as well-rounded.

Whereas GraphQL gives you a nice language for queries, for mutations it's customary to have just a top-level method where the input object carries all the information. Take the following example, obtained from the GraphQL.js tutorial:

type Message {
  id: ID!
 content: String
serras /
Created August 31, 2020 19:37
Variants: the ultimate frontier

Variants: the ultimate frontier

Most data serialization formats, like JSON, YAML, and EDN, feature a similar set of basic building blocks, namely:

  • Some primitive values, like numbers, strings, and booleans;
  • Key-value pairs, also known as maps, dictionaries, or objects;
  • Sequences, usually in the form of lists or arrays, and sometimes also sets.

I completely agree with the fact that those are basic building blocks for data inside any information system. However, as a Haskeller I always miss one additional part of my toolbox: variants. Variants are essentially tagged values which contain further values inside.

Some thoughts on building software

Lately I have been busy reading some new books on Domain Driven Design (DDD) and software architecture -- including a short yet eye-opening one in Python and a great one in F#. At the same time, it seems that more people in the Functional Programming world are looking at more formal approaches to modelling -- some examples here. This has brought some thought from the background of my brain about how we should model, organize, and architect software using the lessons we've learnt from functional programming.

Before moving on, let me be clear about this being just a dump of some thoughts, not always well-defined, definite

serras / BF.agda
Created February 21, 2019 13:31
Small soundness proof for Boolean formulae
module BF where
open import Agda.Builtin.Equality
data BF : Set where
True : BF
False : BF
Not : BF → BF
And : BF → BF → BF
Or : BF → BF → BF
serras / Idea.hs
Last active June 9, 2018 23:22
Code for LambdaConf 2018 Unconference talk about generics
module Idea where
data Person = Person String (Maybe Gender)
data Gender = Male | Female | Other String
Person is like String :*: Maybe Gender
Gender is like NoFields :+: NoFields :+: String
data Pet = Dog String
| Cat Color String
struct Parser<Output> {
let parse : (_ cs : [Character]) -> (value : Output, remainder : [Character])?
func parse(_ s : String) -> (value : Output, remainder : String)? {
if let (v, rem) = parse(Array(s.characters)) {
return (v, String(rem))
} else {
return nil
type family All (c :: k -> Constraint) (t :: [k]) :: Constraint where
All c '[] = ()
All c (x ': xs) = (c x, All c xs)