Idiomatic way of proving things about Applicatives

Stream: lean4

[Brendan Seamas Murphy]

The definition of an Applicative in Lean is different from the one in Haskell, specifically the operator <*> is different. The type signature of Seq.seq is different than the type signature of <*>, in that it takes a thunk as its second argument. My understanding is that this is so that you don't waste time on big computations that won't be evaluated anyway (e.g. if you're in the Maybe monad) don't have time wasted on them. Additionally <*> is a more complicated sort of macro than a normal infix operator (this makes propositions involving <*>, e.g. the traversable laws, display with <*> expanded). These design choices make practical sense, but logically (in the precense of function extensionality) we have (Unit → α) ≃ α and so none of this should really matter when reasoning about Applicatives internal to Lean. Is therething I'm missing, or some way to avoid the pain point of <*> printing weirdly?

[Brendan Seamas Murphy]

I guess also it's not clear to me why Seq takes one thunk and one non-thunk argument, instead of having Seq.seq be derived from some more symmetric primitive Seq.seq' : {α β : Type u} → (Unit → f (α → β)) → (Unit → f α) → f β?

[Brendan Seamas Murphy]

Also, somewhat related, it seems like if you define a monad by just giving pure and bind and then want to prove that it's a lawful monad then you'll get some junk proof burdens about the applicative data that's just been derived from the given pure/bind. I might be missing something, but isn't requiring the user to prove seqLeft_eq totally redundant here?

[Kyle Miller]

Yes, Lean uses eager evaluation and Haskell uses lazy evaluation, which explains the practical difference in their types.

Brendan Seamas Murphy said:

I guess also it's not clear to me why Seq takes one thunk and one non-thunk argument, instead of having Seq.seq be derived from some more symmetric primitive Seq.seq' : {α β : Type u} → (Unit → f (α → β)) → (Unit → f α) → f β?

Seq always evaluates the first argument and it might evaluate the second, so there's no need for it to be symmetric. This operator is for writing programs, and making the first argument be Unit -> ... as well would just be giving the compiler more work to do to eliminate the function application.

[Kyle Miller]

Brendan Seamas Murphy said:

I might be missing something, but isn't requiring the user to prove seqLeft_eq totally redundant here?

I don't know what can be derived from what, but if you're able to prove it in general, you could add the proof as a default value for seqLeft_eq in the LawfulMonad definition, just like how it's done for map_pure etc.

[Brendan Seamas Murphy]

Seq does always evaluate the first argument, but that's exactly the design choice I'm asking about. Applicatives are completely symmetric, you can always reverse their internal evaluation order, so why assume in the type of Seq.seq that evaluation is occuring left to right?

[Kyle Miller]

Maybe for consistency with other operators like && which also evaluate left-to-right? It's also conceivable that they wanted to make sure the compiler didn't have to unfold Seq.seq and eliminate function applications before seeing how it sequences, similar to what I already suggested.

[Kyle Miller]

Re pretty printing of Seq.seq, that just seems to be an oversight.

[Kyle Miller]

To do it right takes a bit of work that hasn't been done yet. (You can write an app_unexpander that's right almost all the time, but it'd be good to make sure it really is always right.)

[Brendan Seamas Murphy]

&& was a good point of comparison, I didn't know about @[macro_inline]. Maybe I'll toy around with it and see if I can somehow modify <*> to be a @[macro_inline] operator which calls Seq.seq on a thunk without breaking anything. Thanks!

[Kyle Miller]

@Brendan Seamas Murphy If all you're wanting is nice pretty printing, then here's what's missing:

import Lean

section Delab
open Lean PrettyPrinter.Delaborator SubExpr

@[delab app.Seq.seq]
def delabSeq : Delab := whenPPOption Lean.getPPNotation do
  let #[_, _, _, _, _, thunk] := (← getExpr).getAppArgs | failure
  guard <| thunk.isLambda && !thunk.bindingBody!.hasLooseBVar 0
  let a ← withAppFn <| withAppArg delab
  let b ← withAppArg <| withBindingBody `_ delab
  `($a <*> $b)

@[delab app.SeqLeft.seqLeft]
def delabSeqLeft : Delab := whenPPOption Lean.getPPNotation do
  let #[_, _, _, _, _, thunk] := (← getExpr).getAppArgs | failure
  guard <| thunk.isLambda && !thunk.bindingBody!.hasLooseBVar 0
  let a ← withAppFn <| withAppArg delab
  let b ← withAppArg <| withBindingBody `_ delab
  `($a <* $b)

@[delab app.SeqRight.seqRight]
def delabSeqRight : Delab := whenPPOption Lean.getPPNotation do
  let #[_, _, _, _, _, thunk] := (← getExpr).getAppArgs | failure
  guard <| thunk.isLambda && !thunk.bindingBody!.hasLooseBVar 0
  let a ← withAppFn <| withAppArg delab
  let b ← withAppArg <| withBindingBody `_ delab
  `($a *> $b)

end Delab

-- Example
#print LawfulApplicative
/-
LawfulApplicative.mk : ∀ {f : Type u → Type v} [inst : Applicative f] [toLawfulFunctor : LawfulFunctor f],
  (∀ {α β : Type u} (x : f α) (y : f β), x <* y = Function.const β <$> x <*> y) →
    (∀ {α β : Type u} (x : f α) (y : f β), x *> y = Function.const α id <$> x <*> y) →
      (∀ {α β : Type u} (g : α → β) (x : f α), pure g <*> x = g <$> x) →
        (∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)) →
          (∀ {α β : Type u} (g : f (α → β)) (x : α), g <*> pure x = (fun h ↦ h x) <$> g) →
            (∀ {α β γ : Type u} (x : f α) (g : f (α → β)) (h : f (β → γ)),
                h <*> (g <*> x) = Function.comp <$> h <*> g <*> x) →
              LawfulApplicative f
-/

[Kyle Miller]

I just had it print LawfulApplicative as a test because it had all the operators

[Brendan Seamas Murphy]

Thanks, that's awesome! Should be much easier to read now

[Brendan Seamas Murphy]

Kyle Miller said:

Brendan Seamas Murphy said:

I might be missing something, but isn't requiring the user to prove seqLeft_eq totally redundant here?

I don't know what can be derived from what, but if you're able to prove it in general, you could add the proof as a default value for seqLeft_eq in the LawfulMonad definition, just like how it's done for map_pure etc.

I think the issue is that map_pure can be proven without knowing the actual definition of the Applicative structure, using bind_pure_comp and pure_bind, while the implementation I'm suggesting requires you to know that the Applicative structure was constructed using the defaults in the declaration of Monad. Maybe it could be an alternate constructor for LawfulMonad? I'm not clear enough on how the default implementation sugar actually works

[Eric Wieser]

Brendan Seamas Murphy said:

Also, somewhat related, it seems like if you define a monad by just giving pure and bind and then want to prove that it's a lawful monad then you'll get some junk proof burdens about the applicative data that's just been derived from the given pure/bind.

I think this is what docs#LawfulMonad.mk' is for

[Brendan Seamas Murphy]

!!! Tysm