Anjana Sofia Vakil

Developer Educator & Software Engineer

© 2024. Credits.

Notes from KatsConf2

19 Feb 2017

Hello from Dublin! Yesterday I had the privilege of attending KatsConf2, a functional programming conference put on by the fun-loving, welcoming, and crazy-well-organized @FunctionalKats. It was a whirlwind of really exciting talks from some of the best speakers around. Here’s a glimpse into what I learned.

I took a bunch of notes during the talks, in case you’re hungering for more details. But @jessitron took amazing graphical notes that I’ve linked to in the talks below, so just go read those!

And for the complete experience, check out this storify Vicky Twomey-Lee, who led a great ally skills workshop the evening before the conference, made of the #KatsConf2 tweets:

Hopefully this gives you an idea of what was said and which brain-exploding things you should go look up now! Personally it opened up a bunch of cans of worms for me - definitely a lot of the material went over my head, but I have a ton of stuff to go find out more (i.e. the first thing) about.

Disclaimer: The (unedited!!!) notes below represent my initial impressions of the content of these talks, jotted down as I listened. They may or may not be totally accurate, or precisely/adequately represent what the speakers said or think, and the code examples are almost certainly mistake-ridden. Read at your own risk!

The origin story of FunctionalKats

FunctionalKatas => FunctionalKats => (as of today) FunctionalKubs

The Perfect Language

Bodil Stokke @bodil

What would the perfect programming language look like?

“MS Excel!” “Nobody wants to say ‘JavaScript’ as a joke?” “Lisp!” “I know there are Clojurians in the audience, they’re suspiciously silent…”

There’s no such thing as the perfect language; Languages are about compromise.

What the perfect language actually is is a personal thing.

I get paid to make whatever products I feel like to make life better for programmers. So I thought: I should design the perfect language.

What do I want in a language?

It should be hard to make mistakes

On that note let’s talk about JavaScript. It was designed to be easy to get into, and not to place too many restrictions on what you can do. But this means it’s easy to make mistakes & get unexpected results (cf. crazy stuff that happens when you add different things in JS). By restricting the types of inputs/outputs (see TypeScript), we can throw errors for incorrect input types - error messages may look like the compiler yelling at you, but really they’re saving you a bunch of work later on by telling you up front.

Let’s look at PureScript

Category theory! Semiring: something like addition/multiplication that has commutativity (a+b == b+a). Semigroup: …?

There should be no ambiguity

1 + 2 * 3

vs.

(+ 1 (* 2 3))

Pony: 1 + (2 * 3) – have to use parentheses to make precedence explicit

It shouldn’t make you think

Joe made a language at Ericsson in the late 80’s called “Erlang”. This is a gif of Joe from the Erlang movie. He’s my favorite movie star.

Immutability: In Erlang, values and variable bindings never change. At all.

This takes away some cognitive overhead (because we don’t have to think about what value a variable has at the moment)

Erlang tends to essentially fold over state: the old state is an input to the function and the new state is an output.

The “abstraction ceiling”

This term has to do with being able to express abstractions in your language.

Those of you who don’t know C: you don’t know what you’re missing, and I urge you not to find out. If garbage collection is a thing you don’t have to worry about in your language, that’s fantastic.

Elm doesn’t really let you abstract over the fact that e.g. map over array, list, set is somehow the same type of operation. So you have to provide 3 different variants of a function that can be mapped over any of the 3 types of collections. This is a bit awkward, but Elm programmers tend not to mind, because there’s a tradeoff: the fact that you can’t do this makes the type system simple so that Elm programmers get succinct, helpful error messages from the compiler.

I was learning Rust recently and I wanted to be able to express this abstraction. If you have a Collection trait, you can express that you take in a Collection and return a Collection. But you can’t specify that the output Collection has to be the same type as the incoming one. Rust doesn’t have this ability to deal with this, but they’re trying to add it.

We can do this in Haskell, because we have functors. And that’s the last time I’m going to use a term from category theory, I promise.

