Skip to content

Instantly share code, notes, and snippets.

@koropicot
Last active December 21, 2015 06:39
Show Gist options
  • Save koropicot/6265729 to your computer and use it in GitHub Desktop.
Save koropicot/6265729 to your computer and use it in GitHub Desktop.
FunctorからF-initial algebraを書ける何かを書こうとしたけれどつらみがたまった。 NYSL Version 0.9982
trait Functor[F[_]]
{
def lift[A,B](f: A=>B): F[A]=>F[B]
}
//定数関手と恒等関手
class Const[A,+B](val value: A)
class Ident[A](val value: A)
object Functor{
implicit def ConstFunctor[X] = new Functor[({type L[Y]=Const[X,Y]})#L] {
def lift[A,B](f: A=>B) = Fa => new Const(Fa.value)
}
implicit def IdentFunctor[X] = new Functor[Ident]{
def lift[A,B](f: A=>B) = Fa => new Ident(f(Fa.value))
}
}
object Initial
{
//コンストラクタ
def c1[Self,F1[_],F2[_]](v1: F1[Self])
(implicit fc1: Functor[F1], fc2: Functor[F2], ev1: Initial[F1,F2]=>Self, ev2: Self=>Initial[F1,F2]): Self
= new Initial(Left(fc1.lift(ev2)(v1)),fc1,fc2)
def c2[Self,F1[_],F2[_]](v2: F2[Self])
(implicit fc1: Functor[F1], fc2: Functor[F2], ev1: Initial[F1,F2]=>Self, ev2: Self=>Initial[F1,F2]): Self
= new Initial(Right(fc2.lift(ev2)(v2)),fc1,fc2)
}
//Catamorphismが関手から定義される
class Initial[F1[_],F2[_]] private[Initial](value: Either[F1[Initial[F1,F2]],F2[Initial[F1,F2]]], fc1: Functor[F1], fc2: Functor[F2])
{
def cata[T](f1: F1[T]=>T,f2: F2[T]=>T): T = value match {
case Left(v1: F1[Initial[F1,F2]]) => f1(fc1.lift((s:Initial[F1,F2])=>s.cata[T](f1,f2))(v1))
case Right(v2: F2[Initial[F1,F2]]) => f2(fc2.lift((s:Initial[F1,F2])=>s.cata[T](f1, f2))(v2))
}
}
object Nat{
//Nat = Initial2.Initial[Nat,({type L[X]=Const[Unit,X]})#L,Ident]であることの証明
implicit def initialToNat(initial: Initial[({type L[X]=Const[Unit,X]})#L,Ident]): Nat = {
new Nat(initial)
}
implicit def natToInitial(nat: Nat): Initial[({type L[X]=Const[Unit,X]})#L,Ident] = {
nat.initial
}
//コンストラクタを委譲
def Zero: Nat = Initial.c1[Nat,({type L[X]=Const[Unit,X]})#L,Ident](new Const[Unit,Nat](()))
def Succ(n: Nat) = Initial.c2[Nat,({type L[X]=Const[Unit,X]})#L,Ident](new Ident[Nat](n.initial))
}
class Nat private[Nat](val initial: Initial[({type L[X]=Const[Unit,X]})#L,Ident]){
//Catamorphismを委譲
def cata[T](zero: T,succ: T=>T): T = initial.cata[T](_=>zero,identF=>succ(identF.value))
}
object Main{
def main(args: Array[String]): Unit = {
val zero: Nat = Nat.Zero
val _1 = Nat.Succ(zero)
//これがやりたかった
val plusNat = (a: Nat) => (b: Nat) => a.cata(b,Nat.Succ)
val _10 = intToNat(10)
val _32 = intToNat(32)
val _42 = plusNat(_10)(_32)
print(natToInt(_42))
}
def intToNat(i: Int): Nat = {
if(i == 0)
Nat.Zero
else
Nat.Succ(intToNat(i-1))
}
def natToInt(n: Nat): Int = {
n.cata[Int](0,i=>i+1)
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment