Paul Tarau's Iso type in F# from Everything is Everything Paper

iso.fsx

(*
This is a port of the Haskell code from Paul Tarau's paper:

Everything Is Everything" Revisited: Shapeshifting Data Types with Isomorphisms and Hylomorphisms

Tarau, Paul. "" Everything Is Everything" Revisited: Shapeshifting Data Types with Isomorphisms and Hylomorphisms." Complex Systems 18.4 (2010): 475.

*)

type Iso<'A, 'B> = Iso of f: ('A -> 'B) * g: ('B -> 'A)

module Iso =
    let fnFrom (Iso(f, _)) = f
    let fnTo (Iso(_, g)) = g

    let compose: Iso<'A, 'B> -> Iso<'B, 'C> -> Iso<'A, 'C> =
        fun (Iso(f1, g1)) (Iso(f2, g2)) -> Iso(f1 >> f2, g2 >> g1)

    let itself = Iso(id, id)

    let invert (Iso(f, g)) = Iso(g, f)

    let borrow: Iso<'T, 'S> -> ('T -> 'T) -> ('S -> 'S) =
        fun (Iso(f, g)) h z -> f (h (g z))

    let borrow2 (Iso(f, g)) h x y = f (h (g x) (g y))

    let borrowN (Iso(f, g)) h xs = f (h (List.map g xs))

    let lend i = i |> invert |> borrow
    let lend2 x  = x |> invert |> borrow2
    let lendN x = x |> invert |> borrowN

    let fit : ('b -> 'c) -> Iso<'a, 'b> -> 'a -> 'c = 
        fun op iso x -> op ((fnFrom iso) x)

    let retrofit : ('a -> 'c) -> Iso<'a, 'b> -> 'b -> 'c = 
        fun op iso x -> op((fnTo iso) x)



module Encoders = 
    type Nat = bigint
    type Root = Nat list

    type Encoder<'a> = Iso<'a, Root>

    let withE : Encoder<'a> -> Encoder<'b> -> Iso<'a, 'b> = 
        fun this that -> Iso.compose this (Iso.invert that)

    let asE : Encoder<'a> -> Encoder<'b> -> 'b -> 'a =
        fun this that -> Iso.fnTo (withE this that)

    let funE : Encoder<Root> = Iso.itself

(*
set2fun is | is_set is =
    map pred (genericTake l ys) where
        ns = sort is
        l = genericLength ns
        next n | n >= 0 = succ n
        xs = (map next ns)
        ys = (zipWith (-) (xs++[0]) (0:xs))
    is_set ns = ns == nub ns

fun2set ns =
    map pred (tail (scanl (+) 0 (map next ns))) where
    next n | n >= 0 = succ n    

*)



