dependent type in inductive variant?

Stream: Is there code for X?

[SnowFox]

Hello. I'm trying to fine-tune the parameters of an inductive variant but hit a type error. Is there a coersion trick I need?

inductive Q
| a : Pi (b : bool), if b then nat → Q else Q

type mismatch at application
  ite ↥b (ℕ → Q) Q
term
  Q
has type
  Sort ? : Type ?
but is expected to have type
  Sort (imax 1 ?) : Type (imax 1 ?)

[SnowFox]

I know I can do inductive Q | a (b : bool) (c : if b then nat else unit) but this doesn't suffice for my use case.

[Reid Barton]

I don't think this is valid in any schema for inductive types I've ever seen

[Reid Barton]

what would the recursor look like?

[Mario Carneiro]

You have to do inductive Q | a (b : bool) (c : if b then nat else unit). But you can still define a wrapper function that has the type you want

[SnowFox]

My real code for reference. This works, but I want to encode that rs3 isn't unit but doesn't exist for all other operations. Similarly, I want to inline reg_imm which is currently inductive reg_imm | register reg | imm int. But I'm fine either way on the reg_imm case because I can just coe reg and int to it respectively.

| arith (op : arith) (rd rs1 : reg)
  (rs2_imm : if op ∈ [xor, or, and, shiftl, shiftr, add] then reg_imm else reg)
  (rs3 : if op ∈ [fmadd, fnmadd, fmsub, fnmsub] then reg else unit)

[SnowFox]

Could you elaborate about the wrapper function? Not sure if it'd apply here. The easiest hack I can see as sugar for the consumer is to use opt_param unit () in place of unit but I still need to discard it when matching.

[SnowFox]

I'm perfectly fine to just discard it, I'm not matching it too many times. Just wanted to know if I could avoid it.

[Mario Carneiro]

You could have rs2 and rs3 in a type like arith_args : arith -> Type defined by pattern matching

[Mario Carneiro]

this seems a little smelly though

[Reid Barton]

Why not just pretend you're writing Haskell

[Reid Barton]

and then try to factor out as much repetition as possible

[SnowFox]

I guess I'll go with the code above with opt_param unit (). Thanks anyway.

[SnowFox]

I am trying to factor out the repetition here :)

[Reid Barton]

e.g. op can have three variants depending on which kind of rs2_imm and rs3 it takes

[Reid Barton]

right, but you're using way too powerful features to do so. You skipped the step "pretend you're writing in Haskell"

[SnowFox]

I'm not sure what you're proposing here. I did start with less powerful tools. I'm trying to reduce repetition and have done so. The only caveat which remained is that the last parameter doesn't belong in most cases but doesn't deserve its own variant.

[Reid Barton]

combine the op and rs2_imm and rs3 fields into one type, with three constructors

[Reid Barton]

It just seems to me that with putting if then else in the middle of your types, the best case scenario is that the ifs always reduce and you end up with something no harder to use than if you wrote something Haskell-style

[Mario Carneiro]

Or just throw everything into one arg type, that can be all of those things. That's what most assemblers do

[SnowFox]

I had this earlier too but felt it too verbose.

[SnowFox]

Hmm. This was unexpected to fail.

inductive Q | a (b : ℕ) (c : if b = 0 then ℕ else unit)
def f : Q → ℕ
| (Q.a 0 c) := c
| (Q.a b ()) := 0 -- Lean doesn't know b /= 0

[SnowFox]

I expected the pattern matching to recognize that if a parameter's type is assumed, then the condition must hold, constraining in this case b. :/

[Reid Barton]

Even if you had a hypothesis h : b /= 0 in the context, it would still fail

[Reid Barton]

because if b = 0 then ℕ else unit would not be definitionally equal to unit

[Reid Barton]

so you would need to insert a cast along (a proof of) the propositional equality (if b = 0 then ℕ else unit) = unit

[Reid Barton]

and that cast will cause headaches when you want to prove things about it later

[Reid Barton]

This issue only goes away when the if then else reduces to one of the branches--when precisely that happens depends on the decidable instance for the condition, but in your original example, it would only happen once op is a constructor

[Reid Barton]

and at that point, you are basically forced to treat the type the same way as if it had a separate constructor for each value of op, since you had to do cases on op in order to get the types of the fields to reduce

[Reid Barton]

That's why I said the best case scenario with this approach is that you get back what you would have had with the simple approach anyways

[SnowFox]

To be more specific; what I was trying to do was match | (arith op rd rs1 (rs2 : reg) ()) which I expected should imply (rs3 : unit) and op \in .. for this branch.

[SnowFox]

This is exactly an IFF, lacking the inverse implication. :/

[Reid Barton]

You could write a custom recursor which takes hypotheses of this form. But the application arith op rd rs1 (rs2 : reg) () is still ill-typed even when you "know" that op \in ...

[Reid Barton]

If you replace the variable op by a specific constructor then it could be well-typed

[Reid Barton]

(and you wouldn't need the ( _ : reg) part)

[SnowFox]

Right, but then we're manually matching every case which is what I was trying to avoid. :/

[SnowFox]

New plan; inline the op splits and call a helper. shrugs

[Mario Carneiro]

You could have another sub-inductive type to chunk up the different classes of arith op

[Mario Carneiro]

or multiple arith variants in the top level instruction inductive type

[SnowFox]

Each variation I try has more implications than I'd like... :/

[SnowFox]

I have had and will just return to using two arith variants.

[Mario Carneiro]

You can also map your one inductive type to multiple inductive types for categorization along different axes

[SnowFox]

@Mario Carneiro Current code -> https://gist.github.com/4d56511885f5b44514b0fcf006a5546a

[SnowFox]

Note the redundancies of arith arith_f and atomic_op.

[SnowFox]

However, a really really neat detail of Lean which I didn't catch until just now is that names can be shared between types. I.e. add is defined in all of these, yet Lean knows which one to match based on the types. :)

[SnowFox]

I mean, overlapping names in open arith arith_f

[SnowFox]

If only I could share the arith name inside the inst variants... the register types would distinguish the cases.

[SnowFox]

arith_f is fine though

[SnowFox]

Wait. Can open rename bindings? If so, then this might be viable for consumers? :O

[Reid Barton]

I think the syntax is open arith (renaming foo -> bar)

[SnowFox]

open inst (renaming arith_f -> arith) in this case.

[SnowFox]

This looks like it might just work. :D

[Reid Barton]

And yeah, if the same name is available in multiple open namespaces then Lean will make some effort to infer which one is needed based on the types

[SnowFox]

open arith arith_f inst (renaming arith_f → arith)
#check arith add (0 : reg integer) 0 0

Close! It doesn't know which to pick between arith_f.add and arith.add. Despite the register types forcing arith.add.

[SnowFox]

I might revert to the clearly distinguished cases and just rename the variants to overload it. :)

[SnowFox]

Yay. Moral of the story; match fat but simple. Overload the imports. :D