Skip to content

Instantly share code, notes, and snippets.

@mmenestret
Last active April 19, 2024 14:19
Show Gist options
  • Star 18 You must be signed in to star a gist
  • Fork 4 You must be signed in to fork a gist
  • Save mmenestret/0b746cfd650796a639723ee74a3de302 to your computer and use it in GitHub Desktop.
Save mmenestret/0b746cfd650796a639723ee74a3de302 to your computer and use it in GitHub Desktop.
FP and tagless final - Fabio Labella

Purity and pure FP

  • purity is a syntactical property of programs, more precisely defined as referential transparency: replacing an expression for its bound value doesn't change meaning (precise definition)
  • side effects are things that break referential transparency (precise definition)
  • There's no direct connection between the concepts of IO, State and so on, and side effects. Traditionally, these things are side effectful (break referential transparency), but you can have abstractions that are pure (don't break ref.trans.)
  • Due to the above, the term purely functional programming is not an oxymoron, it makes perfect sense.
  • In haskell style pure FP, type constructors and algebras are used to represent "things that would otherwise traditionally be side effects (break ref.trans.)". We call these F[]s effects or computational contexts for brevity. You can see for yourself how this cannot be a precise definition (especially because they could also have kind higher than * -> *, even though most famous algebras like Functor and Monad operate on F[]

I guess the other thing to add is that purity really matters a lot, it's not pedantry. Referentially transparent expressions respect the substitution model, which means you can use local reasoning only to understand and compose your programs, which is a huge win

Initial vs final encoding

Generally speaking final tagless is a technique for encoding DSLs, these days, often it's used to mean "a final tagless encoding of an effectful algebra", like a DB or something The general idea is simple:

trait KVS[F[_]] {
   def put(k: String, v: String): F[Unit]
   def get(k: String): F[Option[String]]
}

F will be replaced by a concrete type like cats.effect.IO, or Kleisli[IO, DbConnection, ?], that's the gist of it really.

The domain all this originated is EDSLs (embedded domain specific languages). The most intuitive way of writing one is by writing a data structure that represent your EDSL, then interpreting it into something else, e.g. data Op = Add Int Int | Const Int plus a function from Op to whatever you want to interpret this to (e.g. an Int for evaluation, or a String for pretty printing). This is an example of an initial encoding, also referred to as a deep embedding, what you had there is therefore initial, an AST basically.

The Free monad is another example of this: your EDSL is "monadicity", and you represent that by a concrete data structure, which you then interpret to something else. A final encoding is when you represent your mini language using functions, i.e. directly in terms of what are going to be the interpreters (the eliminators of your language/edsl/algebra).

data Exp = Add Exp Exp | Lit Int
sealed trait Exp
case class Add(l: Exp, r: Exp) extends Exp
case class Lit(i: Int) extends Exp

So that we can nest expressions like Add(Lit(1), Add(Lit(3), Lit(3)), interpretation for this style is just a function that uses pattern matching and recursion.

The same thing in final style would be:

class Exp t where
   lit :: Int -> t
   add :: t -> t -> t
trait Exp[T] {
  def lit(i: Int): T
  def add(l: T, r: T): T
}

We're using typeclasses and, more generally, functions, to represent our expressions. What do these function represent? they represent the interpreters for each instruction, for example, let's see how to evaluate both styles to an Int:

First one would be:

def rec(exp: Exp): Int { exp match { case Add(l, r) => rec(l) + rec(r); case Lit(i) => i }}

Second one would be:

new Exp[Int] { def lit(i: Int): Int = i def add(l: Int, r: Int): Int = l + r }

So when you write an expression def expr[A]: Expr[A] = add(lit(1), add(lit(3), lit(5)) // not valide code, quickly typed, you are already calling the evaluator, so to speak. Btw, that trait (at least in Haskell) is normally encoded as a type class and instead of Exp[Int], you create a newtype over Int, and use that as your target. So in tagless style interpretation is the identity function in Haskell (since the typeclass dictionary can't be touched) it's kinda in between in scala, depends on whether you pass the instance implicitly or not but that's the gist of what the two approaches are.

If you squint, you can recognise the philosophy between Free and mtl (encoding effects in final tagless style, which is what you see in most scala examples) as being initial vs final and even by just looking at the Exp example, we can already talk a bit about the tradeoffs between Free and mtl.

In short:

  • In an initial dsl you write a concrete datatype, then you interpret it
  • In a final dsl you write things directly in terms of the functions that will interpret them (I promise the longer explanation is clearer) When we apply these two philosophies to effects the initial approach is the Free monad, we create a concrete datatype (Free, basically a tree), then interpret it.

Tagless

so the tagless thing comes into play when you want your EDSL to be typed let's start with a very simple example, in initial encoding

data Expr =
  =  I Int
   | B Bool
   | Eq Expr Expr
   | Add Expr Expr
sealed trait Expr 
case class B(b: Boolean) extends Expr
case class I(i: Int) extends Expr
case class Eq(l: Expr, r: Expr) extends Expr
case class Add(l: Expr, r: Expr) extends Expr

Note that in the formulation above, we can now construct things that are ill-typed from our dsl point of view. The first thing you could do is to pass along a runtime tag to Expr (for example a String), which encodes what type the expression is supposed to be.

case class Add(tag = "Int", l: Expr, r: Expr)

Then, when interpreting, you use the String to perform casting (returning an error while evaluating if things are ill-typed) such an approach would be initial-tagged but we can do a few things to make it initial tagless. The first approach is to use phantom types to track type info.

sealed trait Expr[A] 
case class B(b: Boolean) extends Expr[A]
case class I(i: Int) extends Expr[A]
case class Eq(l: Expr[A], r: Expr[A]) extends Expr[A]
case class Add(l: Expr[A], r: Expr[A]) extends Expr[A]

We then make the constructors private, and expose

def add(l: Expr[Int], r: Expr[Int]): Expr[Int] = Add(l, r)

Do you think this will work? It doesn't, it works for creating expression but during interpretation you'd have no way to know which types do the inner expression have when pattern matching (you want to write the interpreter for Expr[A]).

The solution to an initial tagless encoding is GADTs

sealed trait Expr[A] 
case class B(b: Boolean) extends Expr[Boolean]
case class I(i: Int) extends Expr[Int]
case class Eq(l: Expr[Int], r: Expr[Int]) extends Expr[Boolean]
case class Add(l: Expr[Int], r: Expr[Int]) extends Expr[Int]
data Expr a where
   I   :: Int  -> Expr Int
   B   :: Bool -> Expr Bool
   Add :: Expr Int -> Expr Int -> Expr Int
   Mul :: Expr Int -> Expr Int -> Expr Int
   Eq  :: Expr Int -> Expr Int -> Expr Bool

In haskell, when you pattern match on a gadt, each branch will know the correct type, and everything will work out

eval :: Expr a -> a
eval (I n) = n
eval (B b) = b
eval (Add e1 e2) = eval e1 + eval e2
eval (Mul e1 e2) = eval e1 * eval e2
eval (Eq  e1 e2) = eval e1 == eval e2

See how the add branch knows it can add the result of evaluating Add.

The equivalent scala will sometimes work, sometimes won't, sometimes will work with horrid tricks (do you know that a lowercase variable in pattern match introduce an existential), and in almost every case will bring you to a state that oscillates between fury, exhilaration and sorrow. That being said, it does work in some case, e.g. that's what you do with Free you write your algebra as a GADT. GADTs are initial tagless encodings, the nice thing about the final encoding we were talking about before is that it just doesn't have this problem: it is indeed final tagless. The moniker "finally tagless" was a pun on finally getting to a final tagless encoding in the original paper "finally tagless, partially evaluated".

Tagless final

Final tagless is a general technique for building DSLs (domain specific languages, algebras, however you want to call them). There is no requirement to use F[], it works for A as well. The way it's used more often than not is with F[] (so, with higher-kinded things). This doesn't really need a new name, it's still 100% final tagless, but the application of final tagless to effects is known as mtl-style, from the haskell library called mtl which popularised it at first. It's not a great name however, because mtl means monad transformer library, which made sense historically because the library used to provide monad transformers as well, but doesn't really make sense anymore, since the technique of encoding effects in final tagless style isn't really linked to monad transformers necessarily, or even to monads (you can have less powerful ones with Applicative, or more powerful ones with Sync.

trait Num[A] {
  def add(a: A, b: A): A
  def const(a: Int): A
}

That is a typeclass, that's how you implement final tagless style in haskell (you could also use records of functions or modules in ML) That's still final tagless. F[_] is a special case that happens to be use to reprensents effectful computation.

What if there is no typeclass covering the specifics I need ? Then you can create your own, in fact, that's what you do all the time.

You start by imagining a language in which the problem you need to solve is easy, encode that in one or more final tagless algebras, write most of your code in terms of that, and now you have reduced your complex problem to the simpler case of implementing the primitives of your language. My approach is that when I need a new concern, I just imagine an algebra for it.

If the typeclass at your disposal does not expose the behavior you need, create your own

Yes absolutely, that's the point. And you know what actually, the opinion of some in the haskell community is actually that using MonadState and so on is often an antipattern and the typeclasses you use should actually mirror your domain so, Counter[F] over MonadState[F, Int] because MonadState is too wide and Counter is also more descriptive, the resulting code maps better to your problem domain. You can still use MonadState at the layer below, to implement Counter, or not, and go for a specific type.

About inner State in a F[_] context that shouldn't be exposed to the outside world

Well, in that case, you want to interpret (run the state) in which case using a concrete interpreter (so StateT, interpreters are generally concrete types) is not that bad. Or, you need to have some constraint at the higher level. You can then have multiple alternatives, but you still ended up with at least one constraint on the higher level, or a concrete type, that's unavoidable. You can make your own abstraction as well, in another 5 or 6 different ways, but at the end of the day, either you will have a concrete type for that layer of interpretation, or some constraint at the higher level. This is not a limitation, it's unavoidable, think about this: If you don't give a concrete type (an interpreter, so StateT), or a constraint describing an interpreter (a million choices here), how the hell am I supposed to interpret that layer? With what semantics?

My intuition was to be able to have a G[] algebra which would produce a G[F[]] -> Yes, you can do that, but then you have a G constraint above. For example, you could create MonadState with Ref, but now you need something to create Refs, so Concurrent You can create a typeclass just for creating Ref, but now you will have that constraint on the outer one, and so on... You cannot create it out of thin air.

There is a third choice: you go back to initial and return a concrete datatype (like Free of something), but still, you haven't run anything unless you have an interpreter for that. At the end of the day, either you delay intepretation, or when you want to interpret you need to give me a concrete interpreter or an abstraction over the intepreter.

Stuff

  • Rob Norris: I think we're kind of moving away from the idea of fixed effect stacks. In tagless style every method demands the effects it needs and the "stack" ends up being a dependency graph you have to satisfy at the end of the (local) world, but you 're never really programming in it. So all transformer use becomes transient. You construct one and quickly discharge it.

  • Exemple of pure FP / tagless final approach

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment