Seq.seq on an Option

Stream: lean4

[Chris Lovett]

can someone give me a simple example of implementing Seq.seq on an Option? I'm a bit surprised the while Option is a Monad (instance : Monad Option where...), seq does not seem to be defined:

image.png

[Mario Carneiro]

seq is not an exported name, you have to use Seq.seq

[Mario Carneiro]

or <*>

[Chris Lovett]

Ha, but pure is ?

def fred : Option Nat :=
  pure 5

#eval fred -- some 5

[Mario Carneiro]

yes

[Mario Carneiro]

if you look in the prelude file you will find export Pure (pure)

[Mario Carneiro]

which basically means it's open for everyone

[Mario Carneiro]

This has nothing to do with Option or the way the monad is defined BTW

[Mario Carneiro]

if you are wondering why src4#instMonadOption does not declare a seq field, it's because there is a default implementation of seq in terms of bind and map in src4#Monad

[Chris Lovett]

So where is the seq defined for Option? I see the type class:

class Seq (f : Type u → Type v) : Type (max (u+1) v) where
  seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β

But when the Option Monad instance is defined there is no seq := ... filling in the Option specific implementation so what happens?

[Chris Lovett]

Ah thanks you just answered my question...

[Chris Lovett]

So how would I port something like this from Haskell using Option instead of Maybe:

pure (*) <*> Just 4 <*> Just 5        -- Just 20

[Chris Lovett]

Never mind, I got it:

#eval pure Mul.mul <*> some 4 <*> some 5

[Leonardo de Moura]

#eval pure (·*·) <*> some 4 <*> some 5 -- some 20
#eval pure (.*.) <*> some 4 <*> some 5 -- some 20

[Leonardo de Moura]

For more information about the (·*·). https://leanprover.github.io/functional_programming_in_lean/getting-to-know/conveniences.html#anonymous-functions

[Leonardo de Moura]

https://leanprover.github.io/lean4/doc/functions.html#syntax-sugar-for-simple-lambda-expressions

[Chris Lovett]

Yep thanks, I remember (. * .) from that chapter.

[Mario Carneiro]

Usually, we would use <$> for the first application there to avoid the pure

[Mario Carneiro]

#eval (.*.) <$> some 4 <*> some 5 -- some 20

[Chris Lovett]

Oh, much nicer, thanks! I was pretty confused about using pure on a function (.*.) ...

[Chris Lovett]

Looking at seq f x := bind f fun y => Functor.map y (x ()) why does x take () as input, making my example more combersome:

#eval Seq.seq ((.*.) <$> (some 4)) (fun _ : Unit => (some 5)) -- some 20

only to have the infix notation invent that required function:

@[inheritDoc] notation:60 a:60 " <*> " b:61 => Seq.seq a fun _ : Unit => b

so I can write the lovely clean:

#eval pure (·*·) <*> some 4 <*> some 5

?

[Mario Carneiro]

Because lean is an eagerly evaluated language (call-by-value), you have to use Unit -> functions whenever you want to explicitly delay evaluation

[Mario Carneiro]

So the idea here is that we want f <*> long_running x to not evaluate long_running x unless the evaluation of seq determines that it is necessary

[Mario Carneiro]

For example, if we are working over Option, we want none <*> some (long_running x) to not evaluate long_running x at all

[Chris Lovett]

Interesting thanks.

[Chris Lovett]

Stuck on the next sample following the same pattern, this time on List:

#eval (.*.) <$> [1, 2, 3] <*> [4, 5, 6]   -- failed to synthesize instance Seq List

[Mario Carneiro]

There is (currently) no Monad List instance. You will have to provide one yourself if you want to use it in examples

[Mario Carneiro]

see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/List.20Functor

[Chris Lovett]

Hey this stuff is very slowly starting to make sense... I got the sample from mmhaskell working using this:

instance : Applicative List where
  pure := List.pure
  seq f x := List.bind f fun y => Functor.map y (x ())

#eval [(· +2), (· *3)] <*> [4, 6] -- [6, 8, 12, 18]

[Mario Carneiro]

It's presumably easier to just make an instance of Monad List using List.bind and List.pure and then the seq will get automatically filled in

[Chris Lovett]

True but then the chapter is jumping ahead to monads... it is supposed to be building up to Monads :-) But it's tempting - especially since it avoids the awkward delayed function execution trick with x ().

[Chris Lovett]

Does Lean Applicative obey the Interchange law:

-- Interchange
u <*> pure y = pure ($ y) <*> u

if so now do I write an example of this using my applicative list or Option ? I'm not sure what the Haskell syntax $ y means... and I'm not sure our <*> can put the function u on the right hand side like this can it?

[Chris Lovett]

Perhaps this is an example of interchange?

#eval pure (·+·) <*> [1, 2] <*> [3, 4] -- [4, 5, 5, 6]
#eval pure (·+·) <*> [3, 4] <*> [1, 2] -- [4, 5, 5, 6]

[Mario Carneiro]

Does Lean Applicative obey the Interchange law

No. Lean's Applicative doesn't obey any laws, really (that's what LawfulApplicative et al are for), but even then we do not generally assume this property for lawful applicatives. Applicatives that do have this property are called commutative IIRC

[Mario Carneiro]

and List is not commutative

[Mario Carneiro]

The haskell syntax ($ y) is equivalent to (. y) in lean, i.e. fun f => f y

[Mario Carneiro]

Option is commutative, as is Multiset ( = List quotient by permutation)

[Mario Carneiro]

Actually I take it back. The interchange law takes one side or the other to be a pure, in which case it is true for any lawful applicative because both sides are equivalent to the map expression (· y) <$> u

[Mario Carneiro]

example [Applicative m] [LawfulApplicative m] (u : m (α → β)) (y : α) :
  u <*> pure y = pure (· y) <*> u := by simp [pure_seq]

[Mario Carneiro]

Commutativity for applicatives says you can reorder effects, like this:

class CommApplicative (m) [Applicative m] where
  comm (x : m (α → β)) (y : m α) : x <*> y = flip id <$> y <*> x

[Chris Lovett]

Should we add this to LawfulApplicative ?

[Reid Barton]

No, this is an additional property which usually does not hold