Zulip Chat Archive

Stream: Is there code for X?

Topic: dependent type in inductive variant?


view this post on Zulip 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 ?)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reid Barton (Oct 18 2020 at 13:18):

what would the recursor look like?

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 18 2020 at 13:24):

this seems a little smelly though

view this post on Zulip Reid Barton (Oct 18 2020 at 13:26):

Why not just pretend you're writing Haskell

view this post on Zulip Reid Barton (Oct 18 2020 at 13:27):

and then try to factor out as much repetition as possible

view this post on Zulip SnowFox (Oct 18 2020 at 13:27):

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

view this post on Zulip SnowFox (Oct 18 2020 at 13:27):

I am trying to factor out the repetition here :)

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip Reid Barton (Oct 18 2020 at 13:39):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip SnowFox (Oct 18 2020 at 13:49):

I had this earlier too but felt it too verbose.

view this post on Zulip 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

view this post on Zulip 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. :/

view this post on Zulip Reid Barton (Oct 18 2020 at 14:35):

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

view this post on Zulip Reid Barton (Oct 18 2020 at 14:36):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Oct 18 2020 at 14:37):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip SnowFox (Oct 18 2020 at 14:40):

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

view this post on Zulip 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 ...

view this post on Zulip Reid Barton (Oct 18 2020 at 14:42):

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

view this post on Zulip Reid Barton (Oct 18 2020 at 14:43):

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

view this post on Zulip SnowFox (Oct 18 2020 at 14:44):

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

view this post on Zulip SnowFox (Oct 18 2020 at 14:46):

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

view this post on Zulip Mario Carneiro (Oct 18 2020 at 16:01):

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

view this post on Zulip Mario Carneiro (Oct 18 2020 at 16:01):

or multiple arith variants in the top level instruction inductive type

view this post on Zulip SnowFox (Oct 18 2020 at 16:26):

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

view this post on Zulip SnowFox (Oct 18 2020 at 16:38):

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

view this post on Zulip 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

view this post on Zulip SnowFox (Oct 18 2020 at 17:09):

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

view this post on Zulip SnowFox (Oct 18 2020 at 17:10):

Note the redundancies of arith arith_f and atomic_op.

view this post on Zulip 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. :)

view this post on Zulip SnowFox (Oct 18 2020 at 17:12):

I mean, overlapping names in open arith arith_f

view this post on Zulip 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.

view this post on Zulip SnowFox (Oct 18 2020 at 17:14):

arith_f is fine though

view this post on Zulip SnowFox (Oct 18 2020 at 17:15):

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

view this post on Zulip Reid Barton (Oct 18 2020 at 17:15):

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

view this post on Zulip SnowFox (Oct 18 2020 at 17:16):

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

view this post on Zulip SnowFox (Oct 18 2020 at 17:16):

This looks like it might just work. :D

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip SnowFox (Oct 18 2020 at 17:21):

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

view this post on Zulip 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