Forward declarations

Stream: general

[Keeley Hoek]

Is it possible to forward declare definitions in lean? I'd like to write something like

structure some_data -- forward declare structure because lean can't look ahead

def mutator_fn := some_data → some_data

structure some_data :=
  (the_data : list nat)
  (data_mutator : mutator_fn)

def some_data.mutate (my_data : some_data) : some_data := my_data.data_mutator my_data

and that way my_data.mutate would be able mutate itself, for example.

If you can't I'm pretty sad. :( Has it ever been asked for?

[Scott Morrison]

I'm not exactly sure what you're after yet, but "mutual defs" may be what you want, and I think are as close as you're going to get.

[Keeley Hoek]

I'm now all about mutual definitions!

[Mario Carneiro]

This sounds like an obvious source of unsoundness, so it's definitely by design that this isn't doable. I think you should explain in more detail what you are trying to do - there is likely a standard "functional" approach to your problem that does not require forward declaration.

[Mario Carneiro]

Rather than forward declaration, the structure can just refer to itself. Since this makes it recursive you have to define it with inductive:

meta inductive some_data
| mk (the_data : list nat)
     (data_mutator : some_data → some_data) : some_data

This has to be meta, though, because it is unsound

[Keeley Hoek]

Sure, this was just for programming in lean just like another functional language (i.e. with reckless abandon). Often functions invoke each other, for example. I was willing to sell my soul to the metas :D

[Mario Carneiro]

here is the mutator:

meta def some_data.mutate : some_data → some_data
| ⟨d, m⟩ := m ⟨d, m⟩

[Keeley Hoek]

cheers

[Kenny Lau]

what does meta mean?

[Johan Commelin]

Roughly that you are doing raw Lean. Without proof checking. So all tactics are written in meta land.

[Johan Commelin]

But Mario can give you a definition that is a lot better.

[Mario Carneiro]

It turns off the safety

[Mario Carneiro]

you can do unbounded recursion and non-positive inductives and other unsound things, as well as being able to call meta constants that have a definition in C++

[Keeley Hoek]

Actually, how might I solve a related problem, like declaring (toy example):

meta structure vertex :=
( color : string )
( adj_list : list edge )

meta structure edge :=
( start end : vertex )
( weight : nat )

[Mario Carneiro]

mutual inductive

[Keeley Hoek]

(thanks again for the practically instant help)

[Keeley Hoek]

beat me!

[Mario Carneiro]

meta mutual inductive vertex, edge
with vertex : Type
| mk (color : string) (adj_list : list edge) : vertex
with edge : Type
| mk (start end_ : vertex) (weight : nat) : edge

[Mario Carneiro]

end is a keyword

[Mario Carneiro]

Note that these are dangerous even in pure programming lean, because the pointer structure has cycles and lean is reference counted

[Keeley Hoek]

(In principle) there are countermeasures against rc cycles though, right? Are you saying that lean isn't able to find them at the moment?---if so, appreciate the heads up. thanks again :)

[Mario Carneiro]

Well, lean is pretty explicitly designed to make rc cycles impossible as a result of the type system

[Mario Carneiro]

I don't know if it does something special for meta mutual inductives, but I doubt it

[Mario Carneiro]

the goal is to have a strong enough type system that lean can assume powerful things about your code. Functional stuff like common subexpression evaluation is one simple example