Skip to content

Instantly share code, notes, and snippets.

@Odomontois
Created February 22, 2018 16:16
Show Gist options
  • Save Odomontois/63a3e20b1389b7ec9cb0b60a4da2961a to your computer and use it in GitHub Desktop.
Save Odomontois/63a3e20b1389b7ec9cb0b60a4da2961a to your computer and use it in GitHub Desktop.
Lazy vs Eager church encoded binary naturals
package sb.church.lz
import ChOption._
import ChPair._
import ChBool._
import ChEither._
import ChList._
import Lambda._
import cats.Eval
import cats.syntax.apply._
import Eval.{later, now}
trait ∀[f[_]] {def rec[α]: f[Eval[α]]}
trait ChurchModule {
type f[α]
abstract class T extends ∀[f] {
def $[α]: f[Eval[α]]
def rec[α] = {
Lambda.counter += 1
$[α]
}
}
}
object Lambda {
def id[a]: a => a = x => x
var counter = 0L
def count() = {
val c = counter
counter = 0
c
}
}
object ChBool extends ChurchModule {
type f[α] = α => α => α
type ChBool = ∀[f]
val True: Eval[ChBool] = now(new T {def $[α] = t => f => t})
val False: Eval[ChBool] = now(new T {def $[α] = t => f => f})
def or: Eval[ChBool] => Eval[ChBool] => Eval[ChBool] = x => y => x.flatMap(_.rec(True)(y))
def and: Eval[ChBool] => Eval[ChBool] => Eval[ChBool] = x => y => x.flatMap(_.rec(y)(False))
def toBool: Eval[ChBool] => Eval[Boolean] = _.flatMap(_.rec(now(true))(now(false)))
}
object ChOption {
private class mod[x] extends ChurchModule {
type f[α] = (Eval[x] => α) => α => α
val none = now(new T {def $[α] = _s => n => n})
def some: Eval[x] => Eval[ChOption[x]] = x => later(new T {def $[α] = s => _n => s(x)})
}
type ChOption[X] = ∀[mod[X]#f]
def none[x]: Eval[ChOption[x]] = new mod[x].none
def some[x]: Eval[x] => Eval[ChOption[x]] = new mod[x].some
def toOption[x]: Eval[ChOption[x]] => Eval[Option[x]] = _.flatMap(_.rec[Option[x]](x => x.map(Some(_)))(now(None)))
}
object ChList {
private class mod[x] extends ChurchModule {
type f[α] = (Eval[x] => α => α) => α => α
val nil = now(new T {def $[α] = c => n => n})
def cons: Eval[x] => Eval[ChList[x]] => Eval[ChList[x]] = x => xs => later(new T {def $[α] = c => n => c(x)(xs.flatMap(_.rec(c)(n)))})
}
type ChList[x] = ∀[mod[x]#f]
def nil[x]: Eval[ChList[x]] = new mod[x].nil
def cons[x]: Eval[x] => Eval[ChList[x]] => Eval[ChList[x]] = new mod[x].cons
def uncons[x]: Eval[ChList[x]] => Eval[ChOption[ChPair[x, ChList[x]]]] =
_.flatMap(_.rec[ChOption[ChPair[x, ChList[x]]]](h => re => some(pair(h)(re.flatMap(r => r.rec(u => u.flatMap(t => t.rec(cons)))(nil)))))(none))
def headOption[x]: ChList[x] => Eval[ChOption[x]] = xs => xs.rec[ChOption[x]](head => _ => some(head))(none)
def toList[x]: Eval[ChList[x]] => Eval[List[x]] = _.flatMap(_.rec[List[x]](head => tail => head.map2(tail)(_ :: _))(now(Nil)))
}
object ChPair {
private class mod[x, y] extends ChurchModule {
type f[α] = (Eval[x] => Eval[y] => α) => α
def pair: Eval[x] => Eval[y] => Eval[ChPair[x, y]] = x => y => later(new T {def $[α] = f => f(x)(y)})
}
type ChPair[x, y] = ∀[mod[x, y]#f]
def pair[x, y] = new mod[x, y].pair
def fst[x, y]: Eval[ChPair[x, y]] => Eval[x] = _.flatMap(_.rec(x => _ => x))
def snd[x, y]: Eval[ChPair[x, y]] => Eval[y] = _.flatMap(_.rec(_ => y => y))
def toTuple[x, y]: Eval[ChPair[x, y]] => Eval[(x, y)] = _.flatMap(_.rec(x => y => (x, y).tupled))
def mapFst[x, y, a]: Eval[x => a] => ChPair[x, y] => Eval[ChPair[a, y]] = f => _.rec(x => y => pair(f.ap(x))(y))
def mapSnd[x, y, b]: Eval[y => b] => ChPair[x, y] => Eval[ChPair[x, b]] = f => _.rec(x => y => pair(x)(f.ap(y)))
def mapBoth[x, y, a, b]: (Eval[x] => Eval[a]) => (Eval[y] => Eval[b]) => Eval[ChPair[x, y]] => Eval[ChPair[a, b]] = f => g => _.flatMap(_.rec(x => y => pair(f(x))(g(y))))
def product[a, b, c]: (Eval[a] => Eval[b]) => (Eval[a] => Eval[c]) => Eval[a] => Eval[ChPair[b, c]] = f => g => a => pair(f(a))(g(a))
}
object ChEither {
private class mod[x, y] extends ChurchModule {
type f[α] = (x => α) => (y => α) => α
def left: Eval[x] => Eval[ChEither[x, y]] = ex => ex.map(x => new T {def $[α] = f => g => f(x)})
def right: Eval[y] => Eval[ChEither[x, y]] = ey => ey.map(y => new T {def $[α] = f => g => g(y)})
}
type ChEither[x, y] = ∀[mod[x, y]#f]
def left[x, y]: Eval[x] => Eval[ChEither[x, y]] = new mod[x, y].left
def right[x, y]: Eval[y] => Eval[ChEither[x, y]] = new mod[x, y].right
def toEither[x, y]: Eval[ChEither[x, y]] => Eval[Either[x, y]] = _.flatMap(_.rec[Either[x, y]](x => later(Left(x)))(x => later(Right(x))))
}
object ChBin extends ChurchModule {
type f[α] = (α => α) => (α => α) => α => α
type ChBin = ∀[f]
val zero: Eval[ChBin] = now(new T {def $[α] = p0 => p1 => z => z})
def dig0: Eval[ChBin] => Eval[ChBin] = _.map(x => new T {def $[α] = d0 => d1 => z => d0(x.rec(d0)(d1)(z))})
def dig1: Eval[ChBin] => Eval[ChBin] = _.map(x => new T {def $[α] = d0 => d1 => z => d1(x.rec(d0)(d1)(z))})
val one = dig1(zero)
def toBigInt: Eval[ChBin] => Eval[BigInt] = _.flatMap(_.rec[BigInt](_.map(_ * 2))(_.map(_ * 2 + 1))(now(0)))
def fromBigInt: BigInt => Eval[ChBin] = _.toString(2).stripPrefix("0").foldLeft(zero) {
case (n, '0') => dig0(n)
case (n, '1') => dig1(n)
case _ => throw new NotImplementedError()
}
def succ: Eval[ChBin] => Eval[ChBin] = _.flatMap(
x => snd(x.rec[ChPair[ChBin, ChBin]](
p => pair(dig0(fst(p)))(dig1(fst(p))))(
p => pair(dig1(fst(p)))(dig0(snd(p))))(
pair(zero)(one))))
def consBin: Eval[ChBool] => Eval[ChBin] => Eval[ChBin] = b => x => b.flatMap(_.rec(dig1(x))(dig0(x)))
type ChBinUncons = ChOption[ChPair[ChBool, ChBin]]
private def unconsStep: Eval[ChBool] => Eval[ChBinUncons] => Eval[ChBinUncons] =
b => _.flatMap(_.rec(pr => some(pair(b)(pr.flatMap(_.rec(consBin)))))(some(pair(b)(zero))))
def unconsBin: Eval[ChBin] => Eval[ChBinUncons] = _.flatMap(_.rec[ChBinUncons](unconsStep(False))(unconsStep(True))(none))
def digits: Eval[ChBin] => Eval[ChList[ChBool]] = _.flatMap(_.rec(cons(False))(cons(True))(nil))
def unDigits: Eval[ChList[ChBool]] => Eval[ChBin] =
_.flatMap(_.rec[ChBin](b => l => b.flatMap(_.rec(now(dig1))(now(dig0))).value(l))(zero))
type SumIter = Eval[Eval[ChBin] => Eval[ChPair[ChBin, ChBin]]]
def sum: Eval[ChBin] => Eval[ChBin] => Eval[ChBin] = xe => ye =>
xe.flatMap(_.rec[Eval[ChBin] => Eval[ChPair[ChBin, ChBin]]](
(xf: SumIter) => later((y: Eval[ChBin]) => unconsBin(y).flatMap(_.rec(
_.flatMap(_.rec(
bit => yl => bit.flatMap(_.rec[ChPair[ChBin, ChBin]](
mapBoth(dig1)(dig0)(xf.flatMap(_ (yl)))
)(
product(dig0)(dig1)(fst(xf.flatMap(_ (yl))))
)))))(
product(dig0)(dig1)(fst(xf.flatMap(_ (zero))))
))))(
(xf: SumIter) => later((y: Eval[ChBin]) => unconsBin(y).flatMap(_.rec(
_.flatMap(_.rec(
bit => yl => bit.flatMap(_.rec[ChPair[ChBin, ChBin]](
product(dig0)(dig1)(snd(xf.flatMap(_ (yl))))
)(
mapBoth(dig1)(dig0)(xf.flatMap(_ (yl)))
)))))(
mapBoth(dig1)(dig0)(xf.flatMap(_ (zero)))
))))(
later(y => pair(y)(succ(y)))
)
).flatMap(f => fst(f(ye)))
}
package sb.church
import ChOption._
import ChPair._
import ChBool._
import ChList._
import Lambda._
import cats.Eval
import Eval.later
trait ∀[f[_]] {def rec[α]: f[α]}
trait ChurchModule {
type f[α]
abstract class T extends ∀[f] {
def $[α]: f[α]
def rec[α] = {
Lambda.counter += 1
$[α]
}
}
}
object Lambda {
def id[a]: a => a = x => x
var counter = 0L
def count() = {
val c = counter
counter = 0
c
}
}
object ChBool extends ChurchModule {
type f[α] = α => α => α
type ChBool = ∀[f]
val True: ChBool = new T {def $[α] = t => f => t}
val False: ChBool = new T {def $[α] = t => f => f}
def or: ChBool => ChBool => ChBool = x => y => x.rec(True)(y)
def and: ChBool => ChBool => ChBool = x => y => x.rec(y)(False)
def toBool: ChBool => Boolean = _.rec(true)(false)
}
object ChOption {
private class mod[x] extends ChurchModule {
type f[α] = (x => α) => α => α
val none = new T {def $[α] = _s => n => n}
def some: x => ChOption[x] = x => new T {def $[α] = s => _n => s(x)}
}
type ChOption[X] = ∀[mod[X]#f]
def none[X]: ChOption[X] = new mod[X].none
def some[X]: X => ChOption[X] = new mod[X].some
def toOption[X]: ChOption[X] => Option[X] = _.rec[Option[X]](Some(_))(None)
}
object ChList {
private class mod[x] extends ChurchModule {
type f[α] = (x => α => α) => α => α
val nil = new T {def $[α] = c => n => n}
def cons: x => ChList[x] => ChList[x] = x => xs => new T {def $[α] = c => n => c(x)(xs.rec(c)(n))}
}
type ChList[x] = ∀[mod[x]#f]
def nil[x]: ChList[x] = new mod[x].nil
def cons[x]: x => ChList[x] => ChList[x] = new mod[x].cons
def uncons[x]: ChList[x] => ChOption[ChPair[x, ChList[x]]] =
_.rec[ChOption[ChPair[x, ChList[x]]]](h => r => some(pair(h)(r.rec(_.rec(cons))(nil))))(none)
def headOption[x]: ChList[x] => ChOption[x] = xs => xs.rec[ChOption[x]](head => _ => some(head))(none)
def toList[x]: ChList[x] => List[x] = xs => xs.rec[List[x]](head => tail => head :: tail)(Nil)
}
object ChPair {
private class mod[x, y] extends ChurchModule {
type f[α] = (x => y => α) => α
def pair: x => y => ChPair[x, y] = x => y => new T {def $[α] = f => f(x)(y)}
}
type ChPair[x, y] = ∀[mod[x, y]#f]
def pair[x, y] = new mod[x, y].pair
def fst[x, y]: ChPair[x, y] => x = _.rec(x => _ => x)
def snd[x, y]: ChPair[x, y] => y = _.rec(_ => y => y)
def toTuple[x, y]: ChPair[x, y] => (x, y) = _.rec(x => y => (x, y))
def mapFst[x, y, a]: (x => a) => ChPair[x, y] => ChPair[a, y] = f => _.rec(x => y => pair(f(x))(y))
def mapSnd[x, y, b]: (y => b) => ChPair[x, y] => ChPair[x, b] = f => _.rec(x => y => pair(x)(f(y)))
def mapBoth[x, y, a, b]: (x => a) => (y => b) => ChPair[x, y] => ChPair[a, b] = f => g => _.rec(x => y => pair(f(x))(g(y)))
def product[a, b, c]: (a => b) => (a => c) => a => ChPair[b, c] = f => g => a => pair(f(a))(g(a))
}
object ChEither {
private class mod[x, y] extends ChurchModule {
type f[α] = (x => α) => (y => α) => α
def left: x => ChEither[x, y] = x => new T {def $[α] = f => g => f(x)}
def right: y => ChEither[x, y] = y => new T {def $[α] = f => g => g(y)}
}
type ChEither[x, y] = ∀[mod[x, y]#f]
def left[x, y]: x => ChEither[x, y] = new mod[x, y].left
def right[x, y]: y => ChEither[x, y] = new mod[x, y].right
def toEither[x, y]: ChEither[x, y] => Either[x, y] = _.rec[Either[x, y]](Left(_))(Right(_))
}
object ChBin extends ChurchModule {
type f[α] = (α => α) => (α => α) => α => α
type ChBin = ∀[f]
val zero: ChBin = new T {def $[α] = p0 => p1 => z => z}
def dig0: ChBin => ChBin = x => new T {def $[α] = d0 => d1 => z => d0(x.rec(d0)(d1)(z))}
def dig1: ChBin => ChBin = x => new T {def $[α] = d0 => d1 => z => d1(x.rec(d0)(d1)(z))}
val one = dig1(zero)
def toBigInt: ChBin => BigInt = _.rec[BigInt](n => n * 2)(n => n * 2 + 1)(0)
def fromBigInt: BigInt => ChBin = _.toString(2).stripPrefix("0").foldLeft(zero) {
case (n, '0') => dig0(n)
case (n, '1') => dig1(n)
case _ => throw new NotImplementedError()
}
def succ: ChBin => ChBin = x => snd(x.rec[ChPair[ChBin, ChBin]](
p => pair(dig0(fst(p)))(dig1(fst(p))))(
p => pair(dig1(fst(p)))(dig0(snd(p))))(
pair(zero)(one)))
def consBin: ChBool => ChBin => ChBin = b => x => b.rec(dig1(x))(dig0(x))
private def unconsStep: ChBool => ChBinUncons => ChBinUncons =
b => _.rec(pr => some(pair(b)(pr.rec(consBin))))(some(pair(b)(zero)))
type ChBinUncons = ChOption[ChPair[ChBool, ChBin]]
def unconsBin: ChBin => ChBinUncons = _.rec[ChBinUncons](unconsStep(False))(unconsStep(True))(none)
def digits: ChBin => ChList[ChBool] = _.rec(cons(False))(cons(True))(nil)
def unDigits: ChList[ChBool] => ChBin = _.rec(_.rec(dig1)(dig0))(zero)
def sum: ChBin => ChBin => ChBin = x =>
x.rec[ChBin => ChPair[ChBin, ChBin]](
xx => y => unconsBin(y).rec(_.rec(
bit => lower => bit.rec(
mapBoth(dig1)(dig0)(xx(lower)))(
product(dig0)(dig1)(fst(xx(lower))))))(
product(dig0)(dig1)(fst(xx(zero)))))(
xx => y => unconsBin(y).rec(_.rec(
bit => lower => bit.rec(
product(dig0)(dig1)(snd(xx(lower))))(
mapBoth(dig1)(dig0)(xx(lower)))))(
mapBoth(dig1)(dig0)(xx(zero))))(
y => pair(y)(succ(y))
) andThen fst
private def sumDigits: ChList[ChBool] => ChList[ChBool] => ChBin =
_.rec[ChList[ChBool] => ChPair[ChBin, ChBin]](
xDigit => recur => y => uncons(y).rec(_.rec(yDigit => yn =>
xDigit.rec(
yDigit.rec(
product(dig0)(dig1)(snd(recur(yn))))(
mapBoth(dig1)(dig0)(recur(yn))))(
yDigit.rec(
mapBoth(dig1)(dig0)(recur(yn)))(
product(dig0)(dig1)(fst(recur(yn)))))
))(
xDigit.rec(
mapBoth(dig1)(dig0)(recur(nil)))(
product(dig0)(dig1)(fst(recur(nil))))))(
unDigits andThen product(identity[ChBin])(succ)
) andThen fst
def sum2: ChBin => ChBin => ChBin = x => y => sumDigits(digits(x))(digits(y))
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment