Zulip Chat Archive
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 if
s 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... :/
SnowFox (Oct 18 2020 at 16:38):
I have had and will just return to using two arith variants.
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: Dec 20 2023 at 11:08 UTC