parametricity

Stream: general

[Cyril Cohen]

Hi, @Johannes Hölzl @Mario Carneiro @Rob Lewis,
I am debugging my -- very buggy -- parametricity plugin. Could you tell me the shortest way to get the name of an inductive type from the name of its recursor? (I found environment.inductive_type_of to get it from the name of a constructor, but I cannot find the same for the recursor, and taking just the namespace sounds dirty to me...)

[Johannes Hölzl]

Hm, it looks like there is no other (easy) option. You can analyse the type of the recursor, and try to get the inductive type from this, but this is not easy: there is an arbitrary number of parameters, I guess you need to analyse the motive to figure out what is a parameter and what is the actual inductive value...

[Mario Carneiro]

For an arbitrary recursor accepted by induction, the type is a bunch of pis followed by C a1 ... an where C is a variable in the context. The type of this variable is a bunch of pis ending in Type or Prop, and the last argument should have the type T b1 ... bn where T is the type in question

[Mario Carneiro]

But if you know it's a builtin recursor the easiest way is just to knock off the last segment from the name

[Mario Carneiro]

Oh wait, that doesn't work for the nondependent recursors. I think you can always look at the last pi in the type, which will have type T b1 ... bn

[Mario Carneiro]

for example:

inductive T (α : Type) : Type → Prop
| mk1 : T nat
| mk2 : T α

#print T.rec
-- protected eliminator T.rec : ∀ {α : Type} {C : Type → Prop},
-- C ℕ → C α → ∀ {a : Type}, T α a → C a
#check @T.drec
-- T.drec : ∀ {α : Type} {C : Π (a : Type), T α a → Prop},
-- C ℕ _ → C α _ → ∀ {a : Type} (n : T α a), C a n

Note that the last pi in the type has T α a as its domain, where T is what you want

[Cyril Cohen]

Sure I know where to get the the type of the inductive from the type of the recursor, but I was looking for a primitive that I think is missing from the API... What does not work for nondependent recursors?

[Mario Carneiro]

I think if we can figure it out there is no need for an API function

[Mario Carneiro]

we can add it to mathlib

[Cyril Cohen]

an API function would always be more efficient than retro-engineering... since the recursor is generated when the inductive type is added it should be indexed in the same way the constructors are...

[Mario Carneiro]

the API function would do what I just said, this information is not stored

[Cyril Cohen]

at least it would be coded in C++... meh I guess for my use case efficiency does not matter, but it's a matter of uniformity

[Cyril Cohen]

anyway, take the number of parameters + 1 pis out, then take the next pi, take its head symbol, done

[Mario Carneiro]

sure but you could say that about anything

[Cyril Cohen]

oh + the number of constructors

[Mario Carneiro]

well you can't get the constructors until you know the type...

[Cyril Cohen]

oh right... so last pi then

[Mario Carneiro]

right

[Cyril Cohen]

sure but you could say that about anything

Since the API function is there for constructors, it should also be there for anything that is generated by adding an inductive, such as recursors. I think none or both should be part of the core api, that is all I am saying.

[Mario Carneiro]

I think that's reasonable, but, well, core is frozen

[Cyril Cohen]

Oh right, I forgot about that, sorry for the noise :thinking:

[Cyril Cohen]

meta def environment.trailing_pi_type_of (env : environment) : expr → option name
 | (pi _ _ t b) := match b with
   | (pi _ _ _ _) := environment.trailing_pi_type_of b
   | _ := some t.get_app_fn.const_name
   end
 | _ := none

meta def environment.inductive_type_of_rec (env : environment) (n : name) : exceptional name := do
  decl ← env.get n,
  match env.trailing_pi_type_of decl.type with
  | some i := return i
  | none := exceptional.fail $ "inductive_type_of_rec: not a recursor " ++ to_string n
  end

[Cyril Cohen]

or for the second one:

meta def environment.inductive_type_of_rec (env : environment) (n : name) : option name :=
  match env.get n with
  | (exceptional.success decl) := env.trailing_pi_type_of decl.type
  | _ := none
  end

[Cyril Cohen]

@Mario Carneiro @Johannes Hölzl @Rob Lewis I am confused by the output of #print has_zero.zero i.e.

def has_zero.zero : Π (α : Type u) [c : has_zero α], α :=
λ (α : Type u) [c : has_zero α], [has_zero.zero c]

what construction is [has_zero.zero c] internally? I figured it is a "macro", but I cannot find its API... is it possible to get its expansion?

[Johannes Hölzl]

its a projection. so the projection data you get out of environment should tell you what the inductive is and which position of the constructor it is from. The macro hides a application of the recursor.

[Cyril Cohen]

Nevermind, I was looking for environment.unfold_all_macros