nested occurrence [..] contains variables that are not pa...

Stream: general

[SnowFox]

Hello. Can someone shed some light on this unusual error?

inductive foo : nat -> Type
| alpha {n} : foo n
| beta {n} (foos : list (foo n)) : foo n

nested occurrence 'list.{0} (foo n)' contains variables that are not parameters

[Mario Carneiro]

This is called a nested inductive type, because you have the type you are defining inside the argument to another inductive type. Lean's support for nested inductives is extremely limited and I recommend you avoid them entirely. It's usually possible to rewrite things to avoid them, although that would require some more context to #xy it properly

[SnowFox]

Okay. The X I want to describe is the Regionalized Value State Dependency Graph; which I want to generalize over the primitive operations (a dialect). RVSDG -> https://arxiv.org/abs/1912.05036 ; with 2 initial dialects, RISC-V as we've previously discussed, and GrTT, a type theory with grades and dependent types. GrTT extends RDT which I think I've mentioned before. https://arxiv.org/abs/2010.13163 ; After these two, I plan to experiment with WebAssembly and SPIRV (GPU shader target).

[SnowFox]

In addition to generalizing RVSDG; I'd like to enrich it with Equality Saturation and Proof Generalization. http://www.cs.cornell.edu/~ross/publications/eqsat/ + http://www.cs.cornell.edu/~ross/publications/proofgen/

[SnowFox]

(Which has direct implications for the representation)
I hit these errors while trying to describe a graph with its nodes and its edges, using a set of (node \x node) as the edges.

[SnowFox]

Current mock minus problematic attempts to make it more strict. Notably adding input/output counts on the node type GADT style, and describing edges as set (node \x node).

inductive node (operation : Type)
-- primitive operations
| simple (operation : operation) : node
-- symmetric split and join; if-then-else; case-with
| gamma (branches : nat -> node) : node
-- tail-controlled loops; do-while
| theta (body : list node) : node
-- lambda
| lambda (body : list node) : node
-- global variables
| delta (body : list node) : node
-- mutually recursive environments; primitive recursion
| phi (lambdas : list node) : node
-- translation units
| omega (body : list node) : node

[SnowFox]

The omega node kinda doesn't make sense to include as it is just the root of the graph itself and can't be a child node. Phi only accepts lambda nodes (though its definition could be expanded to understand non-lambdas by basically ignoring them)

[SnowFox]

(Currently ignoring the eqsat representation implications. Eqsat requires an equivalence graph. Optimizations enrich the graph with equivalences instead of destructively updating it. Thus optimizations may be applied in any order up to any depth the resources permit to search the space efficiently while avoiding exponential blowup.)

[Mario Carneiro]

What's the version you would like to write?

[Mario Carneiro]

You can probably avoid the cardinality limitations if you use finset instead of set, although that can't be used directly in an inductive type

[SnowFox]

I'm not exactly sure what I want yet. There are several node types: simple (primitive operation), gamma (branches), theta (do-while), lambdas, delta (global constants), and phi (mutual recursion & primitive recursion). Phi can only contain lambdas. Due to normalization regions shouldn't really be lists of nodes because the order is irrelevant. The edges connect node outputs and region arguments to node inputs and region results. The edges represent data as either values or state; where state imposes strict ordering but may be fine grained (I.e. non-aliased memory accesses are unordered unless explicitly sequenced).

The operations need to be a type parameter representing the respective dialects. Let this be GrTT, RISC-V, WASM, or SPIRV. A simple node inherits the input and output types from the primitive operations. I.e. RISC-V addi takes one input integer register and a signed 12-bit immediate value, which then returns a single XLEN integer register. All composition must preserve these types.

For equality saturation each node or set of nodes or region may have multiple equivalent implementations. As optimization works by adding equivalent alternatives without destructively corrupting the graph. Sharing all common subgraphs along the way.

Reconsidering set; I'd have to pairwise query the set to recover its members for analysis... so that was probably the wrong tool to reach for. I'm not seeing the ability to enumerate a finset either, even if its cardinality is allowed in the inductive definition.

[SnowFox]

Although I have several dialects in mind for the IR; I'd like to focus on GrTT as its types are the most demanding and helpful. Notably the grades on types include quantities of binder usages in both values and in their types. The \forall operator is defined as a Pi-type whose value-usage is zero. Correctly erasing the binder from value reach. Similarly linear arrows \-o are Pi-type whose value-usage is one. In addition to the quantities, I'll be tracking sensitive dataflow for taint analysis. Classified data may not be made public (without and only after explicit declassification) and may not be translated to observable data-dependent machine code (at least for the RISC-V target; I can't exactly rely on either WASM nor SPIRV for this kind of safety --- even for RISC-V the specification doesn't require add/mul et al to be constant-time; though there is a proposed extension (which I can't find...) which adds this.)

[SnowFox]

The ideal starting point would be an acyclic hierarchical multigraph enriched with equivalences. To then define RVSDG atop.

[Mario Carneiro]

I'm not seeing the ability to enumerate a finset either, even if its cardinality is allowed in the inductive definition.

In that case it sounds like you want a list (node x node)

[SnowFox]

If Lean shares the immutable data and doesn't explode here; sounds good. Either way I'll need to figure out how to efficiently represent the equivalence graph and treat the order of these lists as irrelevant such that equivalent regions which differ only by definitional order are not repeated.