Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.
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:
DSum Food Identity
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.
DMap f Identity
Even higher, the whole "Tracking" thing is positioned in a "calendar tree" (a tree of years, then months, then days)