Agda to Lean translation issue

Stream: lean4

[Sofia]

Have I not translated this correctly?

record func {k : Level}(ℓ : Level)(I J : Set k) : Set (k ⊔ (sucL ℓ)) where
  constructor mk
  field
    out : J → IDesc ℓ I

⟦_⟧func : ∀{k ℓ}{I J : Set k} → func ℓ I J → (I → Set ℓ) → (J → Set ℓ)
⟦ D ⟧func X j = ⟦ func.out D j ⟧ X

data μ (D : func ℓ I I)(i : I) : Set ℓ where
  ⟨_⟩ : ⟦ D ⟧func (μ D) i → μ D i

inductive Fixpoint : (I -> Desc I) -> I -> Type u
  | step : (D i).over (Fixpoint D) -> Fixpoint D i

error: (kernel) arg #4 of 'Desc.Fixpoint.step' contains a non valid occurrence of the datatypes being declared

[Sofia]

Desc.over d x is ⟦ d ⟧ x

[Marcus Rossel]

I don't know about Agda, but the error is probably due to the fact that you're referring to Fixpoint in its own constructor in an invalid position (there's some rules as to what's a valid position).
How is Desc.over defined?

[Sofia]

/- A Cosmology of Datatypes. Pierre- ́Evariste Dagand.
https://www.irif.fr/~dagand/stuffs/thesis-2011-phd/thesis.pdf -/
inductive Desc : Type u' -> Type (max u' (u + 1))
  | var   : I -> Desc I
  | const : Desc I
  | prod  : Desc I -> Desc I -> Desc I
  | sigma : (S : Type u) -> (S -> Desc I) -> Desc I
  | pi    : (S : Type u) -> (S -> Desc I) -> Desc I

namespace Desc
  -- FIXME: Better name? interpret?
  def over : Desc.{u} I -> (I -> Type u) -> Type u
    | var i,     X => X i
    | const,     _ => Lift Unit
    | prod a b,  X => a.over X × b.over X
    | sigma S D, X => (s : S) ×  (D s).over X
    | pi    S D, X => (s : S) -> (D s).over X

  inductive Fixpoint : (I -> Desc I) -> I -> Type u
    | step : (D i).over (Fixpoint D) -> Fixpoint D i
end Desc

[Sofia]

That does seem to be the error, if so either I have translated it incorrectly or this is a divergence between Agda and Lean; which typically means there is an alternative approach to encode this. I hope?

[Sofia]

Also the Agda. https://pages.lip6.fr/Pierre-Evariste.Dagand/stuffs/thesis-2011-phd/model/html/Chapter5.IDesc.html

[Sofia]

If this is a divergence. How are my chances for the limitation being lifted if merely arbitrary and not yet known useful?

[Sofia]

https://github.com/leanprover/lean4/blob/master/src/kernel/inductive.cpp#L380-L397

[Sebastian Ullrich]

Lean's positivity checker does not unfold definitions. And even if it did, it would likely be stuck at the recursor implementing over. And even if it handled that, nested inductives still have to be translated to mutual inductives, which the recursion would make either very difficult or perhaps impossible. So this does look like a stack of complicated extensions to me.

[Sofia]

Aww. :/

[Marcus Rossel]

Sofia said:

If this is a divergence. How are my chances for the limitation being lifted if merely arbitrary and not yet known useful?

IIRC, other languages/proof assistants like Agda or Coq tend to handle more of the "non-standard" inductive declarations, but at the cost of moving this complexity into the kernel (which also increases the TCB). I think with Lean a small kernel is preferred. But there have been discussions on Zulip about how it would be nice to have certain non-standard inductives natively in Lean (but for that the underlying theory would have to be proven to work first).

[Marcus Rossel]

Usually @Mario Carneiro knows how to transform cases like Fixpoint into simpler inductives though :D

[Sofia]

For context I am trying to take a stab at an intrinsically typed implementation of the Calculus of Constructions for my own compiler, which I'm writing in Lean 4. The exact code I'm trying to translate is a description of type universes, which is first-class, can bootstrap itself and enable programming over the calculus of types within the language.

[Sofia]

In other words... I dived in the deep end. :D

[Mario Carneiro]

Marcus Rossel said:

Usually Mario Carneiro knows how to transform cases like Fixpoint into simpler inductives though :D

@Sofia Voilà:

