Idris：不能将函数用作应用函子吗？

Question

在 Haskell 中，我习惯在函数上使用 liftA2 作为 S' 组合器。这是有效的，因为 Haskell STL 实例化了函数的 Functor 和 Applicative（请参阅 https://hackage.haskell.org/package/base-4.12.0.0/docs/src/GHC.Base.html#line-818）。据我所知，Idris STL 并没有这样做（除了我在 STL 中也找不到 liftA2 的事实），所以我想我应该自己做。只是，它似乎不起作用，但也许我对伊德里斯不够了解，因为我今天才第一次尝试。

我能够实例化 Functor 和 Applicative for => a -> b，但是类型系统似乎无法弄清楚当我使用 a -> b 类型的东西时，applicative functor 应该是 = > a -> b。

我有以下代码：

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

但是S'的定义给出了以下错误：

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
           ^^^^^^

Answer 1

如果您命名函子或应用程序，例如

[Foo] Functor ...

，然后用

map @{Foo}

调用它，它可能会起作用，但通常在 Idris 中实现和使用函数接口是不切实际的。这是可能的，但不切实际。您可以将函数包装在瘦数据类型中，并为此实现函子和应用程序