argument has type _nested

Stream: lean4

[Anatoliy Baskakov]

I was trying to implement lambda calculus extended with records with unique keys.

The code goes

namespace List
  def keys (pairs : List (α × β)) : List α
    := match pairs with
      | [] => []
      | ⟨a, _⟩ :: rest => a :: keys rest

  def values (pairs : List (α × β)) : List β
    := match pairs with
      | [] => []
      | ⟨_, b⟩ :: rest => b :: values rest
end List

inductive Term : Type where
  | var : String → Term
  | app : Term → Term → Term
  | lam : String → Term → Term
  | record : (entries : List (String × Term)) → (unique : entries.keys.Nodup) → Term

It results in an error:

application type mismatch
  List.keys entries
argument has type
  _nested.List_1
but function has type
  List (String × Term) → List String

I have tried to tweak the definition a bit, factor out the record into a separate record, define it both generically and mutually with the term itself.

I still do not fully understand the reasoning behind it. Does it have to do with inductive-inductive? Why are such types prohibited? Are there plans to support it in the future? Is there no way around it?

[Jannis Limperg]

You're defining a nested inductive type because Term appears as an argument to another inductive type, List (and Prod). Lean internally translates such definitions into mutual inductive types. This translation creates a specialised List type; this is the _nested.List_1 from the error message. But apparently it doesn't also create a specialised List.keys, so entries.keys becomes ill-typed. I would consider this a bug.

As a workaround, you could remove unique from Term.record and create a predicate Term.WellFormed : Term -> Prop that characterises the well-formed terms (namely those where the record fields are unique). You'll probably want a type system anyway, in which case you can also push this property into the typing relation.

[Edward van de Meent]

i think the best way around this is not to use general List (A x B) for this inductive, but rather a special-purpose inductive Record definition, which you put together with Term in a mutual block.

[Jannis Limperg]

Even then, I think you'd have to define the function keys on Record mutually with Term and Record, so the type would become inductive-recursive (which is not supported). Is this actually a fundamental limitation of this translation?

[Edward van de Meent]

right....

[Edward van de Meent]

perhaps the best way is to rather use a get : String -> Option Term parameter...

[Edward van de Meent]

wait no, that allows for infinite records...

[Arthur Adjedj]

One way to avoid this issue would be to parametrise your inductive by the function you're using, namely List.keys. One caveat is that this inductive will live in a bigger universe:

inductive PreTerm (f : {α β : Type} → List (α × β) → List α): Type 1 where
  | var : String → PreTerm f
  | app : PreTerm f → PreTerm f → PreTerm f
  | lam : String → PreTerm f → PreTerm f
  | record : (entries : List (String × Term)) → (unique : (f entries).Nodup) → PreTerm f

def Term := PreTerm List.keys

[Jannis Limperg]

Nice idea, but you forgot to change Term to PreTerm in entries. And with that change, it doesn't work any more because of the universe bump:

inductive PreTerm (f : {α β : Type} → List (α × β) → List α): Type 1 where
  | var : String → PreTerm f
  | app : PreTerm f → PreTerm f → PreTerm f
  | lam : String → PreTerm f → PreTerm f
  | record : (entries : List (String × PreTerm f)) → (unique : (f entries).Nodup) → PreTerm f
/-
application type mismatch
  f entries
argument
  entries
has type
  List (String × PreTerm fun {α β} => f) : Type 1
but is expected to have type
  List (?m.703 entries × ?m.704 entries) : Type
-/

[Arthur Adjedj]

Oups.

[Mario Carneiro]

Here's a definition that works:

inductive PreTerm : Type where
  | var : String → PreTerm
  | app : PreTerm → PreTerm → PreTerm
  | lam : String → PreTerm → PreTerm
  | record : (entries : List (String × PreTerm)) → PreTerm

mutual
def PreTerm.WF : PreTerm → Prop
  | .var _ => True
  | .app f a => f.WF ∧ a.WF
  | .lam _ e => e.WF
  | .record e => e.keys.Nodup ∧ WF_list e
def PreTerm.WF_list : List (String × PreTerm) → Prop
  | [] => True
  | (_, e) :: es => e.WF ∧ WF_list es
end

def Term := {e : PreTerm // e.WF}

[Edward van de Meent]

indeed. although you might want to name it wellFormed rather than WF to distinguish it from wellFounded

[Anatoliy Baskakov]

Thank you for your answers! I will see what I can do with it.
Additionally, I have opened an issue on Lean's github, hopefully they will address it to simplify the matter