is there a way to do lazy computation in lean

Stream: new members

[Shubham Kumar 🦀 (he/him)]

same as the title, I was looking at Json serializer and it use lazy

public export
orElse : Either a b -> Lazy (Either a b) -> Either a b
orElse r@(Right _) _ = r
orElse _           v = v

public export
(<|>) : Parser v a -> Parser v a -> Parser v a
f <|> g = \vv => f vv `orElse` g vv

is there something similar in lean?

[Kyle Miller]

docs#Thunk

[Shubham Kumar 🦀 (he/him)]

Ah thanks!!

[Kyle Miller]

Though that's if you want to save the result. If you just want a one-shot lazy value, you may as well use Unit -> a

[Shubham Kumar 🦀 (he/him)]

Kyle Miller said:

Though that's if you want to save the result. If you just want a one-shot lazy value, you may as well use Unit -> a

ok so it's similar to ocaml, got it

[Kyle Miller]

docs#HOrElse.hOrElse uses that

[Shubham Kumar 🦀 (he/him)]

this is giving me error

instance : HOrElse.hOrElse (Either α β) (Thunk.pure (Either α β)) where

It seems right to me but the compiler doesn't

[Shubham Kumar 🦀 (he/him)]

error: application type mismatch
  HOrElse.hOrElse (Either α β) (Thunk.pure (Either α β))
argument
  Thunk.pure (Either α β)
has type
  Thunk Type : Type 1
but is expected to have type
  Unit → ?m.1635 : Type ?u.1632

[Shubham Kumar 🦀 (he/him)]

created an either type and implemented hOrElse

def hOrElse
  {α β : Type}
  {a : Either α β}
  {b : Thunk (Either α β)}
  {c : Either α β}
  (e₁ : a) (f : b) : c :=
  match e₁, f with
  | Either.Right r, _ => Either.Right r
  | _, v => v

but I am getting an error where a has to be a type but is Either a b isn't Either a type if I have defined it as an inductive type

inductive Either (α β : Type) : Type
  | Left  : α -> Either α β
  | Right : β -> Either α β

[Eric Wieser]

Either is builtin, it's docs#Sum

[Shubham Kumar 🦀 (he/him)]

Oh ok, sorry. Thanks for the help :pray:

[Eric Wieser]

Shubham Kumar 🦀 (he/him) said:

I am getting an error where a has to be a type but is Either a b isn't Either a type

The error doesn't say "Either isn't a type", it says "a isn't a type".

[Eric Wieser]

Nat is a type and 37 is a Nat but 37 is not a type

[Eric Wieser]

Though give the orElse semantics you want, you might want docs#Except instead of Sum

[Kyle Miller]

Shubham Kumar 🦀 (he/him) said:

this is giving me error

instance : HOrElse.hOrElse (Either α β) (Thunk.pure (Either α β)) where

It seems right to me but the compiler doesn't

Here's a hint: move your mouse over HOrElse.hOrElse. What's its type? Is it actually a typeclass?