Cascade: Playing with reified categorical composition

Cascades are collections of composable functions (e.g. a -> b, b -> c, ... , y -> z) where the intermediate types are stored in a type level list (e.g. Cascade [a,b,c,...,y,z]).

For example, consider these Cascades:

fc :: Cascade '[String, Int, Double, Double]
fc =  read          :>>>
      fromIntegral  :>>>
      (1/)          :>>> Done

gc :: Cascade '[String, Int, Double, Double]
gc =  length        :>>>
      (2^)          :>>>
      negate        :>>> Done

We can convert a cascade into a function easily enough:

λ :m +Cascade.Examples Cascade.Operators
λ fc # "5"
0.2
λ gc # "20"
-4.0

But that's not very inspiring. The real question, as Christian Conkle put it, is "what does such a collection give you over function composition?"

Because none of the type information has been lost, we can still extract each of the functions that went into the Cascade using simple pattern matching. This opens the door to replacing parts of a cascade, or indexing into the cascade with type-level naturals.

It also lets us do something silly like mix and match two different cascades:

λ zigzag fc gc # "3" -- read >>> (2^) >>> (1/)
0.125
λ zigzag gc fc # "123456789" -- length >>> fromIntegral >>> negate
-9.0

More seriously, we can record the intermediate results of each Cascade using a Product type as output:

λ :m +Cascade.Product
λ record fc # "5" *: None
0.2 *: 5.0 *: 5 *: "5" *: None
λ record gc # "5" *: None
-2.0 *: 2.0 *: 1 *: "5" *: None

Or I can resume the computation at some later point rather that the first function in the Cascade using a Sum type as input:

λ :m +Cascade.Sum
λ resume fc # (there.there.here) 0.2
here 5.0
λ resume gc # (there.here) 0
here (-1.0)

Or we could do both:

λ resume (record fc) # (there.here) (17 *: "foo" *: None)
here (5.8823529411764705e-2 *: 17.0 *: 17 *: "foo" *: None)
λ record (resume fc) # (there . there $ here 0.25) *: None
here 4.0 *: here 0.25 *: (there.here $ 0.25) *: (there.there.here $ 0.25) *: None

But what's nice is that this generalizes nicely to categorical composition, so we can do the same with any category, including the Kleisli and Cokleisli categories for Monads and Comonads, respectively:

-- some example monadic cascades
mc, nc :: CascadeM IO '[ String, (), String, String, () ]
mc =  putStr                  >=>:
      const getLine           >=>:
      return . map toUpper    >=>:
      putStrLn                >=>: Done
nc =  setEnv "foo"            >=>: 
      const (return "foo")    >=>:
      getEnv                  >=>:
      print . length          >=>: Done

-- some example comonadic cascades
wc, vc :: CascadeW ((,) Char) '[ Int, Char, Int, String ]
wc =  fst                       =>=:
      fromEnum . snd            =>=:
      uncurry (flip replicate)  =>=: Done
vc =  toEnum . snd              =>=:
      const 5                   =>=:
      show                      =>=: Done

Flipping back to ghci:

λ mc #~ "? "
? i like cheese
I LIKE CHEESE
λ nc #~ "? "
2
λ wc ~# ('.', 5)
".............................................."
λ vc ~# ('x', 9)
"('x',5)"
λ zigzag mc nc #~ "hi!"
hi!3
λ zigzag nc mc #~ "hello."
USER
rampion
λ zigzag wc vc ~# ('.', 3)
"....."
λ zigzag vc wc ~# ('a', 9)
"('a',9)"

resume works on both comonads and monads:

λ resumeM nc #~ (there.there.here) "USER"
7
here ()
λ toEither $ resumeW vc # (There . There . Here) ('c',9)
Left ('c',"('c',9)")

record works on comonads, but I've been having some issues getting it to work the way I want on monads (see Cascade.Product.hs for more).

So, instead of continue to wrestle the type system, for now, I just implemented a debugger that uses Cascades, so in addition running a monadic Cascade you can debug it.

-- run the debugger for the mc cascade all the way to the end
rundmc :: IO (DebuggerM IO '[String, String, (), [Char]] () '[])
rundmc = debugM >>> use "walk this way\n> " >=> step >=> step >=> step $ mc

Dropping into ghci:

λ d <- rundmc
walk this way
> talk this way
TALK THIS WAY

We can see the current state of the debugger:

λ d
End   { given = "TALK THIS WAY", returned = () }

the full stack trace

λ printHistory d
End   { given = "TALK THIS WAY", returned = () }
Break { given = "talk this way", returned = "TALK THIS WAY" }
Break { given = (), returned = "talk this way" }
Break { given = "walk this way\n> ", returned = () }
Begin

back up, step forward:

λ back d
Break { given = "talk this way", returned = "TALK THIS WAY" }
λ back it
Break { given = (), returned = "talk this way" }
λ step it
Break { given = "talk this way", returned = "TALK THIS WAY" }
λ step it
TALK THIS WAY
End   { given = "TALK THIS WAY", returned = () }

(Note that when we step forward, the monadic computation reruns)

We can also use a different input than the default at the current stage:

λ back d
Break { given = "talk this way", returned = "TALK THIS WAY" }
λ d' <- use "(talk this way)" it
(talk this way)
λ printHistory d'
End   { given = "(talk this way)", returned = () }
Break { given = "talk this way", returned = "TALK THIS WAY" }
Break { given = (), returned = "talk this way" }
Break { given = "walk this way\n> ", returned = () }
Begin

And since the debuggers are normal immutable haskell values, we can use both d and d' without errors.

Cascades are still very limited. They're linear, and of a set length. They don't let you hook into functions that call themselves recursively, or functions that have computation paths better represented by trees or lattices.

But that doesn't mean those are necessarily impossible to model, either. For example, simple recursion is fairly easily captured with only a slight modification to Cascade

data CascadeR (ts :: [*]) where
  (:>>>)  :: x -> y -> CascadeR (y ': zs) -> CascadeR (x ': y ': zs)
  Fix     :: ((x -> y) -> x -> y) -> CascadeR (y ': zs) -> CascadeR (x ': y ': zs)
  Done    :: CascadeR '[t]