Idris中无法将函数用作applicative functor？问题求助

你的问题核心是Idris的类型推断无法自动识别liftA2需要绑定的函子实例——也就是你定义的(\b => a -> b)类型构造器。Haskell的类型类推断在处理高阶函子时更宽松，但Idris需要更明确的提示，以下是两种可行的解决方式：

方法一：用类型同义词简化类型构造器 #

先把匿名的函数类型构造器定义成更清晰的类型同义词，让Idris更容易匹配实例：

-- 定义Reader类型同义词，对应a -> b的函数类型
Reader : Type -> Type -> Type
Reader a b = a -> b

-- 为Reader a实现Functor实例
Functor (Reader a) where
  map = (.)

-- 为Reader a实现Applicative实例
Applicative (Reader a) where
  pure = const
  (<*>) f g x = f x (g x)

-- 通用liftA2定义不变
liftA2 : (Functor f, Applicative f) => (a -> b -> c) -> f a -> f b -> f c
liftA2 = (<*>) .: map

-- 显式指定S'使用Reader a作为函子
S' : (b -> c -> d) -> Reader a b -> Reader a c -> Reader a d
S' = liftA2

这样修改后，Idris能直接通过Reader a的类型签名找到对应的Functor和Applicative实例，不会再出现推断失败的错误。

方法二：显式指定liftA2的隐式函子参数 #

如果你不想引入类型同义词，可以用Idris的@符号显式传递liftA2需要的隐式函子参数，直接告诉编译器要使用哪个实例：

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

-- 用@符号指定隐式参数f为(\b => a -> b)
S' : (b -> c -> d) -> (a -> b) -> (a -> c) -> a -> d
S' = liftA2 @(\b => a -> b)

原理说明 #

Idris的隐式参数推断不会自动回溯高阶类型构造器的实例，尤其是当函子是依赖于其他类型参数（比如这里的a）的匿名构造器时，必须通过类型同义词或显式参数传递的方式，给编译器明确的实例匹配线索。而Haskell的类型推断在处理函数类型这类常见的Applicative实例时做了特殊优化，所以不需要额外提示。

你可以测试一下修改后的S'：

-- 测试：输入5时，计算(5*2)+(5+3)=18
test : Int -> Int
test = S' (\x y => x + y) (\x => x * 2) (\x => x + 3)

内容的提问来源于stack exchange，提问作者Joris KBos