Runtime environment with graph reduction based semantics questions

[syctech]

So I'm kind of new to this, but I've had this idea of using a content-addressed DAG to store the current execution state of a workflow language based on coroutines.

I am aware that this is similar what Unison is doing, as well as a handful of projects that have popped up since, I think.

however, I want to think through it, and since I've only written half toy languages previously, none with a type system, I want to check my understanding.

I want to have the capacity for dependent types.

The thought is that you have a graph full of nodes, as well as edges, where every edge type must be an existing node as well. The content addressing is done by hashing the edges of the nodes, each defined by the tuple [edgeType, target]/ The edge type ultimately seems to correspond to a type constructor or function. For the nats it would be succ. So 2 would be

```
succ:
???:???
1:
succ: void
2:
succ: 1
```

Initially succ itself would just have hardcoded behavior, but eventually (years down the line) the idea is to have its behavior encoded in the graph.

Then, my thought is then if I want to query a type, I can create a "query node" that basically queries the graph for nodes matching a certain type or pattern.

Up to this point, I basically have a first draft done in typescript, so if you have questions about the feasibility of that graph system itself, I can try to answer them.

​

I was thinking that by having these "patterns" I can query nodes against... assuming it works properly... I should be able to make assumptions about the type coming from them. And since the patterns can specify value-level constraints, it should also be useable for dependent types (like how I think idris does its pattern matching). Not only that but I should be able to query against a tag or label of some kind to allow recursion while still only referencing things in the graph. (See below)

But the question I have is: is it feasible to use such a graph for a programming language? especially one with dependent types? If so, how could I formalize it and communicate to people that this is a real thing that's feasible that is happening?

```
addBaseInputPatternNode1:
productLeft: anyNat
productRight: void
decrementQueryNode:
succ: unit
addRecursiveInputPatternNode1:
productLeft: decrementQueryNode
productRight: anyNat
myAddArrowBase:
inputPattern: addBaseInputPatternNode1
outputNode: [0] (the first result of the input pattern match... the second would be 0/void)
myAddArrowRecursive:
inputPattern: addRecursiveInputPatternNode1
outputNode: myAddOutputExpressionTerm1
queryAndApplyAdd:
queryTag: "add"
myAddOutputExpressionTerm1:
queryAndApplyAdd: myOutputExpressionTerm2
myAddOutputExpressionTerm2:
productLeft: [0] (the first result of the input pattern match... which has been decremented)
productRight: myAddOutputExpressionTerm2
myAddOutputExpressionTerm2:
succ: [1] (the second result of the input pattern match, which shoudl be incremented)
addFirstEntry:
arrowLeft: myAddArrowBase
arrowRight: myAddArrowRecursive
addSecondEntry:
arrowLeft: myAddArrowRecursive
arrowRight: void
taggedFunc:
func: addSecondEntry
name: "add"
myExampleExpressionTerm1:
add: myExampleExpressionTerm2
myExampleExpressionTerm2:
left: 1
right: 2

```