Questions about a la carte data types

Question

I was reading the original paper about data types a la carte and decided to try to implement the idea in Scala (I know it's already implemented in many functional libraries). Unfortunately I found the original paper is hard to comprehend and I stuck somewhere in the beginning. Then I found another paper that was easier to understand and I managed to rewrite Haskell code from the paper into Scala, you can find it here. However I still struggling to understand a few moments:

1. A quote from the second paper

Orignal Expr data type

data Expr = Val Int | Add Expr Expr

New type signature:

data Arith e = Val Int | Add e e

For any functor f, its induced recursive datatype, Fix f, is defined as the least fixpoint of f, implemented as follows:

data Fix f = In (f (Fix f))

Now that we have tied the recursive knot of a signature, Fix Arith is a language equivalent to the original Expr datatype which allowed integer values and addition.

What does it mean exactly "we have tied the recursive knot of a signature" and what does it mean Fix Arith is a language equivalent to the original Expr ?

The actual type of In is In :: f (Fix f) -> Fix f If we try to construct a value using In construct and Val 1 variable we'll get the following result:

> :t  In(Val 1)
> In(Val 1) :: Fix Arith

Scala encoding of the same data types:

  sealed trait Arith[A]
  case class Val[A](x: Int) extends Arith[A]
  case class Add[A](a: A, b: A) extends Arith[A]

  trait Fix[F[_]]
  case class In[F[_]](exp: F[Fix[F]]) extends Fix[F]

2. fold function The fold function has the following signature and implementation

Haskell:

fold :: Functor f => (f a -> a) -> Fix f -> a
fold f (In t) = f (fmap (fold f) t)

Scala variant I came up with

  def fold[F[_] : Functor, A](f: F[A] => A): Fix[F] => A = {
    case In(t) =>
      val g: F[Fix[F]] => F[A] = implicitly[Functor[F]].lift(fold(f))
      f(g(t))
  }

The thing that I'm curious about is that in my Scala version function g has the following type F[Fix[F]] => F[A] but the type of variable t after pattern matching is LaCarte$Add with value Add(In(Val(1)),In(Val(2))), how it happens that it's valid to apply function g to LaCarte$Add ? Also, I'd very appreciate if you can help me to understand fold function ?

Quote from the paper:

The first argument of fold is an f-algebra, which provides the behavior of each constructor associated with a given signature f.

Answer 1

What does it mean exactly “we have tied the ‘recursive knot’ of a signature”?

The original Expr datatype is recursive, referring to itself in its own definition:

data Expr = Val Int | Add Expr Expr

The Arith type “factors out” the recursion by replacing recursive calls with a parameter:

data Arith e = Val Int | Add e e

The original Expr type can have any depth of nesting, which we want to support with Arith as well, but the maximum depth depends on what type we choose for e:

• Arith Void can’t be nested: it can only be a literal value (Val n) because we can’t construct an Add, because we can’t obtain a value of type Void (it has no constructors)

• Arith (Arith Void) can have one level of nesting: the outer constructor can be an Add, but the inner constructors can only be Lit.

• Arith (Arith (Arith Void)) can have two levels

• And so on

What Fix Arith gives us is a way to talk about the fixed point Arith (Arith (Arith …)) with no limit on the depth.

This is just like how we can replace a recursive function with a non-recursive function and recover the recursion with the fixed-point combinator:

factorial' :: (Integer -> Integer) -> Integer -> Integer
factorial' recur n = if n <= 1 then 1 else n * recur (n - 1)

factorial :: Integer -> Integer
factorial = fix factorial'

factorial 5 == 120

What does it mean Fix Arith is a language equivalent to the original Expr?

The language (grammar) that Fix Arith represents is equivalent to the language that Expr represents; that is, they’re isomorphic: you can write a pair of total functions Fix Arith -> Expr and Expr -> Fix Arith.

How it happens that it’s valid to apply function g to LaCarte$Add?

I’m not very familiar with Scala, but it looks like Add is a subtype of Arith, so the parameter of g of type F[Fix[F]] can be filled with a value of type Arith[Fix[Arith]] which you get by matching on the In constructor to “unfold” one level of recursion.