On the other hand, in a language like Lisp you can use its metaprogramming capabilities to raise the abstraction ceiling in other ways.

Efficiency

I have a colleague and when I suggested using OCaml as an implementation language for our utopian language, she rejected it because it was 50% slower than C.

In slower languages like Python or Ruby you tend to have performance-critical code written in the lower-level language of C.

But my feeling is that in theory, we should be able to take a language like Haskell and build a smarter compiler that can be more efficient.

But the problem is that we’re designing languages that are built on the lambda calculus and so on, but the machines they’re implemented on are not built on that idea, but rather on the Von Neumann architecture. The computer has to do a lot of contortions to take the beautiful lambda calculus idea and convert it into something that can run on an architecture designed from very different principles. This obviously complicates writing a performant and high-level language.

Rust wanted to provide a language as high-level as possible, but with zero-cost abstractions. So instead of garbage collection, Rust has a type-system-assisted kind of clean up. This is easier to deal with than the C version.

If you want persistent data structures a la Erlang or Clojure, they can be pretty efficient, but simple mutation is always going to be more efficient. We couldn’t do PDSs natively.

Suppose you have a langauge that’s low-level enough to have zero-cost abstractions, but you can plug in something like garbage collection, currying, perhaps extend the type system, so that you can write high-level programs using that functionality, but it’s not actually part of the library. I have no idea how to do this but it would be really cool.

Summing up

You need to think about:

Your language has to be open source. You can make a proprietary language, and you can make it succeed if you throw enough money at it, but even the successful historical examples of that were eventually open-sourced, which enabled their continued use. I could give a whole other talk about open source.

Functional programming & static typing for server-side web

Oskar Wickström @owickstrom

FP has been influencing JavaScript a lot in the last few years. You have ES6 functional features, libraries like Underscore, Rambda, etc, products like React with FP/FRP at their core, JS as a compile target for functional languages

But the focus is still client-side JS.

Single page applications: using the browser to write apps more like you wrote desktop apps before. Not the same model as perhaps the web browser was intended for at the beginning.

Lots of frameworks to choose from: Angular, Ember, Meteor, React&al. Without JS on the client, you get nothing.

There’s been talk recently of “isomorphic” applications: one framework which runs exactly the same way on the esrver and the client. The term is sort of stolen & not used in the same way as in category theory.

Static typing would be really useful for Middleware, which is a common abstraction but every easy to mess up if dynamically typed. In Clojure if you mess up the middleware you get the Stack Trace of Doom.

Let’s use extensible records in PureScript - shout out to Edwin’s talk related to this. That inspired me to implement this in PureScript, which started this project called Hyper which is what I’m working on right now in my free time.

Goals:

How?

Design

Functional Program Derivation

@Felienne

(Amazing, hand-drawn, animal-filled) Slides

Program derivation:

Problem => Specification => Derivation => Program

Someone said this is like “refactoring in reverse”

Generalization: introduce parameters instead of constant values

Induction: prove something for a base case and a first step, and you’ve proven it for all numbers

Induction hypothesis: if you are at step n, you must have been at step n-1 before that.

With these elements, we have a program! We just make an if/else: e.g. for sum(n), if n == 0: return 0; else return sum(n-1) + n

It all comes down to writing the right specification: which is where we need to step away from the keyboard and think.

Induction is the basis of recursion.

We can use induction to create a specification for sorting lists from which we can derive the QuickSort algorithm.

But we get 2 sorting algorithms for the price of 1: if we place a restriction that we can only do one recursive call, we can tweak the specification to derive InsertionSort, thus proving that Insertion Sort is a special case of Quick Sort.

I stole this from a PhD dissertation (“Functional Program Derivation” by ). This is all based on program derivation work by Djikstra.

Takeaways:

I’m writing a whole book on this, if you’re interested in giving feedback on chapter drafts let me know! mail at felienne dot com

Q&A:

The cake and eating it: or writing expressive high-level programs that generate fast low-level code at runtime

Nada Amin @nadamin

Distinguish stages of computation

