Example of fold/unfold operations...

rectypes.eff.ml

(* type-level recursion with fold/unfold *)

(* $ eff --effects -l rectypes.eff *)

(* there's an unique isomorphism between fold and unfold such that:

    fold :: ...1 Unfix (...2 Fix (func) ...3) ...4 <=> ...1 Fix (func) ...4 :: unfold
      where func = \fix -> ...2 fix ...3

  so, conceptually:

    let func = \fix -> Type in
    fold   :: Unfix (Type[ fix := Fix (func) ]) -> Fix (func)
    unfold :: Fix (func) -> Unfix (func (Fix (func))) = Unfix (Type[ fix := Fix (func) ])
      where Type = 0 | 1 | Type + Type | Type * Type
                 | Unfix Type
                 | Forall (type :: Type), param type  :: Type
                 | Fix (self :: Type),    unroll self :: Type

*)

type label = Zero
           | One
           | Sum   of label * label
           | Prod  of label * label
           | Fix   of (label -> label)
           | Param of (label -> label)
           | Unfix of label

let ( |+| ) left right   = Sum (left, right)
let ( |*| ) first second = Prod (first, second)

let boolean = Sum (One, One)
let natural = Fix (fun self -> One |+| self)
let bintree = Param (fun any -> Fix (fun self -> One |+| (self |*| any |*| self)))

let instance label = function
    | Param param -> param label
    | default     -> default

type wire = Unit
          | Left  of wire
          | Right of wire
          | Pair  of wire * wire

let rec unroll = function
    | Fix fix              -> Unfix (fix (Fix fix))
    | Sum (left, right)    -> Sum (unroll left, unroll right)
    | Prod (first, second) -> Prod (unroll first, unroll second)
    | Unfix unfix          -> Unfix (unroll unfix)
    | default              -> default

let roll label =
    let replace = function
        | (that, true)  -> that
        | (that, false) -> Unfix that
    in
    let choosewith constr (x, a) (y, b) = match (a, b) with
        | (true, false)  -> (x, true)
        | (false, true)  -> (y, true)
        | (false, false) -> (constr x y, false)
        | (_, _)         -> (x, true) (* the left side matters most than the right *)
    in
    let rec loop = function
        | Fix fix              -> (Fix fix, true)
        | Unfix unfix          -> (replace (loop unfix), false)
        | Sum (left, right)    -> choosewith ( |+| ) (loop left) (loop right)
        | Prod (first, second) -> choosewith ( |*| ) (loop first) (loop second)
        | default              -> (default, false)
    in
    match loop label with (first, _) -> first

type recursive = effect
    operation fold   : unit -> label
    operation unfold : unit -> label
end

(* stateful resource for recursive types, like an object
   every operation takes an argument and the old state,
   then the result is composed of the result of operation
   with the new state for the current resource            *)
let recursive label = new recursive @ label with
    operation unfold ( ) @ label -> let result = unroll label in (result (* output *), result (* new state *))
    operation fold   ( ) @ label -> let result = roll   label in (result (* output *), result (* new state *))
end

let nat  = recursive natural
let tree = recursive (instance boolean bintree)

(* end of code *)

On interpreter, try:

nat # unfold ( );; (* n times *)
nat # fold ( );; (* m times *)

tree # unfold ( );; (* x times *)
tree # fold ( );; (* y times *)