Zulip Chat Archive

Stream: general

Topic: Forward declarations


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Keeley Hoek (Aug 10 2018 at 09:43):

I'm now all about mutual definitions!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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⟩

view this post on Zulip Keeley Hoek (Aug 10 2018 at 09:48):

cheers

view this post on Zulip Kenny Lau (Aug 10 2018 at 09:48):

what does meta mean?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 10 2018 at 09:50):

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

view this post on Zulip Mario Carneiro (Aug 10 2018 at 09:50):

It turns off the safety

view this post on Zulip 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++

view this post on Zulip 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 )

view this post on Zulip Mario Carneiro (Aug 10 2018 at 09:51):

mutual inductive

view this post on Zulip Keeley Hoek (Aug 10 2018 at 09:52):

(thanks again for the practically instant help)

view this post on Zulip Keeley Hoek (Aug 10 2018 at 09:52):

beat me!

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 10 2018 at 09:53):

end is a keyword

view this post on Zulip 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

view this post on Zulip 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 :)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: May 14 2021 at 21:11 UTC