Codensity and ContT

Question

While studying functional programming and exploring the concept of continuations, I became acquainted with the types (monad transformers) Codensity and ContT. They look similar, but it is still not clear how they relate. It seems like Codensity is more primary than ContT, doesn't it?

In Scala 3, such types can be written like this:

type Codensity = [F[_]] =>> [A] =>> [B] => (A => F[B]) => F[B]
type ContT     = [F[_]] =>> [A, B]     =>> (A => F[B]) => F[B]

How to infer the type of ContT when Codensity is specified (assuming we don’t know in advance what ContT is)? And on what grounds? Or some other inference of one type based on another?

Answer 1

You're right. The difference is not only in currying (polymorphic function vs. type lambda).

How to infer the type of ContT when Codensity is specified

How would you answer your question in easier situation?

type X = [A] =>> List[A]
type Y = [A] => () => List[A] // it would be better to write [A] => List[A]
                              // but it's forbidden in Scala for technical reasons

"How to infer the type of X when Y is specified?"

X is a type depending on A. Y is a type whose term (value) depends on A.

X is List. Y is inhabited for example with Nil[A] (if we consider invariant list i.e.

sealed trait List[A]
case class Cons[A](head: A, tail: List[A]) extends List[A]
case class Nil[A]() extends List[A]

instead of

sealed trait List[+A]
case class Cons[+A](head: A, tail: List[A]) extends List[A]
case object Nil extends List[Nothing]

).

Relation between two types is the following. For a value of type Y, this value applied to A belongs to the type X applied to A.

It seems like Codensity is more primary than ContT, doesn't it?

Is type constructor List more primary than polymorphic function Nil[A]?

---

type ContT     = [F[_]] =>> [A, B]     =>> (A => F[B]) => F[B]
type Codensity = [F[_]] =>> [A] =>> [B] => (A => F[B]) => F[B]

Here in order to get a proper type (i.e. a type of kind *), for ContT we have to fix F, A, B, for Codensity we have to fix F, A.

[B] =>> (A => F[B]) => F[B] is a type depending on B. [B] => (A => F[B]) => F[B] is a type whose term depends on B.

Relation between two types is the following. For a value of type Codensity[F][A], this value applied to B belongs to the type ContT[F][A, B]

type F[_]
type A
type B
type X = ContT[F][A, B]
val x: X = ???
type Y = Codensity[F][A]
val y: Y = ???
y[B]: X