Awesome stuff

Stream: general

[Simon Hudon]

My mind was just blown by how useful has_coe_to_fun is. I constructed a morphism between applicative functors:

variables (f : Type u → Type v) [applicative f]
variables (g : Type u → Type w) [applicative g]

structure applicative_morphism : Type (max (u+1) v w) :=
  (F : ∀ {α : Type u}, f α → g α)
  (preserves_pure' : ∀ {α : Type u} (x : α), F (pure x) = pure x)
  (preserves_seq' : ∀ {α β : Type u} (x : f (α → β)) (y : f α), F (x <*> y) = F x <*> F y)

and defined the following instance:

instance : has_coe_to_fun (applicative_morphism f g) :=
{ F := λ _, ∀ {α}, f α → g α,
  coe := λ m, m.F }

It's already pretty cool that, given x : f int and m : applicative_morphism f g I can write f x to just apply it. What really blew my mind is that I can write @f int x to make the {α : Type u} of F explicit.