zraffer

Alternative to the Church, Scott and Parigot encodings of data on the Lambda Calculus.

When it comes to encoding data on the pure λ-calculus (without complex extensions such as ADTs), there are 3 widely used approaches.

Church Encoding

The Church Encoding, which represents data structures as their folds. Using Caramel’s syntax, the natural number 3 is, for example. represented as:

0 c0 = (f x -> x)
1 c1 = (f x -> (f x))
2 c2 = (f x -> (f (f x)))

zraffer

Introductory Material

• Add Graal JIT Compilation to Your JVM Language in 5 Steps, A Tutorial http://stefan-marr.de/2015/11/add-graal-jit-compilation-to-your-jvm-language-in-5-easy-steps-step-1/

• The SimpleLanguage, an example of using Truffle with great JavaDocs. It is the officle getting-started project: https://github.com/graalvm/simplelanguage

• Truffle Tutorial, Christan Wimmer, PLDI 2016, 3h recording https://youtu.be/FJY96_6Y3a4 Slides

zraffer

sealed trait Free[F[_], A] { self =>
  final def map[B](ab: A => B): Free[F, B] = Free.flatMap(self, ab andThen (Free.point[F, B](_)))
  final def flatMap[B](afb: A => Free[F, B]): Free[F, B] = Free.flatMap(self, afb)
  final def interpret[G[_]: Monad](fg: F ~> G): G[A] = self match {
    case Free.Point(a0) => a0().point[G]
    case Free.Effect(fa) => fg(fa)
    case fm : Free.FlatMap[F, A] =>
    	val ga0 = fm.fa.interpret[G](fg)
    	ga0.flatMap(a0 => fm.afb(a0).interpret[G](fg))
  }

zraffer

Fix : (Type -> Type) -> Type
Fix f = {x : Type} -> (f x -> x) -> x

fold : Functor f => {x : Type} -> (f x -> x) -> Fix f -> x
fold k t = t k

embed : Functor f => f (Fix f) -> Fix f
embed s k = k (map (fold k) s)

project : Functor f => Fix f -> f (Fix f)

zraffer

%default total

data Mu : (Type -> Type) -> Type where
    In : f (Mu f) -> Mu f

out : Mu f -> f (Mu f)
out (In x) = x

data LstF : Type -> Type -> Type where
    LF : ({c : Type} -> (Maybe (a, Unit -> c, b) -> c) -> c) -> LstF a b

zraffer

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE Rank2Types #-}

import Data.Maybe

data List a = L (forall b. (Maybe (a, (b, List a)) -> b) -> b)

nil :: List a
nil = L (\f -> f Nothing)