Skip to content

Instantly share code, notes, and snippets.

Avatar

Alejandro Serrano serras

View GitHub Profile
View program-analysis.md

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
serras / advent-haskell-2020.md
Created Dec 15, 2020
Advent of Haskell 2020
View advent-haskell-2020.md

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
View variants-proposal.md

Variants

Author

  • Alejando Serrano (47 Degrees)

Champions

  • Searching for one ;)
@serras
serras / graphql-better-mutation.md
Created Sep 30, 2020
Better mutations for GraphQL
View graphql-better-mutation.md

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
serras / variants.md
Created Aug 31, 2020
Variants: the ultimate frontier
View variants.md

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.

View building-software.md

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
serras / BF.agda
Created Feb 21, 2019
Small soundness proof for Boolean formulae
View BF.agda
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
serras / Idea.hs
Last active Jun 9, 2018
Code for LambdaConf 2018 Unconference talk about generics
View Idea.hs
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
View Parsers.swift
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
}
}
View all.hs
type family All (c :: k -> Constraint) (t :: [k]) :: Constraint where
All c '[] = ()
All c (x ': xs) = (c x, All c xs)