Placing External Iterators in Category Theory

Disclaimer: I may have no idea what I'm talking about!

Excuse the Pikelet syntax

The problem

[0..10] 
  |> flat-map (\x => [x, x * x])
  |> map show
  |> list-to-set

This looks pretty, but it results in lots of intermediate copies. We would require fusion optimizations (via {-# RULES ... #-} in Haskell) to get rid of these.

To the best of my knowledge most category theory inspired libraries (that rely on our friends, Functor, Applicative, Monad, Foldable, and Traversable) in strictly evaluated languages like Scala, Purescript, and Idris seem to ignore this reality. This is untenable for a 'systems' language.

Why we want a basis in Category Theory

• composition
• code reuse
• lawful interfaces

TODO

Why fusion is icky

Fusion is not easily partially evaluated in the programmers head. It is brittle and easy to break by mistake. We want to be able to lift ourselves into some context where each operation is guaranteed to be fused correctly.

Hypothesis:

Optimizations that are 'easy to reason about' seem to be some sort of 'partial evaluation'.

Some examples:

• monomorphization
• constant folding
• inlining

External iteratoration

One well-known way to manually 'fuse' chained iterations is to use 'external iterators':

iter [0..10]                           -- VecIter Int
  |> flat-map (\x => iter [x, x * x])  -- FlatMap (VecIter Int) (VecIter Int)
  |> map show                          -- Map String (FlatMap (VecIter Int) (VecIter Int))
  |> collect (Set String)              -- Set String

Note that the iteration is only triggered on the collect. Each new operation wraps the previous iterator adaptor in a new type. The adaptors are unboxed and allocated on the stack, making them quite easy for the compiler to inline and optimize away to a fused, low level implementation.

The problem

Iterator (it : Type) = Record {
    Item : Type;
    next : {m : Type -> Type} {{M : Monad}} -> it -> m (Option Item);

    map : {b : Type} -> it -> (I.Item -> b) -> MapIter b it;
    flat-map : {it' : Type} {{I' : Iterator it'}} -> it -> (I.Item -> it') -> FlatMapIter it it';
};

Bluuurgh! The specialised map function looks NOTHING like Functor's map function!

Functor (Map : Type -> Type) = Record {
    map : {a b : Type} -> (a -> b) -> Map a -> Map b;
};

We have some possibilities here:

1. map should be called something else
   • Something from foldables/traversables?
   • Something lensy?
     • Profunctor Optics: Modular Data Accessors
     • Don’t Fear the Profunctor Optics
     • Profunctor Optics: The Categorical View
2. we could figure out if Functor could be made more general, to allow us to define functor instances for ListIter a, HashMapIter k v, MyFuture a, etc.

A category of iterator adapters

Investigating Option 2 from above, note that Haskell's Functor typeclass is specialised to the category of Haskell types and functions. We could instead use a more general notion of categories however:

Category = Record {
    Object : Type;
    Arrow : Object -> Object -> Type;
    id : {a : Object} -> Arrow a a;
    seq : {a b c : Object} -> Arrow a b -> Arrow b c -> Arrow a c;
};

Functor = Record {
    Source : Category;
    Target : Category;
    Map : Source.Object -> Target.Object;
    map : {a b : Source.Object} -> Source.Arrow a b -> Target.Arrow (Map a) (Map b);
};

Could we define a new Category instance for the iterator adapters? This might allow Target.Arrow to wrap the resulting type in another iterator adaptor. I don't know though, it might not be lawful!

-- this feels wrong - kind of stabbing in the dark though
IteratorAdaptor-Category (adaptor : (it : Type) {{Iterator it}} -> Type) = record {
    Object = Type;
    Arrow iter = adaptor iter;
    id iter = IdIter iter;
    seq = ?todo;
};

TODO

What about monads, foldables, and traversables?

TODO

Can this work for other families of adapters?

Eg. Futures, Parallel iterators, etc.

TODO

How to teach this from scratch

TODO

References

• http://www.cs.ox.ac.uk/bruno.oliveira/iterator.pdf
• https://www.fpcomplete.com/blog/2017/07/iterators-streams-rust-haskell
• https://www.reddit.com/r/rust/comments/6mf2sz/iterators_and_streams_in_rust_and_haskell/