## Stream: Is there code for X?

### Topic: dependent type in inductive variant?

#### SnowFox (Oct 18 2020 at 13:09):

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 (Oct 18 2020 at 13:11):

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 (Oct 18 2020 at 13:14):

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

#### Reid Barton (Oct 18 2020 at 13:18):

what would the recursor look like?

#### Mario Carneiro (Oct 18 2020 at 13:18):

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 (Oct 18 2020 at 13:19):

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 (Oct 18 2020 at 13:22):

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 (Oct 18 2020 at 13:22):

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 (Oct 18 2020 at 13:24):

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

#### Mario Carneiro (Oct 18 2020 at 13:24):

this seems a little smelly though

#### Reid Barton (Oct 18 2020 at 13:26):

Why not just pretend you're writing Haskell

#### Reid Barton (Oct 18 2020 at 13:27):

and then try to factor out as much repetition as possible

#### SnowFox (Oct 18 2020 at 13:27):

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

#### SnowFox (Oct 18 2020 at 13:27):

I am trying to factor out the repetition here :)

#### Reid Barton (Oct 18 2020 at 13:28):

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

#### Reid Barton (Oct 18 2020 at 13:28):

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

#### SnowFox (Oct 18 2020 at 13:35):

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 (Oct 18 2020 at 13:39):

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

#### Reid Barton (Oct 18 2020 at 13:41):

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 (Oct 18 2020 at 13:48):

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

#### SnowFox (Oct 18 2020 at 13:49):

I had this earlier too but felt it too verbose.

#### SnowFox (Oct 18 2020 at 14:31):

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 (Oct 18 2020 at 14:34):

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 (Oct 18 2020 at 14:35):

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

#### Reid Barton (Oct 18 2020 at 14:36):

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

#### Reid Barton (Oct 18 2020 at 14:36):

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

#### Reid Barton (Oct 18 2020 at 14:37):

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

#### Reid Barton (Oct 18 2020 at 14:38):

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 (Oct 18 2020 at 14:39):

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 (Oct 18 2020 at 14:39):

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 (Oct 18 2020 at 14:39):

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 (Oct 18 2020 at 14:40):

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

#### Reid Barton (Oct 18 2020 at 14:41):

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 (Oct 18 2020 at 14:42):

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

#### Reid Barton (Oct 18 2020 at 14:43):

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

#### SnowFox (Oct 18 2020 at 14:44):

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

#### SnowFox (Oct 18 2020 at 14:46):

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

#### Mario Carneiro (Oct 18 2020 at 16:01):

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

#### Mario Carneiro (Oct 18 2020 at 16:01):

or multiple arith variants in the top level instruction inductive type

#### SnowFox (Oct 18 2020 at 16:26):

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

#### Mario Carneiro (Oct 18 2020 at 16:49):

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

#### SnowFox (Oct 18 2020 at 17:09):

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

#### SnowFox (Oct 18 2020 at 17:10):

Note the redundancies of arith arith_f and atomic_op.

#### SnowFox (Oct 18 2020 at 17:11):

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 (Oct 18 2020 at 17:12):

I mean, overlapping names in open arith arith_f

#### SnowFox (Oct 18 2020 at 17:14):

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

#### SnowFox (Oct 18 2020 at 17:14):

arith_f is fine though

#### SnowFox (Oct 18 2020 at 17:15):

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

#### Reid Barton (Oct 18 2020 at 17:15):

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

#### SnowFox (Oct 18 2020 at 17:16):

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

#### SnowFox (Oct 18 2020 at 17:16):

This looks like it might just work. :D

#### Reid Barton (Oct 18 2020 at 17:17):

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 (Oct 18 2020 at 17:19):

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 (Oct 18 2020 at 17:21):

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

#### SnowFox (Oct 18 2020 at 17:27):

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

Last updated: May 17 2021 at 15:13 UTC