namespace Desc
  inductive Over (X : I -> Desc.{u, v} I) : Desc.{u, v} I -> Type (max (u+1) v)
    | var : Over X (X i) → Over X (.var i)
    | const : Over X .const
    | prod : Over X a → Over X b → Over X (.prod a b)
    | sigma (s : S) : Over X (D s) → Over X (.sigma S D)
    | pi : (∀ s : S, Over X (D s)) → Over X (.pi S D)

  def Fixpoint (D : I -> Desc.{u, v} I) (i : I) : Type (max (u+1) v) :=
    Over D (D i)
end Desc

[Notification Bot]

Sofia has marked this topic as unresolved.

[Sofia]

Hmm. @Mario Carneiro I'm not sure this satisfies what I need. And I'm struggling to port any successive code to test it.

https://www.irif.fr/~dagand/stuffs/thesis-2011-phd/thesis.pdf

I think it would be best for me to step back and return to the start of the thesis. I will likely return with lots more problems. Wish me luck.

[Jad Ghalayini]

@Sofia out of curiosity are you too doing metatheory in lean?

[Sofia]

@Jad Ghalayini By meta-theory you mean proving properties hold on the type theory? Maybe? The objective is to implement the interpreter for the language I want, then bootstrap a complete compiler using it. I want an intrinsically typed DTLC/CoC enriched with type grades and multiple stages. Thus all type checking will be enforced in the structure. Once I have this, I will work on a parser and elaborator. Then try to reimplement all of that within the language and continue with other components.

[Sofia]

If by meta-theory you meant the type checking, then yes. Intrinsically if I can. I have an intrinsically typed implementation of STLC.

https://gist.github.com/sofia-snow/0a85cb5ccf6cbeb6ba248813df7bbf0b

The current goal is to retain this style over a DTLC, using the indexed type family descriptions as an indirection for the type in the DTLC term's types.

[Arthur Paulino]

@Sofia I was able to build a parser/elaborator for my language using Lean's Syntax and native parser. But the solution looks a bit hacky. When you start working on your parser, please let me know because I am interested in learning :pray:

[Sofia]

Oh please share that hackery. I have considered doing exactly this for the bootstrapping.

[Sofia]

I plan to make a parser quite similar to Lean's, however it will be constrained by the profunctor/optic laws such that syntax resugaring is formally defined and accurate. https://raw.githubusercontent.com/justinpombrio/thesis/master/resugaring-thesis.pdf

[Sofia]

Which in turn means the compiler can produce syntax and type errors for user-defined syntax without leaking under the abstractions. Ex. A type error for a user-defined DSL should point at the DSL's terms, as written by the user. Without canonicalization and without pointing into the abstractions (code the user didn't write, but the macros expanded to).

[Arthur Paulino]

Are you interested in reading code from an arbitrary text file or from a Lean file?

[Arthur Paulino]

If you want to parse code from a Lean file, then it's not hacky. I use it to debug my interpreter: https://github.com/arthurpaulino/FxyLang/blob/master/MetaDebug.lean

But if you want to read from a text file from the IO monad, then you need to lift a meta monad with an environment created from the compiled olean file (this is the hack):
https://github.com/arthurpaulino/FxyLang/blob/master/FxyLang/Implementation/Parser.lean

[Jad Ghalayini]

@Sofia well I mean if you're proving smt about the type theory in Lean that's what I'd call metatheory haha

[Sofia]

@Arthur Paulino That'll be both, also from stdin for a repl eventually. Thanks.

@Jad Ghalayini Then yes. :)

[Arthur Paulino]

Sebastian said that eventually we'll have builtin syntax, which is likely to eliminate the need for this hack

[Sofia]

I don't quite see where the hacky part is. :)

[Arthur Paulino]

This is the hacky part. I can't release a standalone binary for my interpreter without a companion olean file

[Sofia]

Huh.

[Arthur Paulino]

Sorry, the problematic code isn't in the file I had linked previously. It's in the Main.lean file

[Sofia]

Yeah I see. :)

[Arthur Paulino]

As I said, I am interested in new approaches. @Simon Hudon might be as well

[Sofia]

Noted, though I will probably mirror your approach until I can bootstrap my language in itself, and _then_ implement its own parser in itself. Not in Lean.

[Sofia]

Though it would probably be wise to just prototype the parser in Lean first, having all the tooling established already.