module EncoderTests = 
    open Encoders
    open Iso




    //  Let's convert the above Haskell code to F# code
    let isSet (ns: Nat list) = ns |> List.distinct = ns
    let set2fun (is: Nat Set) =
        let ns = is |> Set.toList
        let l = List.length ns
        let next n = if n >= 0I then n + 1I else n
        let xs = List.map next ns
        let ys = List.zip (List.append xs [0I]) (0I::xs) |> List.map (fun (x, y) -> x - y)
        List.map (fun x -> x - 1I) (List.take l ys)


    // let set2fun (is: Nat list) =
    //     let ns = List.sort is
    //     let l = List.length ns
    //     let next n = if n >= 0I then n + 1I else n
    //     let xs = List.map next ns
    //     let ys = List.zip (List.append xs [0I]) (0I::xs) |> List.map (fun (x, y) -> x - y)
    //     List.map (fun x -> x - 1I) (List.take l ys)

    let fun2set (ns: Nat list) =
        let next n = if n >= 0I then n + 1I else n
        let xs = List.map next ns
        List.map (fun x -> x - 1I) (List.tail (List.scan (+) 0I xs)) |> Set.ofList

    let setE  = Iso(set2fun, fun2set)

    let result1 = asE setE funE [0; 1; 0; 0; 4]
    // [0; 2; 3; 4; 9]
    let result2 = asE funE setE result1
    // [0; 1; 0; 0; 4]
    
    (*
    nat_set = Iso nat2set set2nat
    nat2set n | n >= 0 = nat2exps n 0 where
        nat2exps 0 _ = []
        nat2exps n x =
            if (even n) then xs else (x:xs) where
            xs = nat2exps (n ‘div‘ 2) (succ x)
    
    set2nat ns | is_set ns = sum (map (2^) ns)    
    
    *)

    let nat2set (n: Nat): Set<Nat> =
        let rec nat2exps n x =
            if n = 0I then []
            else
                let xs = nat2exps (n / 2I) (x + 1I)
                if n % 2I = 0I then xs else x::xs
        (if n >= 0I then nat2exps n 0I else []) |> Set.ofList

    let set2nat (ns: Nat Set): Nat =
        Seq.sumBy (fun n -> 2I ** int(n)) ns
    
    let nat_set = Iso(nat2set, set2nat)

    let nat = compose nat_set setE

    let succ x = x + 1I
    let pred x = x - 1I

    module FunExamples =

        let ex1 = asE funE nat 2008I
        //  [3; 0; 1; 0; 0; 0; 0]
        let ex2 = asE setE nat 2008I
        //  set [3; 4; 6; 7; 8; 9; 10]
        let ex3 = asE nat setE ex2
        //  2008
        let ex4 = lend nat (List.rev) 0I
        //  1135
        // let ex5 = lend2 nat_set (List.rev) 2008
        let ex6 = borrow nat_set (fun n -> n + 1I) (set [1I;2I;3I])
        //  set [0; 1; 2; 3]
        let ex7 = asE setE nat 42I
        //  set [1; 3; 5]
        let ex8 = fit (List.length) nat 42I
        //  3
        let ex9 = retrofit succ nat_set (set [1I; 3I; 5I])
        //  43


    module GapExamples = 
        //  as set fun [0,1,2,3]
        let ex1 = asE setE funE [0I; 1I; 2I; 3I]
        //  set [0; 2; 5; 9]

        // as set fun (as set fun [0,1,2,3])
        let ex2 = asE setE funE (ex1 |> Set.toList)
        // set [0; 3; 9; 19]

        // as set fun (as set fun (as set fun [0,1,2,3]))
        let ex3 = asE setE funE (ex2 |> Set.toList)
        // set [0; 4; 14; 34]

    (*
    The unranking operation is seen here as an instance of a generic
    anamorphism mechanism (an unfold operation), while the ranking operation is seen as an instance of the corresponding catamorphism (a
    fold operation) [10, 11]. Together they form a mixed transformation
    called hylomorphism. We use such hylomorphisms to lift isomorphisms between lists and natural numbers to isomorphisms between a
    derived “self-similar” tree data type and natural numbers. In particular, we will derive Ackermann’s encoding from hereditarily finite sets
    to natural numbers.

    The data type representing hereditarily finite structures will be a
    generic multiway tree with a single leaf type [].

    data T = H Ts deriving (Eq,Ord,Read,Show)
    type Ts = [T]

    The two sides of our hylomorphism are parameterized by two
    transformations f and g forming an isomorphism Iso f g.

    unrank :: (a -> [a]) -> a -> T
    unranks :: (a -> [a]) -> [a] -> Ts
    unrank f n = H (unranks f (f n))
    unranks f ns = map (unrank f) ns
    rank :: ([b] -> b) -> T -> b
    ranks :: ([b] -> b) -> Ts -> [b]
    rank g (H ts) = g (ranks g ts)
    ranks g ts = map (rank g) ts

    Both combinators can be seen as a form of “structured recursion”
that propagate a simpler operation guided by the structure of the data
type. For instance, the size of a tree of type T is obtained as:

    tsize = rank (lxs -> 1 + (sum xs))
    *)

    type T = H of Ts
    and Ts = T Set


    let rec unrank =
        fun f n -> H (f n |> unranks f)
    and unranks =
        fun f ns -> ns |> Set.map (unrank f)

    let rec rank =
        fun g (H ts) -> g (ranks g ts)
    and ranks =
        fun g ts -> ts |> Set.map (rank g)


    module Set = 
        let sum (xs: bigint Set) = xs |> Set.toSeq |> Seq.sum

    let tsize = rank (fun lxs -> 1I + (Set.sum lxs))

    (*
    We can now combine an anamorphism+catamorphism pair into an
    isomorphism hylo defined with rank and unrank on the corresponding hereditarily finite data types.

    hylo :: Iso b [b] -> Iso T b
    hylo (Iso f g) = Iso (rank g) (unrank f)

    hylos :: Iso b [b] -> Iso Ts [b]
    hylos (Iso f g) = Iso (ranks g) (unranks f)
    *)

    let hylo (Iso(f, g)) = Iso(rank g, unrank f)
    let hylos (Iso(f, g)) = Iso(ranks g, unranks f)

    (*
    4.1.1 Hereditarily Finite Sets

    Hereditarily finite sets will be represented as an encoder for the tree
    type T.

        hfs :: Encoder T
        hfs = compose (hylo nat_set) nat

    The hfs encoder can now borrow operations from sets or natural numbers as follows.

        hfs_union = borrow2 (with set hfs) union
        hfs_succ = borrow (with nat hfs) succ
        hfs_pred = borrow (with nat hfs) pred

        *ISO> hfs_succ (H [])
        H [H []]
        *ISO> hfs_union (H [H []] ) (H [])
        H [H []]

    Otherwise, hylomorphism induced isomorphisms work as usual with our embedded transformation language.

        *ISO> as hfs nat 42
        H [H [H []],H [H [],H [H []]],H [H [],H [H [H []]]]]    
    *)

    

    let hfs = compose (hylo nat_set) nat

    let hfs_union = borrow2 (withE setE hfs) Set.union
    let hfs_succ = borrow (withE nat hfs) succ
    let hfs_pred = borrow (withE nat hfs) pred

    // Ackmann's encoding from hereditarily finite sets to natural numbers

    let ackermann = asE nat hfs
    let inverse_ackermann = asE hfs nat

    module HfsExamples = 
        let test50 f = seq { 0I..50I } |> Seq.map (f >> sprintf "%A") |> Dump
    
        let ex1 = (H (set [])) |> hfs_succ |> printfn "%A"
        // H [H []]
        let ex2 = hfs_union (H (set [H (set [])])) (H (set []))
        // H [H []]
        let ex3 = asE hfs nat // |> test50
        // H [H [H []], H [H [], H [H []]], H [H [], H [H [H []]]]

        let ex4 = inverse_ackermann // |> test50

    (*

    4.1.2 Hereditarily Finite Functions

    The same tree data type can host a hylomorphism derived from finite functions instead of finite sets.
    
        hff :: Encoder T
        hff = compose (hylo nat) nat

    The hff encoder can be seen as another free algorithm, providing
    data compression/succinct representation for hereditarily finite sets.
    Note, for instance, the significantly smaller tree size in the following.
    
        *ISO> as hff nat 42
        H [H [H []],H [H []],H [H []]]

    As the cognoscenti might observe, this is explained by the fact that
    hff provides higher information density than hfs by incorporating order information that matters in the case of a sequence, and is ignored
    in the case of a set.

    *)    


        
        // compose (hylo nat) nat