Add default arguments to OpSignature to make Id default

[bollu]

In #191, a dialect consists of Op, Ty, and a monad m, leading to rather verbose variable/argument lists.

Possible Solutions

Make Id default

Often, when writing pure dialects, it is overhead to mention the monad. Consider making Id the default monad.

Introduce a Dialect structure

This structure would be defined as

structure Dialect 
  Op : Type
  Ty : Type
  m : Type -> Type

This way, we can have classes like OpSignature/OpDenote, but also datastructures like Com/Expr take just a d : Dialect argument. Consider, for example, the following code paraphrased from #191

variable (Op : Type) {Ty : Type} {m : Type → Type} [OpSignature Op Ty m]
mutual 
inductive Expr : (Γ : Ctxt Ty) → (eff : EffectKind) → (ty : Ty) → Type := ...

after introducing a Dialect struct, this would be shortened to

variable (d : Dialect) [OpSignature d]
mutual 
inductive Expr : (Γ : Ctxt d.Ty) → (eff : EffectKind) → (ty : d.Ty) → Type := ...

Besides being less verbose, it has the benefit of making it much easier to change what exactly constitutes a dialect in the future, since we only have to add/remove a field of the Dialect definition, instead of having to change every mention of OpSignatere,OpDenote, Com, Expr, Lets, etc. to include the new/removed variable (as we had to do in #191). In particular, making this change before #191 is merged, would make that diff substantially smaller.

[alexkeizer]

I agree with the problem, not sure I like the solution.

How about making a

structure Dialect 
  Op : Type
  Ty : Type
  m : Type -> Type

That would also make future refactors easier, without implicit/default magic.

I think it would also help consistency in other places, for example in Transform.lean, where we write

abbrev ExceptM  Op [OpSignature Op Ty] := Except (TransformError Ty)

We really only need Ty, but because everything else takes Op explicitly, and then infers Ty from the outParam on OpSignature, we chose to do the same here, even though we don't actually need Op or OpSignature for this definition. Making Dialect an explicit structure, would make that

abbrev ExceptM  (d : Dialect) := Except (TransformError d.Ty)

which feels cleaner to me

EDIT: only just noticed you also opened #252, which suggest exactly this change. I'm a bit confused: do you want to implement both? They seem two different (and mostly conflicting) solutions to the same problem to me. I guess we could make Id a default value for the m field of Dialect, but since we only have to mention the monad once in the Dialect-scenario, the overhead seems minimal?

[bollu]

I do not have a good sense of the tradeoffs, and would prefer to refactor this after #191 has been merged — we can try it out and see how it feels?

[alexkeizer]

Then I'd have a project management nit: this and #252 should be a single GH issue (since it's one "issue" with the code-base), which then mentions both possible solutions, so that there is a single clear home for discussion. I'll close #252, and edit this issue to include the Dialect solution

[alexkeizer]

I do not have a good sense of the tradeoffs, and would prefer to refactor this after #191 has been merged — we can try it out and see how it feels?

An important difference is that making Id default really only reduces verbosity when defining a dialect, it doesn't change anything for the definitions in Framework, which have to be generic over all monads that a dialect might use. So, my starting point is not that the problem is "it is unnecessary overhead to mention Id so often for pure dialects", it's that we have to mention the monad m so often at all, which is really only addressed by the Dialect struct.

I've tried out making the change (only for Framework so far, not downstream files) in #254, and the only thing that broke is that deriving Repr no longer works fully automatically, as I wrote there:

[...] Deriving Repr in the definition of Lets no longer works, so I've had to manually implement Repr instead. Presumably the derivation meta-code knows to insert [Repr Op] [Repr Ty] bounds when Op and Ty are arguments, but it doesn't know to insert [Repr d.Op] and [Repr d.Ty] bounds when Lets has an argument d : Dialect.

Admittedly, I don't know if anything else will break downstream. Doing Framework was fairly quick, so I'm happy to do the full refactor, then evaluate and potentially hold off on merging if we encounter anything that might cause problems, or merge if it continues to be as straightforward. Merging this would reduce a lot of the noise in #191's diff, as @tobiasgrosser correctly points out

[alexkeizer]

I've pushed #254 through: FHE and LLVM dialects were completely mechanical (net necessarily automatic, but in a very straightforward "go to the red squigly line and replace Op/Ty with either FooDialect or FooDialect.Op/FooDialect.Ty" sense). All proofs (in FHE/Rewrites and AliveAutoGenerated) are going through unchanged.

Ironically the only proof that does break, is in the supposedly simple PaperExamples dialect (specifically, the dialect with regions, which presumably is the problematic point, since neither LLVM nor FHE dialects use regions).

I should mention, this is after I made sure to define all dialects as an abbrev. When a dialect is defined as a def (which isn't marked reducible), this causes annoying problems, because TyDenote (MyDialect.Op) doesn't pick up on a TyDenote Op instance, nor does DecidableEq MyDialect.Op pick up on DecidableEq Op, etc. I've documented in Dialect that dialects should generally be defined as abbrevs, which certainly loses some beauty points, but I figure is still reasonable

[bollu]

Closed by https://github.com/opencompl/ssa/issues/252, https://github.com/opencompl/ssa/pull/254

[alexkeizer]

@bollu why did you reopen this? I thought it was addressed by the PRs you mentioned, no?