Tagless Final
un pont entre théorie et pratique
Frédéric Cabestre
@fcabestre
I'm not a number, I'm a freelance.— Number 6, The Prisoner
Il était une fois…
Problématique
$\frac{n\, \mathrm{est \, un \, entier}}{n\, :\, \mathbb{Z}}$
$\frac{b\, \mathrm{est \, un \, booleen}}{b\, :\, \mathbb{B}}$
$\frac{e\, :\, \mathbb{Z}}{- e\, :\, \mathbb{Z}}$
$\frac{e_1\, :\, \mathbb{Z} \;\;\; e_2\, :\, \mathbb{Z}}{e_1\, + \,e_2 \, :\, \mathbb{Z}}$
$\frac{e_1\, :\, \mathbb{Z} \;\;\; e_2\, :\, \mathbb{Z}}{e_1\, \times \,e_2 \, :\, \mathbb{Z}}$
$\frac{e_1\, :\, \mathbb{Z} \;\;\; e_2\, :\, \mathbb{Z}}{e_1\, \leq \,e_2 \, :\, \mathbb{B}}$
$\frac{e_1\, :\, \mathbb{B} \;\;\; e_2\, :\, \mathbb{B}}{e_1\, \land \,e_2 \, :\, \mathbb{B}}$
$\frac{e_1\, :\, \mathbb{B} \;\;\; e_2\, :\, \mathbb{B}}{e_1\, \lor \,e_2 \, :\, \mathbb{B}}$
Codage Initial
Syntaxe abstraite $\equiv$ Type Abstrait de Donnée
sealed trait Exp
case class Num(i: Int) extends Exp
case class Bool(b: Boolean) extends Exp
case class Neg(e: Exp) extends Exp
case class Add(e1: Exp, e2: Exp) extends Exp
case class Mul(e1: Exp, e2: Exp) extends Exp
case class Or(e1: Exp, e2: Exp) extends Exp
case class And(e1: Exp, e2: Exp) extends Exp
case class Leq(e1: Exp, e2: Exp) extends Exp
Codage Initial
- $ti_1 \,=\, 8 \,-\,(1 \,+\, 2)$
- $ti_2 \,=\, 7 \,\times\, ti_1$
- $ti_3 \,=\, (ti_1\,\leq\, ti_2) \,\lor\, (0 \,\leq\, ti_2)$
val ti1: Add = Add(Num(8), Neg(Add(Num(1), (Num(2)))))
val ti2: Mul = Mul(Num(7), ti1)
val ti3: Or = Or(Leq(ti2, ti1), Leq(Num(0), ti2))
Codage Initial
Evaluateur de la syntaxe abstraite
object Exp {
def eval = {
case Num(i) => i
case Bool(b) => b
case Neg(e) => - eval(e)
case Add(e1, e2) => eval(e1) + eval(e2)
case Mul(e1, e2) => eval(e1) * eval(e2)
case Or(e1, e2) => eval(e1) || eval(e2)
case And(e1, e2) => eval(e1) && eval(e2)
case Leq(e1, e2) => eval(e1) <= eval(e2)
}
}
Type Universel
Type somme $\longrightarrow$ Tag
trait U {
def asI: Int = this match { case UI(i) => i }
def asB: Boolean = this match { case UB(b) => b }
}
case class UB(b: Boolean) extends U
case class UI(i: Int) extends U
Codage Tagged Initial
object Exp {
def eval: Exp => U = {
case Num(i) => UI(i)
case Bool(b) => UB(b)
case Neg(e) => UI(-eval(e).asI)
case Add(e1, e2) => UI(eval(e1).asI + eval(e2).asI)
case Mul(e1, e2) => UI(eval(e1).asI * eval(e2).asI)
case Or(e1, e2) => UB(eval(e1).asB || eval(e2).asB)
case And(e1, e2) => UB(eval(e1).asB && eval(e2).asB)
case Leq(e1, e2) => UB(eval(e1).asI <= eval(e2).asI)
}
}
Codage Tagged Initial
Évaluation d'un terme
Exp.eval(ExpSamples.ti3).asB == true
Limitations
- Filtrage de la syntaxe abstraite
- Type universel pour les résultats
- Termes mal formés
val tie: Neg = Neg(Bool(false))
Exp.eval(ExpSamples.tie).asB // throws MatchError
Codage Final
Constucteurs de types $\longrightarrow$ Combinateurs
object Exp {
def num(i: Int): Int = i
def neg(r: Int): Int = - r
def add(r1: Int, r2: Int): Int = r1 + r2
}
val tf1: Int = add(num(8), neg(add(num(1), num(2))))
Paramétrisons
- Codage Initial $\rightarrow$ famille de fonctions eval
- Codage Final $\rightarrow$ représentation et evaluation mélées
- Les Type Classes à la rescousse
« Poor Man's Type Classes »
Type classes
- Traitement rigoureux du polymorphisme ad-hoc
- Extension retroactive
- Programmation Générique
- Programmation au niveau des types
- Statique $\neq$ Liaison retardée
Type classes
Façon Java
def sort[T](l: List[T], ord: Ord[T]): List[T] = ???
trait Ord[T] {
def compare(a: T, b: T): Boolean
}
val intOrd: Ord[Int] = new Ord[Int] {
override def compare(a: Int, b: Int): Boolean = a <= b
}
val res: List[Int] = sort(List(26, 1, 1969),intOrd)
Type classes
Façon Scala
def sort[T](l: List[T])(implicit ord: Ord[T]): List[T] = ???
- Identique à
def sort[T: Ord](l: List[T]): List[T] = ???
implicit val intOrd: Ord[Int] = new Ord[Int] {
override def compare(a: Int, b: Int): Boolean = a <= b
}
val res: List[Int] = sort(List(26, 1, 1969))
Codage Final (suite)
trait ExpSym[R] {
def num(i: Int): R
def neg(r: R): R
def add(r1: R, r2: R): R
}
def tf1[R: ExpSym]: R = {
val e = implicitly[ExpSym[R]]
e.add(e.num(8), e.neg(e.add(e.num(1), e.num(2))))
}
Codage Final
Interpretation dans le domaine des entiers
object ExpSymInt {
implicit val expSymInt: ExpSym[Int] = new ExpSym[Int] {
def num(i: Int): Int = i
def neg(r: Int): Int = -r
def add(r1: Int, r2: Int): Int = r1 + r2
}
}
import net.sigusr.it1_5.ExpSymInt.expSymInt
ExpSymSamples.tf1 == 5
Codage Final
Interpretation dans le domaine des chaînes de caractères
object ExpSymString {
implicit val expSymString: ExpSym[String] = new ExpSym[String] {
def num(i: Int): String = i.toString
def neg(r: String): String = s"(-$r)"
def add(r1: String, r2: String): String = s"($r1 + $r2)"
}
}
import net.sigusr.it1_5.ExpSymString.expSymString
ExpSymSamples.tf1 must_== "(8 + (-(1 + 2)))"
Codage Final
Extension de l'interpretation
trait MulSym[R] {
def mul(r1: R, r2: R): R
}
def tf2[R:ExpSym: MulSym]: R = {
val e = implicitly[ExpSym[R]]
val m = implicitly[MulSym[R]]
m.mul(e.num(7), ExpSymSamples.tf1)
}
Codage Final
Extension de l'interpretation
object MulSymInt {
implicit val mulSymInt: MulSym[Int] =
(r1: Int, r2: Int) => r1 * r2
}
object MulSymString {
implicit val mulSymString: MulSym[String] =
(r1: String, r2: String) => s"($r1 * $r2)"
}
Codage Final
- Et Rust dans tout ça ?
pub trait ExpSym {
fn num(i: u64) -> Self;
fn neg(r: Self) -> Self;
fn add(r1: Self, r2: Self) -> Self;
}
pub fn tf1<T: ExpSym>() -> T {
ExpSym::add(
ExpSym::lit(8),
ExpSym::neg(
ExpSym::add(ExpSym::lit(1), ExpSym::lit(2))))
}
Codage Final
- Et Rust dans tout ça ?
pub trait MulSym {
fn mul(r1: Self, r2: Self) -> Self;
}
pub fn tf2<T: ExpSym + MulSym>() -> T {
MulSym::mul(ExpSym::lit(7), tf1())
}
Codage Final
- Et Rust dans tout ça ?
impl ExpSym for i128 {
fn num(i: u64) -> Self { i as i128 }
fn neg(r: Self) -> Self { -r }
fn add(r1: Self, r2: Self) -> Self { r1 + r2 }
}
impl MulSym for String {
fn mul(r1: Self, r2: Self) -> Self {
format!( "({} * {})", r1, r2)
}
}
Codage Tagless
- Ajout des expressions booléennes
- Toujours le problème du typage
- Types d'ordre supérieur
- Haskell, O'Caml, Scala... Mais pas Rust
Codage Tagless
trait BoolSym[R[_]] {
def bool(b: Boolean): R[Boolean]
def leq(r1: R[Int], r2: R[Int]): R[Boolean]
def or(r1: R[Boolean], r2: R[Boolean]): R[Boolean]
def and(r1: R[Boolean], r2: R[Boolean]): R[Boolean]
}
def tf3[R[_]:ExpSym: MulSym: BoolSym]: R[Boolean] = {
val e = implicitly[ExpSym[R]]
val b = implicitly[BoolSym[R]]
b.or(
b.leq(MulSymSamples.tfm2, ExpSymSamples.tf1),
b.leq(e.num(0), MulSymSamples.tfm2)
)
}
Codage Tagless
type I[A] = A
I est de sorte $*\,\rightarrow\,*$
object BoolSymI {
implicit val boolSymI: BoolSym[I] = new BoolSym[I] {
def bool(b: Boolean): I[Boolean] = b
def leq(r1: I[Int], r2: I[Int]): I[Boolean] = r1 <= r2
def or(r1: I[Boolean], r2: I[Boolean]): I[Boolean] = r1 || r2
def and(r1: I[Boolean], r2: I[Boolean]): I[Boolean] = r1 && r2
}
}
Codage Tagless
- $tf_1 \,=\, 8 \,-\,(1 \,+\, 2)$
- $tf_2 \,=\, 7 \,\times\, ti_1$
- $tf_3 \,=\, (ti_1\,\leq\, ti_2) \,\lor\, (0 \,\leq\, ti_2)$
import ExpSymI.expSymI
import MulSymI.mulSymI
import BoolSymI.boolSymI
BoolSymSamples.tf3 must_== true
Oui mais... Dans la vraie vie
- Parametrisation d'un programme par un contexte d'execution
- Principe de moindre pouvoir (least power)
- Inconvenient : contamine toute la base de code
- Cas d'usage: écriture de librairie
Exemple: IO Monads
- Gestion référentiellement transparente des effets
- Embedded Domain Specific Language
- Composé d'un ensemble de « type classes »
- Type classes de Cats effect : Bracket, Sync, Concurrent, ...
- Instances de Cats effect : Cats effect IO, Monix Task, ZIO, ...
- Description d'un programme d'effets
- Interprétation « à la fin du monde »
Shameless Plug: fs2-mqtt
trait Session[F[_]] {
def messages(): Stream[F, Message]
def subscribe(topics: Vector[(String, QualityOfService)]):
F[Vector[(String, QualityOfService)]]
def unsubscribe(topics: Vector[String]): F[Unit]
def publish(
topic: String,
payload: Vector[Byte],
qos: QualityOfService = AtMostOnce,
retain: Boolean = false
): F[Unit]
def state: SignallingRef[F, ConnectionState]
}
Shameless Plug: fs2-mqtt
object Session {
def apply[F[_]: Concurrent: Timer: ContextShift](
transportConfig: TransportConfig[F],
sessionConfig: SessionConfig
): Resource[F, Session[F]] = ...
}
Ressources
- Finally Tagless, Partially Evaluated [PDF]
- Typed Tagless Final Interpreters [PDF]
- How to make ad-hoc polymorphism less ad hoc [PDF]
- Implementing Haskell Overloading [PDF]
- Implementing, and Understanding Type Classes [BLOG]
- Type Classes as Objects and Implicits [PDF]
- IO monad: which, why and how [BLOG]
- fs2-mqtt [CODE]
- Code de cette présentation [CODE]
Frédéric Cabestre
@fcabestre