serras

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

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 = Lego | KNex

serras

Variants

Author

• Alejando Serrano (47 Degrees)

Champions

• Searching for one ;)

serras

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

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.

serras

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

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

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

serras

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
    }
  }

serras

type family All (c :: k -> Constraint) (t :: [k]) :: Constraint where
  All c '[]       = ()
  All c (x ': xs) = (c x, All c xs)