Shonan Challenge for Generative Programming - part of the gen. pro. for HPC literature: you want to generate code that is specialized to a particular matrix

Generative Programming Patterns

Sometimes generating code is not the right solution to your problem

More info on the particular framework I’m using: Generative Programming for ‘Abstraction without Regret’

Rug: an External DSL for Coding Code Transformations (with Scala Parser-Combinators)

Jessica Kerr @jessitron, Atomist

The last talk was about abstraction without (performance) regret. This talk is about abstraction without the regret of making your code harder to read.

Elm is a particularly good language to modify automatically, because it’s got some boilerplate, but I love that boilerplate! No polymorphism, no type classes - I know exactly what that code is going to do! Reading it is great, but writing it can be a bit of a headache.

As a programmer I want to spend my time thinking about what the users need and what my program is supposed to do. I don’t want to spend my time going “Oh no, i forgot to put that thing there”.

Here’s a simple Elm program that prints “Hello world”. The goal is to write a program that modifies this existing Elm code and changes the greeting that we print.

We’re going to do this with Scala. The goal is to generate readable code that I can later go ahead and change. It’s more like a templating engine, but instead of starting with a templating file it starts from a cromulent Scala program.

Our goal is to parse an Elm file into a parse tree, which give us the meaningful bits of that file.

The “parser” in parser combinators is actually a combination of lexer and parser.

Reuse is dangerous, dependencies are dangerous, because they create coupling. (Controlled, automated) Cut & Paste is a safer solution.

at which point @jessitron does some crazy fast live coding to write an Elm parser in Scala

Rug is the super-cool open-source project I get to work on as my day job now! It’s a framework for creating code rewriters

Repo for this talk

In conclusion: any time my job feels easy, I think “OMG I’m doing it wrong”. But I don’t want to introduce abstraction into my code, because someone else is going to have difficulty reading that. I want to be able to abstract without sacrificing code readability. I can make my job faster and harder by automating it.

Relational Programming

Will Byrd

There are many programming paradigms that don’t get enough attention. The one I want to talk about today is Relational Programming. It’s somewhat representative of Logic Programming, like Prolog. I want to show you what can happen when you commit fully to the paradigm, and see where that leads us.

Functional Programming is a special case of Relational Programming, as we’re going to see in a minute.

What is functional programming about? There’s a hint in the name. It’s about functions, the idea that representing computation in the form of mathematical functions could be useful. Because you can compose functions, you don have to reason about mutable state, etc. - there are advantages to modeling computation as math. functions.

In relational programming, instead of representing computation as functions we represent it as relations. You can think of a relation in may ways. If you’re familiar with relational databases, or you can think in terms of tuples where we want to reason over sets or collections of tuples, or we can think of it in terms of algebra - like high school algebra - where we have variables representing unknown quantities and we have to figure out their values. We’ll see that we can get FP as a special case - there’s a different set of tradeoffs - but we’ll see that when you commit fully to this paradigm you can get some very surprising behavior.

Let’s start in our functional world, we’re going to write a little program in Scheme or Racket, a little program to manipulate lists. We’ll just do something simple like append or concatenate. Let’s define append in Scheme:

