Typed forest - Haskell

I'm working on the notion of (for lack of better term) "typed forests" - which is a forest type (a tree with several roots) in which each node "determines" its children types (so, dependent types?). I use GADTs to represent the node types. Each GADT constructor represents the possible choice for a node in that location, with the GADT type a of that constructor being the children type allowed.

I posted an example in Slack, to represent food groups (each function below represents a single "path" in the food forest):

costcoRibEye :: X Food
costcoRibEye = Meat :/ Beef :/ RibEye :/ Costco

cheddar :: X Food
cheddar = Dairy :/ Cheese :/ AncetreCheddar

I am writing a blog post of sorts, to explain the concept. I'm likely to be missing the type system lingo to understand this concept better, but hopefully others would point me in the right direction.

( Inspiration for it came from obelisk-route library: https://github.com/obsidiansystems/obelisk/blob/master/lib/route/src/Obelisk/Route.hs )

Is this similar to Fix/recursion-schemes?

It seems like sort of nested sigma type?

The ultimate goal is to represent food hierarchy. "Ribeye" can only be a food item under the "Beef" group, which itself can only be positioned under "Meat". Every path (leading all the way to the leaf node) is considered an "item" to track in a journal. X Food = DSum Food Identity. And Food is defined like this:

data Food a where
  Meat :: Food (X Meat)
  ...
data Meat a where
  Beef :: Meat (X Beef)
  ..
data Beef a where
  RibEye :: Beef Producer
  ..
data Producer = Costco | ...

The leaf node is either () or some non-X type.

I'm looking forward to reading your blogpost!

As a bonus, creating a polysemy DSL for (monadically) building the forest is in my mind as well (I already use polysemy, but just not in an abstract fashion)

I think it would be nice to auto-generate polysemy effect for a given GADT. Maybe polysemy is an overkill; I only want to monadically build the tree. Funny how this problem domain is now coming to resemble HTML building using do syntax (which @TheMatten is doing in another topic).

Yup, a small amount of polysemy code comes in handy to define monads for building this tree/forest:

demo :: [X Mood]
demo = xlist do
  addX $ Mood_Good :/ xlist do
    addX $ Theme' :/ Theme_Learning
    addX $ Explore' (Markdown "This is too difficult") :/ mempty
    addX $ Belief' (Markdown "I can't solve this") :/ xlist do
      addX $ Fact' (Markdown "I will never know until I try") :/ mempty

Curious, are you using a tree when a graph is more suited? It seems like a "costco" might be used for more than ribeye

You are right. It is actually a graph (DAG) in practice.

And I've got a nice polysemy DSL to monadically build it.

Also, the whole thing is converging on looking to be XML like - _but_ fully type-safe.

eg: in XML node, we say "this node type can only contain this particular node types as children".

and the children can be either sum type (1 child), list (variable number children) or dependent map ( 0 to n children, corresponding to one or many of the n constructors in a sum type (GADT))

Well, actually, it is a graph (with or without cycles) only in type-level, but a tree at value-level. You can't have two arrows coming to one value.

Scratch all that ... it is best to think of this as a tree. A typed tree.

As for your example, the Costco value is simply replicated at the various nodes where it is used.

The Food tree type above, can be used in larger trees, for example:

data Health a where
  SkinCondition :: Health Skin
  Note :: Health (XList Note)
  Meals :: Health Natural
  Consumed :: Health (XList Food)  -- Food tree (forest actually, because XList f = [X f])

data Note a where
  Note_Normal :: Note Text
  Note_Highlight :: Note Text

And that tree can further be positioned in an even higher tree:

data Tracking :: Type -> Type where
  Tracking_Health :: Tracking (XMap Health.Health)
  Tracking_Feeling :: Tracking (XList Feeling.Mood)
  Tracking_Calisthenics :: Tracking (XMap Calisthenics.Move)

Here, we introduce XMap f which is DMap f Identity. The 'dependent map of children' above.

Even higher, the whole "Tracking" thing is positioned in a "calendar tree" (a tree of years, then months, then days)