haskell - 为什么 (*3) `map` (+100) 在 Idris 中不起作用？

Question

在 Haskell 中，函数是仿函数，以下代码按预期工作:

(*3) `fmap` (+100) $ 1

输出当然是 303。但是，在 Idris(使用 fmap -> map)中，它给出了以下错误:

Can't find implementation for Functor (\uv => Integer -> uv)

对我来说，这似乎函数没有在 Idris 中实现为仿函数，至少不像在 Haskell 中那样，但这是为什么呢？

此外，类型签名 (\uv => Integer -> uv) 到底是什么？意思是？它看起来像一些部分应用的函数，这是仿函数实现所期望的，但语法有点困惑，特别是 \应该用于 lambda/literal 正在那里做。

Answer 1

仿函数是一个接口(interface)。在 Idris 中，实现仅限于数据或类型构造函数，即使用 data 定义。关键词。我不是依赖类型方面的专家，但我相信这个限制是必需的——至少实际上——对于一个健全的接口(interface)系统。
当您询问 \a => Integer -> a 的类型时在 REPL，你会得到

\a => Integer -> a : Type -> Type

在 Haskell 中，我们会认为这是一个真正的类型构造函数，可以将其制成类型类的实例，例如 Functor。 .然而，在 idris ， (->)不是类型构造函数，而是 binder .
最接近你在 idris 的例子是

((*3) `map` Mor (+100)) `applyMor` 1

使用 Data.Morphisms模块。或者一步一步:

import Data.Morphisms

f : Morphism Integer Integer
f = Mor (+100)

g : Morphism Integer Integer
g = (*3) `map` f

result : Integer
result = g `applyMor` 1

这是因为 Morphism是一个实型构造函数，带有 Functor库中定义的实现。