{
"$type": "site.standard.document",
"bskyPostRef": {
"cid": "bafyreieu5wn4vgshqmggmci2f7xcft6flwsjm4n47ahubrag4bi52pmk7y",
"uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mktebb66jmb2"
},
"path": "/t/free-like-data-structure/14012#post_10",
"publishedAt": "2026-05-02T00:00:57.000Z",
"site": "https://discourse.haskell.org",
"tags": [
"HOAS",
"Bird and Paterson, Part 1",
"schoolofhaskell.com",
"Bound - School of Haskell | School of Haskell"
],
"textContent": "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.\n\nSide notes:\n`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 .\nHere was my original use case:\n\n\n data Reduction a b = End b | Step (Reduction a (Expr a -> b)) deriving Functor\n\n\nWhich 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\n\nschoolofhaskell.com\n\n### Bound - School of Haskell | School of Haskell\n\nJust mentioning it of a datatype defined similar to `Gree` that I’d seen before.",
"title": "Free-like data structure:"
}