(define append
  (lambda (l s)
    (if (null? l)
        s
        (cons (car l) (append (cdr l) s))))

We’re going to use a relational programming language called Mini Kanren which is basically an extension that has been applied to lots of languages which allows us to put in variables representing values and ask Kanren to fill in those values.

So I’m going to define appendo. (By convention we define our names ending in -o, it’s kind of a long story, happy to explain offline.)

Writes a bunch of Kanren that we don’t really understand

Now I can do:

> (run 1 (q) (appendo '(a b c) '(d e) q))
((a b c d e))

So far, not very interesting, if this is all it does then it’s no better than append. But where it gets interesting is that I can run it backwards to find an input:

> (run 1 (X) (appendo '(a, b, c) X (a b c d e)))
((d e))

Or I can ask it to find N possible inputs:

> (run 2 (X Y) (appendo X Y (a b c d e)))
((a b c d) (e))
((a b c d e) ())

Or all possible inputs:

> (run* (X Y) (appendo X Y (a b c d e)))
((a b c d) (e))
((a b c d e) ())
...

What happens if I do this?

> (run* (X Y Z) (appendo X Y Z))

It will run forever. This is sort of like a database query, except where the tables are infinite.

One program we could write is an interpreter, an evaluator. We’re going to take an eval that’s written in MiniKanren, which is called evalo and takes two arguments: the expression to be evaluated, and the value of that expression.

> (run 1 (a) (evalo '(lambda (x) x) q))
((closure x x ()))

> (run 1 (a) (evalo '(list 'a) q))
((a))

Professor wrote a Valentine's day post "99 ways to say 'I love you' in Racket", to teach people Racket by showing 99 different racket expressions that evaluate to the list `(I love you)`

> (run 99 (q) (evalo q '(I love you)))
...99 ways...

What about quines: a quine is a program that evaluates to itself. How could we find or generate a quine?

> (run 1 (q) (evalo q q))

And twines: two different programs p and q where p evaluates to q and q evaluates to p.

> (run 1 (p q) (=/= p q) (evalo p q) (evalo q p))
...two expressions that basically quote/unquote themselves...

What would happen if we run Scheme’s append in our evaluator?

> (run 1 (q)
    (evalo
      `(letrec ((append
                  (lambda (l s)
                    (if (null? l)
                        s
                        (cons (car l)
                              (append (cdr l)
                                      s)))))))
          (append '(a b c) '(d e))
      q))
((a b c d e))

But we can put the variable also inside the definition of append:

> (run 1 (q)
    (evalo
      `(letrec ((append
                  (lambda (l s)
                    (if (null? l)
                        q
                        (cons (car l)
                              (append (cdr l)
                                      s)))))))
          (append '(a b c) '(d e))
      '(a b c d e)))
(s)

Now we’re starting to synthesize programs, based on specifications. When I gave this talk at PolyConf a couple of years ago Jessitron trolled me about how long it took to run this, since then we’ve gotten quite a bit faster.

This is a tool called Barliman that I (and Greg Rosenblatt) have been working on, and it’s basically a frontend, a dumb GUI to the interpreter we were just playing with. It’s just a prototype. We can see a partially specified definition - a Scheme function that’s partially defined, with metavariables that are fill-in-the-blanks for some Scheme expressions that we don’t know what they are yet. Barliman’s going to guess what the definition is going to be.

(define ,A
    (lambda ,B
      ,C))

Now we give Barliman a bunch of examples. Like (append '() '()) gives '(). It guesses what the missing expressions were based on those examples. The more test cases we give it, the better approximation of the program it guesses. With 3 examples, we can get it to correctly guess the definition of append.

Yes, you are going to lose your jobs. Well, some people are going to lose their jobs. This is actually something that concerns me, because this tool is going to get a lot better.

If you want to see the full dog & pony show, watch the ClojureConj talk I gave with Greg.

Writing the tests is indeed the harder part. But if you’re already doing TDD or property-based testing, you’re already writing the tests, why don’t you just let the computer figure out the code for you based on those tests?

Some people say this is too hard, the search space is too big. But that’s what they said about Go, and it turns out that if you use the right techniques plus a lot of computational power, Go isn’t as hard as we thought. I think in about 10-15 years program synthesis won’t be as hard as we think now. We’ll have much more powerful IDEs, much more powerful synthesis tools. It could even tell you as you’re writing your code whether it’s inconsistent with your tests.

What this will do for jobs, I don’t know. I don’t know, maybe it won’t pan out, but I can no longer tell you that this definitely won’t work. I think we’re at the point now where a lot of the academic researchers are looking at a bunch of different parts of synthesis, and no one’s really combining them, but when they do, there will be huge breakthroughs. I don’t know what it’s going to do, but it’s going to do something.

Working hard to keep things lazy

Raichoo @raichoo

Without laziness, we waste a lot of space, because when we have recursion we have to keep allocating memory for each evaluated thing. Laziness allows us to get around that.

What is laziness, from a theoretical standpoint?

The first thing we want to talk about is different ways to evaluate expressions.

> f x y = x + y
> f (1 + 1) (2 + 2)

How do we evaluate this?

=> (1 + 1) + (2 + 2)
=> 2 + 4
=> 6

This evaluation was normal form

Church-Rosser Theorem: the order of evaluation doesn’t matter, ultimately a lambda expression will evaluate to the same thing.

But! We have things like non-termination, and termination can only be determined after the fact.

Here’s a way we can think of types: Let’s think of a Boolean as something which has three possible values: True, False, and “bottom”, which represents not-yet-determined, a computation that hasn’t ended yet. True and False are more defined than bottom (e.g. _|_ <= True). Partial ordering.

Monotone functions: if we have a function that takes a Bool and returns a Bool, and x and y are bools where x <= y, then f x <= f y. We can now show that f _|_ = True and f x = False doesn’t work out, because it would have the consequence that True => False, which doesn’t work - that’s a good thing because if it did, we would have solve the halting problem. What’s nice here is that if we write a function and evaluate it in normal order, in the lazy way, then this naturally works out.

Laziness is basically non-strictness (this normal order thing I’ve been talking about the whole time), and sharing.

Laziness lets us reuse code and use combinators. This is something I miss from Haskell when I use any other language.

Honorable mention: Purely Functional Data Structures by Chris Okasaki. When you have Persistent Data Structures, you need laziness to have this whole amortization argument going on. This book introduces its own dialect of ML (lazy ML).

How do we do laziness in Haskell (in GHC)? At an intermediate stage of compilation called STG, Haskell takes unoptimized code and optimizes it to make it lazy. (???)

Total Functional Programming

Edwin Brady @edwinbrady

Idris is a pure functional language with dependent types. It’s a “total” language, which means you have program totality: a program either terminates, or gives you new results.

Goals are:

People on the internet say, you can’t do X, you can’t do Y in a total language. I’m going to do X and Y in a total language.

Types become plans for a program. Define the type up front, and use it to guide writing the program.

You define the program interactively. The compiler should be less like a teacher, and more like a lab assistant. You say “let’s work on this” and it says “yes! let me help you”.

As you go, you need to refine the type and the program as necessary.

Test-driven development has “red, green, refactor”. We have “type, define, refine”.

If you care about types, you should also care about totality. You don’t have a type that completely describes your program unless your program is total.

Given f : T: if program f is total, we know that it will always give a result of type T. If it’s partial, we only know that if it gives a result, it will be type T, but it might crash, run forever, etc. and not give a result.

The difference between total and partial functions in this world: if it’s total, we can think of it as a Theorem.

Idris can tell us whether or not it thinks a program is total (though we can’t be sure, because we haven’t solved the halting problem “yet”, as a student once wrote in an assignment). If I write a program that type checks but Idris thinks it’s possibly not total, then I’ve probably done the wrong thing. So in my Idris code I can tell it that some function I’m defining should be total.

I can also tell Idris that if I can prove something that’s impossible, then I can basically deduce anything, e.g. an alt-fact about arithmetic. We have the absurd keyword.

We have Streams, where a Stream is sort of like a list without nil, so potentially infinite. As far as the runtime is concerned, this means this is lazy. Even though we have strictness.

Idris uses IO like Haskell to write interactive programs. IO is a description of actions that we expect the program to make(?). If you want to write interactive programs that loop, this stops it being total. But we can solve this by describing looping programs as a stream of IO actions. We know that the potentially-infinite loops are only going to get evaluated when we have a bit more information about what the program is going to do.

Turns out, you can use this to write servers, which run forever and accept responses, which are total. (So the people on the internet are wrong).

Check out David Turner’s paper “Elementary Strong Functional Programming”, where he argues that totality is more important than Turing-completeness, so if you have to give up one you should give up the latter.

Book coming out: Type-Driven Development with Idris