Zulip Chat Archive

Stream: lean4

Topic: Thunk Bind

Scott Viteri (Apr 22 2021 at 13:30):

Am I misunderstanding Thunk?
When I write

def h := Thunk.pure "hi"
#eval (Thunk.bind h Thunk.pure).get

I am expecting to see "hi", since bind should extract "hi" from h, apply Thunk.pure to it, and get should get the contents.

Mario Carneiro (Apr 22 2021 at 13:32):

what do you get?

Scott Viteri (Apr 22 2021 at 13:32):

processing...

Mario Carneiro (Apr 22 2021 at 13:32):

does it work from the console

Scott Viteri (Apr 22 2021 at 13:34):

segfault

Scott Viteri (Apr 22 2021 at 13:34):

let me isolate it for a more rigorous test

Scott Viteri (Apr 22 2021 at 13:35):

segfault

Daniel Fabian (Apr 22 2021 at 13:35):

FYI, there was an update around yesterday to the vscode extension that fixed what looked like infinite loops for me. Please make sure you have 0.0.24

Scott Viteri (Apr 22 2021 at 13:36):

In emacs

Daniel Fabian (Apr 22 2021 at 13:36):

Scott Viteri (Apr 22 2021 at 13:36):

But also, running from the console does not fix

Scott Viteri (Apr 22 2021 at 13:36):

Lean (version 4.0.0-nightly-2021-03-14, commit c54a7c8ccc75, Release)

Mario Carneiro (Apr 22 2021 at 13:37):

that's pretty old, try updating your nightly

Scott Viteri (Apr 22 2021 at 13:38):

Lean (version 4.0.0-nightly-2021-04-06, commit e863376be155, Release)
Same issue

Mario Carneiro (Apr 22 2021 at 13:38):

it's 2021-04-22 today

Scott Viteri (Apr 22 2021 at 13:39):

right, just pasted what elan updated me to when I asked for nightly -- I'll switch to 4/22 explicitly

Mario Carneiro (Apr 22 2021 at 13:41):

updated just now, this is what I got:

$ elan update leanprover/lean4:nightly
info: syncing channel updates for 'nightly'
info: latest update on nightly, lean version nightly-2021-04-22
info: downloading component 'lean'
103.9 MiB / 103.9 MiB (100 %)   9.8 MiB/s ETA:   0 s
info: installing component 'lean'

  leanprover-lean4-nightly updated - Lean (version 4.0.0-nightly-2021-04-22, commit 20cbb4389a4c, Release)

Scott Viteri (Apr 22 2021 at 13:41):

right just did this

Scott Viteri (Apr 22 2021 at 13:41):

Lean (version 4.0.0-nightly-2021-04-22, commit 20cbb4389a4c, Release)
~/LocalSoftware/signatures/lean4/Cdclt $ lean hi.lean
segmentation fault (core dumped)

Mario Carneiro (Apr 22 2021 at 13:42):

but I am also getting the segfault

Scott Viteri (Apr 22 2021 at 13:46):

#eval (Thunk.pure h.get).get
produces "hi" as expected

Mario Carneiro (Apr 22 2021 at 13:50):

It's a bit suspicious that thunk_bind_fn_closure is basically the same as thunk_map_fn_closure. I think there should be a lean_thunk_get(r) in there

Scott Viteri (Apr 22 2021 at 13:51):

and #eval (Thunk.bind h (λ a:String => (⟨λ x:Unit => a⟩ : Thunk String))).get returns processing...

Daniel Fabian (Apr 22 2021 at 13:56):

I find the ref counting suspicious.

Daniel Fabian (Apr 22 2021 at 13:56):

static obj_res thunk_map_fn_closure(obj_arg f, obj_arg t, obj_arg /* u */) {
    b_obj_res v = lean_thunk_get(t);
    lean_inc(v);
    obj_res r = lean_apply_1(f, v);
    lean_dec(v);
    return r;
}

Mario Carneiro (Apr 22 2021 at 13:56):

By the way, if you use 2 instead of "hi" it's a little safer, you won't get a segfault but 0 is not the right answer

Daniel Fabian (Apr 22 2021 at 13:56):

static obj_res thunk_bind_fn_closure(obj_arg x, obj_arg f, obj_arg /* u */) {
    b_obj_res v = lean_thunk_get(x);
    lean_inc(v);
    obj_res r = lean_apply_1(f, v);
    lean_dec(x);
    return r;
}

Mario Carneiro (Apr 22 2021 at 13:57):

The refcounting is a bit of black art to me

Mario Carneiro (Apr 22 2021 at 13:57):

I'm not sure what the rules are

Daniel Fabian (Apr 22 2021 at 13:57):

yeah, I bet. I don't quite get what's going on. But what I do notice, is that in the upper example you incr and decr the same var.

Daniel Fabian (Apr 22 2021 at 13:58):

and in the 2nd you incr and decr different vars

Mario Carneiro (Apr 22 2021 at 14:00):

But even ignoring the refcounts (which could indeed cause a segfault if not arranged properly), we aren't calling get twice inside bind. My guess is that it's interpreting the thunk r as a string and the segfault results because they have different data layout

Daniel Fabian (Apr 22 2021 at 14:01):

as in we should be getting the r before returning it?

Daniel Fabian (Apr 22 2021 at 14:01):

given that the whole code is wrapped in a thunk again?

Daniel Fabian (Apr 22 2021 at 14:02):

protected def Thunk.bind {α : Type u} {β : Type v} (x : Thunk α) (f : α → Thunk β) : Thunk β :=
  ⟨fun _ => (f x.get).get⟩

Mario Carneiro (Apr 22 2021 at 14:06):

right, this code is the content of the inner function fun _ => (f x.get).get

Mario Carneiro (Apr 22 2021 at 14:07):

and the model calls get twice, as you can see

Mario Carneiro (Apr 22 2021 at 14:07):

the implementation is actually doing fun _ => f x.get

Scott Viteri (Apr 22 2021 at 14:07):

and then why does this cause the segfault

Mario Carneiro (Apr 22 2021 at 14:08):

because it is violating the type system

Mario Carneiro (Apr 22 2021 at 14:08):

it returns a thunk and lean thinks it's a string

Scott Viteri (Apr 22 2021 at 14:08):

should it not be caught by the lean_assert

Mario Carneiro (Apr 22 2021 at 14:08):

so when it calls the string-print function on a thunk value, boom

Mario Carneiro (Apr 22 2021 at 14:09):

I don't think the asserts are air tight

Scott Viteri (Apr 22 2021 at 14:09):

Oh I see, the asserts are only called on f and t anyway

Mario Carneiro (Apr 22 2021 at 14:09):

Also bind doesn't have any asserts on entry, map does

Mario Carneiro (Apr 22 2021 at 14:10):

extern "C" obj_res lean_thunk_map(obj_arg f, obj_arg t) {
    lean_assert(lean_is_closure(f));
    lean_assert(lean_is_thunk(t));
    return mk_thunk_3_2(thunk_map_fn_closure, f, t);
}

extern "C" obj_res lean_thunk_bind(obj_arg x, obj_arg f) {
    return mk_thunk_3_2(thunk_bind_fn_closure, x, f);
}