Zulip Chat Archive

Stream: general

Topic: Forward declarations


Keeley Hoek (Aug 10 2018 at 09:34):

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 (Aug 10 2018 at 09:36):

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 (Aug 10 2018 at 09:43):

I'm now all about mutual definitions!

Mario Carneiro (Aug 10 2018 at 09:43):

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 (Aug 10 2018 at 09:46):

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 (Aug 10 2018 at 09:47):

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 (Aug 10 2018 at 09:48):

here is the mutator:

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

Keeley Hoek (Aug 10 2018 at 09:48):

cheers

Kenny Lau (Aug 10 2018 at 09:48):

what does meta mean?

Johan Commelin (Aug 10 2018 at 09:50):

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

Johan Commelin (Aug 10 2018 at 09:50):

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

Mario Carneiro (Aug 10 2018 at 09:50):

It turns off the safety

Mario Carneiro (Aug 10 2018 at 09:51):

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 (Aug 10 2018 at 09:51):

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 (Aug 10 2018 at 09:51):

mutual inductive

Keeley Hoek (Aug 10 2018 at 09:52):

(thanks again for the practically instant help)

Keeley Hoek (Aug 10 2018 at 09:52):

beat me!

Mario Carneiro (Aug 10 2018 at 09:53):

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 (Aug 10 2018 at 09:53):

end is a keyword

Mario Carneiro (Aug 10 2018 at 09:56):

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

Keeley Hoek (Aug 10 2018 at 10:23):

(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 (Aug 10 2018 at 10:24):

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

Mario Carneiro (Aug 10 2018 at 10:25):

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

Mario Carneiro (Aug 10 2018 at 10:27):

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


Last updated: Dec 20 2023 at 11:08 UTC