when args argue inhabited

Stream: lean4

[James Gallicchio]

is there a way to get something like this to compile?

partial def foldl [mi: Monad m] [ai: Alternative m] (base : γ) (rightCont : γ → m γ) : m γ :=
  (do let base' ← rightCont base; foldl base' rightCont) <|> (pure base)

The argument base justifies the type is inhabited, with pure base as its element.

[Adam Topaz]

(deleted)

[Adam Topaz]

sorry, forgot the recursion. I'll fix it in a few mins

[Adam Topaz]

oh nevermind, using ascii art gives the same issues

[Adam Topaz]

But this works for some reason:

partial def foldl [Monad m] [Alternative m] [Inhabited γ] (base : γ) (rightCont : γ → m γ) : m γ :=
  (rightCont base >>= fun b => foldl b rightCont) <|> (pure base)

[Adam Topaz]

(it also works with do)

[James Gallicchio]

I think that's from the [Inhabited γ] argument

[James Gallicchio]

which is what I'm trying to avoid

[Gabriel Ebner]

Check set_option trace.Meta.synthInstance true

[Gabriel Ebner]

I believe the partial command searches for Nonempty (full function type) as well.

[James Gallicchio]

It does look for Inhabited ([mi : Monad m] → [ai : Alternative m] → γ → (γ → m γ) → m γ), but tc synth can't instantiate it, it seems

[James Gallicchio]

(I wouldn't expect it to, either)

[James Gallicchio]

Frankly I am pretty okay if this doesn't work fully automatically -- the more annoying thing is that there's no way for me to provide the Nonempty (full function type) instance for it to use.

[James Gallicchio]

(other than by making a global instance right before the def)

[James Gallicchio]

I guess I can do this:

instance : Inhabited ([mi : Monad m] → [ai : Alternative m] → γ → (γ → m γ) → m γ) := ⟨λ g _ => pure g⟩ in
partial def foldl [mi: Monad m] [ai: Alternative m] (base : γ) (rightCont : γ → m γ) : m γ :=
  (do let base' ← rightCont base; foldl base' rightCont) <|> (pure base)

[James Gallicchio]

so that the instance doesn't escape scope... but then I'm a bit annoying that I have to copy/paste the type there.

[James Gallicchio]

But that works for me for now. Thanks!

[Gabriel Ebner]

You can do local instance, but you still need to retype the type.

[Gabriel Ebner]

Instance .. in is a big foot gun

[Gabriel Ebner]

It means exactly the same as instance without the in.

[Gabriel Ebner]

Another gotcha is private instance.

[Adam Topaz]

How about this?

partial def foldl_aux [Monad m] [Alternative m] [Inhabited γ] (base : γ) (rightCont : γ → m γ) : m γ :=
  (rightCont base >>= fun b => foldl_aux b rightCont) <|> (pure base)

partial def foldl [Monad m] [Alternative m] (base : γ) (rightCont : γ → m γ) : m γ :=
  letI : Inhabited γ := ⟨base⟩
  foldl_aux base rightCont

[Adam Topaz]

I tried to put Inhabited somewhere inline within foldl, but couldn't get it to work. Maybe Gabriel knows some other tricks?

[Adam Topaz]

Oh this works:

partial def foldl [Monad m] [Alternative m] (base : γ) (rightCont : γ → m γ) : m γ :=
  let rec go [_h : Inhabited γ] (bs : γ) (rc : γ → m γ) : m γ :=
    (rc bs >>= fun b => go b rc) <|> (pure bs)
  go (_h := ⟨base⟩) base rightCont

[Adam Topaz]

using where also works:

partial def foldl [Monad m] [Alternative m] (base : γ) (rightCont : γ → m γ) : m γ :=
  go (_h := ⟨base⟩) base rightCont
  where go [_h : Inhabited γ] (bs : γ) (rc : γ → m γ) : m γ :=
    (rc bs >>= fun b => go b rc) <|> (pure bs)

[Gabriel Ebner]

I would recommend

instance [Alternative m] : Nonempty (m α) := ⟨failure⟩

partial def foldl [Monad m] [Alternative m] (base : γ) (rightCont : γ → m γ) : m γ :=
  (do let base' ← rightCont base; foldl base' rightCont) <|> (pure base)

[Gabriel Ebner]

Even if you don't have Alternative, then you can still get away without writing the precise function type twice:

local instance : Nonempty (α → (α → β) → β) := ⟨(· |> ·)⟩ in
partial def foldl' [Monad m] (base : γ) (rightCont : γ → m γ) : m γ := do
  foldl' (← rightCont base) rightCont

[James Gallicchio]

hm, okay