Free-like data structure:

Cool, that’s interesting to look at, but I guess I was wondering if there was some deeper way of thinking about this structure than just SNat n -> Compositions n f x -> Snee f x. I’m coming to terms with the fact that it’s not particularly special/important.

Side notes: Adjunction f g requires f to be isomorphic to (c,) for some c. This also means that Gree f a is isomorphic to Free f a, (ignoring bottoms), as they are both ([c],a). As such, I that case isn’t that interesting. They are all a pain to work with though . Here was my original use case:

data Reduction a b = End b | Step (Reduction a (Expr a -> b)) deriving Functor

Which is slightly annoying to work with, as it doesn’t permit analysis, but if I ever need that, I’ll just change it to Maybe. This is HOAS, but I think Gree is also similar to Bird and Paterson, Part 1 from here

schoolofhaskell.com

Bound - School of Haskell | School of Haskell

Just mentioning it of a datatype defined similar to Gree that I’d seen before.