Skip to content

Instantly share code, notes, and snippets.

@ClarkeRemy

ClarkeRemy/recursion_schemes.sml

Last active August 16, 2024 12:58
Show Gist options
  • Save ClarkeRemy/0fcf2306db1f69f9ec048ac8824de388 to your computer and use it in GitHub Desktop.
Save ClarkeRemy/0fcf2306db1f69f9ec048ac8824de388 to your computer and use it in GitHub Desktop.
Download ZIP
Recursion Schemes SML extended
Raw
recursion_schemes.sml
signature FUNCTOR = sig
type 'a F
val fmap : ('a -> 'b) -> 'a F -> 'b F (* F is a category theory functor *)
end
signature FUNCTOR_FIX = sig
include FUNCTOR
type fix (* The Fixpoint type *)
val prj : fix -> fix F (* Recursive *)
val inj : fix F -> fix (* Corecursive *)
end
signature REC_SCHEME = sig
include FUNCTOR_FIX
(* Catamorphism : Consuming inductive data *)
val cata : ('ret F -> 'ret) -> fix -> 'ret
(* Anamorphism : Generating coinductive data *)
val ana : ('seed -> 'seed F) -> 'seed -> fix
(* Hylomorphism : generating followed by consuming ; (Edward Kmett) builds up and tears down a virtual structure *)
val hylo : ('ret F -> 'ret) -> ('seed -> 'seed F) -> 'seed -> 'ret
(* Accumulation : Recursion with an accumulating parameter *)
val accumulation : (fix F -> 'acc -> (fix * 'acc) F)
-> ('ret F -> 'acc -> 'ret)
-> fix -> 'acc -> 'ret
(* Mutumorphism : Mutual recursion on inductive data*)
val mutu : (('a * 'b) F -> 'a)
-> (('a * 'b) F -> 'b)
-> (fix -> 'a) * (fix -> 'b)
(* Paramorphism : Primitive recursion, i.e. access to original input *)
val para : ((fix * 'ret) F -> 'ret) -> fix -> 'ret
(* Apomorphism : Early termination of generation *)
val apo : ('seed -> ((fix, 'seed) Either.either) F) -> 'seed -> fix
(* Zygomorphism : Recursion with auxiliary information *)
val zygo : (('ret * 'aux) F -> 'ret)
-> ('aux F -> 'aux)
-> fix -> 'ret
datatype 'a free = RET of 'a
| OP of 'a free F
datatype 'a cofree = COFREE of 'a * ('a cofree) F
val extract : 'a cofree -> 'a
(* Histomorphism : Access to all sub-results *)
val histo : (('ret cofree F) -> 'ret) -> fix -> 'ret
(* Dynamorphism : Dynamic Programming *)
val dyna : ('ret cofree F -> 'ret)
-> ('seed -> 'seed F)
-> 'seed -> 'ret
(* Futumorphishm : Generating multiple layers *)
val futu : ('seed -> 'seed free F) -> 'seed -> fix
(* Chronomorphism : time traveling Hylomorphism *)
val chrono : ('ret cofree F -> 'ret)
-> ('seed -> 'seed free F)
-> 'seed -> 'ret
end
functor Schemes(structure T : FUNCTOR_FIX) : REC_SCHEME = struct
fun id x = x
fun case_either x y = Either.proj o Either.map (x, y)
fun uncurry f (x,y) = f x y
fun || (f,x) = f x
infixr 0 ||
structure T = T
open T
fun cata alg x : 'ret = alg o fmap (cata alg ) o prj || x
fun ana coalg (x : 'seed) = inj o fmap (ana coalg) o coalg || x
fun hylo alg coalg (x : 'seed) : 'ret = alg o fmap (hylo alg coalg) o coalg || x
fun accumulation st alg x (acc : 'acc) : 'ret = alg ((fmap || uncurry || accumulation st alg) || st (prj x) acc) acc
fun mutu alg1 alg2 =
let fun alg x = (alg1 x, alg2 x)
in (#1 o cata alg, #2 o cata alg)
end
fun para alg x : 'ret = alg o fmap (fn y => (y , para alg y)) o prj || x
fun apo coalg (x : 'seed) = inj o fmap (case_either id || apo coalg ) o coalg || x
fun zygo (alg1 : ('ret * 'aux) F -> 'ret) alg2 = #1 || mutu alg1 || alg2 o fmap #2
datatype 'a free = RET of 'a
| OP of 'a free F
datatype 'a cofree = COFREE of 'a * ('a cofree) F
fun extract (COFREE (x, _)) = x
fun cofree' alg = fn x => COFREE (alg x, x)
fun free' coalg = fn RET a => coalg a
| OP k => k
fun histo alg : fix -> 'ret = extract o cata (cofree' alg)
fun dyna alg coalg : 'seed -> 'ret = extract o hylo (cofree' alg) coalg
fun futu coalg : 'seed -> fix = ana (free' coalg) o RET
fun chrono alg coalg : 'seed -> 'ret = extract o hylo (cofree' alg) (free' coalg) o RET
end
signature BIFUNCTOR = sig
type ('a, 'b) BF
(* these can be generated later *)
(* first f = bimap f id *)
(* second f = bimap id f *)
(* bimap f g = first f o second g *)
val bimap : ('a -> 'b) -> ('c -> 'd) -> ('a, 'c) BF -> ('b, 'd) BF
end
signature BIFUNCTOR_FIX = sig
type f
type g
structure F : BIFUNCTOR
structure G : BIFUNCTOR
(* We don't need these ... yet *)
(*
val prj_f : f -> (f, g) F.BF
val prj_g : g -> (f, g) G.BF
*)
val inj_f : (f, g) F.BF -> f
val inj_g : (f, g) G.BF -> g
end
functor Comutumorphism(T : BIFUNCTOR_FIX) :
sig
(* f and g represent mutually recursive datatypes *)
type f
type g
(* F and G are bifunctors that need to be generic on either "recursive slot" *)
structure F : BIFUNCTOR
structure G : BIFUNCTOR
(* Dual of Mutumorphism / Comutumorphism: Generating mutually defined coinductive data *)
val comutu : ('seed -> ('seed, 'seed) F.BF)
-> ('seed -> ('seed, 'seed) G.BF)
-> 'seed -> f * g
end = struct
type f = T.f
type g = T.g
structure F = T.F
structure G = T.G
fun comutu c1 c2 (s : 'seed) =
let fun x z = (T.inj_f o F.bimap x y o c1) z
and y z = (T.inj_g o G.bimap x y o c2) z
in (x s, y s) end
end
signature APPLICATIVE = sig
include FUNCTOR
val pure : 'a -> 'a F
val apply : ('a -> 'b) F -> 'a F -> 'b F
end
signature MONAD = sig
include APPLICATIVE
val join : 'a F F -> 'a F
end
functor MonadicSchemes(
structure T : FUNCTOR_FIX
structure M : MONAD
) : sig
include REC_SCHEME
structure M : MONAD
(* Monadic catamorphism : Recursion causing computational effects *)
val m_cata : ('ret M.F T.F -> 'ret T.F M.F)
-> ('ret T.F -> 'ret M.F)
-> T.fix -> 'ret M.F
end = struct
structure S = Schemes(structure T = T)
open S
structure M = M
fun m_cata seq (alg : 'ret T.F -> 'ret M.F) = cata (M.join o M.fmap alg o seq)
end
signature HFUNCTOR = sig
type 'a I
type 'a O
type 'a HF
(*
Standard ML does not have higher kinded types,
so we encode a higher kinded type by contraining `hfmap` to work on two concrete type constructors.
However doing so makes `hfmap` only work in one direction.
`hfmap'` should have the same behavior as `hfmap`, but just have the opposite type constraint
what should be needed ...
val hfmap : ('a I -> 'b O) -> 'a I HF -> 'b O HF
val hfmap' : ('a O -> 'b I) -> 'a O HF -> 'b I HF
*)
(* but instead we will use this, it is more general, and simplifies the code. *)
val hfmap : ('a -> 'b) -> 'a HF -> 'b HF
end
functor HFunctor(
structure T : sig
type 'a I
type 'a O
structure HF : FUNCTOR
end) : HFUNCTOR = struct
open T
type 'a HF = 'a HF.F
val hfmap = HF.fmap
end
signature HFUNCTOR_FIX = sig
include HFUNCTOR
type fix
val hprj : fix -> fix HF
val hinj : fix HF -> fix
end
signature HFUNCTOR_SCHEMES = sig
include HFUNCTOR_FIX
type 'ret ialg = 'ret O HF -> 'ret O
type 'seed icoalg = 'seed I -> 'seed I HF
val icata : 'ret ialg -> fix -> 'ret O
val iana : 'seed icoalg -> 'seed I -> fix
val ihylo : 'ret ialg -> 'seed icoalg -> 'seed I -> 'ret O
end
functor HFunctorSchemes (
structure T : HFUNCTOR_FIX
) : HFUNCTOR_SCHEMES = struct
open T
type 'ret ialg = 'ret O HF -> 'ret O
type 'seed icoalg = 'seed I -> 'seed I HF
fun icata alg x : 'ret O = (alg o hfmap ( icata alg ) o hprj ) x
fun iana coalg (x : 'seed I) = (hinj o hfmap ( iana coalg ) o coalg ) x
fun ihylo alg coalg (x : 'seed I) : 'ret O = (alg o hfmap ( ihylo alg coalg ) o coalg ) x
end
(* what have we learned from implementing HFunctorSchemes? ... it's just Schemes, with extra type constraints *)
structure Z = struct
datatype tree = NODE of int * tree list
datatype 'a fTree = FNODE of int * 'a list
structure TreeSchemes = Schemes(structure T = struct
type fix = tree
type 'a F = 'a fTree
fun fmap f (FNODE (n, l)) = FNODE (n, List.map f l)
val prj = fn NODE (n, l) => FNODE (n, l)
val inj = fn FNODE (n, l) => NODE (n, l)
end)
datatype 'a fTreeZip = FNIL | FCONS of (tree * tree) * 'a
structure TreeZipSchemes = Schemes(
structure T = struct
type fix = (tree * tree) list
type 'a F = 'a fTreeZip
fun fmap _ FNIL = FNIL
| fmap f (FCONS (x, l)) = FCONS (x, f l)
val prj = fn [] => FNIL
| (x :: xs) => FCONS (x, xs)
val inj = fn FNIL => []
| FCONS (x, xs) => x::xs
end)
val _ = let
fun node n l = NODE (n, l)
fun fnode n l = FNODE(n, l)
val show_tree = TreeSchemes.cata
(fn FNODE (n, l) => "NODE(" ^ Int.toString n ^ ", [" ^ List.foldr (op ^) "" l ^ "]) ")
fun insert_left_most new = TreeSchemes.para
(fn FNODE (i, []) => node i [node new []]
| FNODE (i, ((_, recur) :: tts)) =>
let
val unzip = TreeZipSchemes.cata (fn FNIL => ([],[])
| FCONS ((l,r), (ls, rs)) => (l::ls, r::rs))
in
node i (recur :: (#1 o unzip) tts)
end
)
val myTree = node 0 [
node 1 [],
node 2 [],
node 3 [
node 31 [
node 311 [
node 3111 [],
node 3112 []
]]]]
in
(print o show_tree o insert_left_most 999)
myTree
end
end
val _ = OS.Process.exit OS.Process.success
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment