In Haskell I am wont to use liftA2 on functions as the S' combinator. This works because the Haskell STL instantiates Functor and Applicative for functions (see https://hackage.haskell.org/package/base-4.12.0.0/docs/src/GHC.Base.html#line-818). As far as I could find, the Idris STL does not do this (besides the fact that I also couldn't find liftA2 in the STL), so I thought I'd do it myself. Only, it doesn't seem to work, but maybe I don't know Idris well enough, as I only first tried it today.
I am able to instantiate Functor and Applicative for \b => a -> b, but the typesystem does not seem able to figure out that when I use something of type a -> b, that the applicative functor is supposed to be \b => a -> b.
I have the following code:
Functor (\b => a -> b) where
map = (.)
Applicative (\b => a -> b) where
pure = const
(<*>) f g x = f x (g x)
liftA2 : (Functor f, Applicative f) => (a -> b -> c) -> f a -> f b -> f c
liftA2 = (<*>) .: map
S' : (b -> c -> d) -> (a -> b) -> (a -> c) -> a -> d
S' = liftA2
But the definition of S' gives the following error:
Error: While processing right hand side of S'. Can't find an implementation for (Functor ?f, Applicative ?f).
Helpers:16:6--16:12
12 | liftA2 : (Functor f, Applicative f) => (a -> b -> c) -> f a -> f b -> f c
13 | liftA2 = (<*>) .: map
14 |
15 | S' : (b -> c -> d) -> (a -> b) -> (a -> c) -> a -> d
16 | S' = liftA2
^^^^^^
If you name your functor or applicative, like [Foo] Functor ..., then call it with map @{Foo} it might work, but generally it's not practical to implement and use interfaces for functions in Idris. It's possible but not practical. You could wrap your function in a thin data type and implement functor and applicative for that