Pi as a functor

Stream: Type theory

[Snir Broshi]

For every type A, the function fun (B : Type) => A -> B is a functor, with the map operation being function composition. So I have a couple of questions about it:

1- Why doesn't Lean consider this as a functor (in stdlib)? Haskell does, which is very useful IMO

2- I tried manually defining a Functor instance for it, but it doesn't seem to work:

instance (A : Type) : Functor (fun (B : Type) => A -> B) where
  map := Function.comp

-- works:
#eval Function.comp id id 3
-- fails:
#eval Functor.map id id 3

(btw I'm asking here both because there's no channel for neither category theory nor functional programming, and also because universe issues seem to be related to this)

[Kenny Lau]

@loogle Functor

[loogle]

:search: Functor, Applicative.toFunctor, and 108 more

[Kenny Lau]

there are only 110 results with Functor so I don't think it's used a lot

[Kenny Lau]

do you really want it for functional programming, or are you asking about category theory in Mathlib?

[Kyle Miller]

Lean uses Reader to opt-in to using it as a functor/monad

[Aaron Liu]

The equivalent of the functor/monad in Haskell is Reader

[Snir Broshi]

Cool, how is it used?
I tried

#eval Functor.map id (id : ReaderM Nat Nat) 3

but it doesn't work

[Aaron Liu]

Instead of (id : ReaderM Nat Nat) you want (read : ReaderM Nat Nat)

[Aaron Liu]

-- 3
#eval (id <$> (read : ReaderM Nat Nat)).run 3

[Snir Broshi]

Thanks, weird that it fails without the type assertion.
Is there an easy way to convert A -> B to ReaderM A B? Or even better, a coercion?

[Kyle Miller]

The reason the id example fails is that type ascriptions aren't coercions (they only make sure that the type is definitionally equal to what it's supposed to be, not that the type will be structurally equal).

Amusingly, id can be used to "save" the type.

#eval Functor.map id (id id : ReaderM Nat Nat) 3

More idiomatically there's show, whose semantics are to make sure the type is structurally equal to what you say it is

#eval Functor.map id (show ReaderM Nat Nat from id) 3

[Aaron Liu]

Coercion would definitely be bad, but you can do

def funToReaderM.{u} {α β : Type u} (f : α → β) : ReaderM α β := f <$> read

[Kyle Miller]

Or there's using do and read

#eval Functor.map id (do return id (← read) : ReaderM Nat Nat) 3

[Kyle Miller]

Anyway, this is a contrived example; in practice you can pass a function to anything that expects specifically a ReaderM argument.

And also in practice you don't use the functor interface when ∘ will do

[Aaron Liu]

but I heard that defeq abuse is bad

[Snir Broshi]

Very weird, but seems to mostly work, although I definitely don't understand the rules which allow passing a function as a reader. Also, why does having an actual coercion for it in the standard library so bad?

[Snir Broshi]

Kyle Miller said:

Anyway, this is a contrived example; in practice you can pass a function to anything that expects specifically a ReaderM argument.

And also in practice you don't use the functor interface when ∘ will do

Are there equivalent operations defined on functions for fancier types of composition, like <*>? i.e. fun x => f x (g x)

[Aaron Liu]

You can use <*> for ReaderM and ReaderT

[Aaron Liu]

not for regular functions though

[Kyle Miller]

There might be an operator for the S combinator somewhere, but it's not really Lean style to use fancy compositions. Dependent types are hard enough, no need to tax the neurons with complicated combinators :-)

[Snir Broshi]

Yeah but that kinda defeats the short point-free writing style for functional programming.
Replacing fun x => f x (g x) with f <*> g is great, but if I have to instead use
((funToReaderM f) <*> (funToReaderM g))
then it defeats the purpose

[Kyle Miller]

The idea is that you'd work entirely with ReaderM, because that captures the idea of what you're doing (threading in an argument across multiple functions)

[Aaron Liu]

pointfree is great, but sometimes I lose track of where everything is going

[Snir Broshi]

I prefer not to swap functions in theorems for ReaderM (specifically I have a graph G on V, and I'd need a ReaderM V), but it's okay if proofs use fancy functional programming shenanigans

[Snir Broshi]

So it sounds like you both suggest ignoring the urge to swap an S combinator that appears in the wild with an actual <*>
I'll go with that, thank you!

[Kyle Miller]

I'd suggest also maybe not using any combinators, since that's just one more thing to unfold when proving things. Plain lambdas with actual variables tend to be easiest.

But it's too hard to speak about this in generalities. If you have some concrete code, it's probably worth taking a look.