Em Haskell, costumo usar liftA2 em funções como o combinador S'. Isso funciona porque o Haskell STL instancia Functor e Applicative para funções (consulte https://hackage.haskell.org/package/base-4.12.0.0/docs/src/GHC.Base.html#line-818). Pelo que pude descobrir, o Idris STL não faz isso (além do fato de que também não consegui encontrar o liftA2 no STL), então pensei em fazer isso sozinho. Só que parece não funcionar, mas talvez eu não conheça Idris bem o suficiente, pois só tentei hoje.
Eu sou capaz de instanciar Functor e Applicative para \b => a -> b, mas o sistema de tipos não parece capaz de descobrir que quando eu uso algo do tipo a -> b, o functor do aplicativo deve ser \b => uma -> b.
Eu tenho o seguinte código:
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
Mas a definição de S' dá o seguinte erro:
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
^^^^^^
Se você nomear seu functor ou aplicativo como
[Foo] Functor ...
, chamá-lomap @{Foo}
pode funcionar, mas geralmente não é prático implementar e usar interfaces para funções no Idris. É possível, mas não é prático. Você poderia agrupar sua função em um tipo de dados fino e implementar functor e aplicativo para isso