时间戳

首页 > 解决方案 > 为什么 (*3) `map` (+100) 在 Idris 中不起作用？

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

问题描述

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

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

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

找不到实现Functor (\uv => Integer -> uv)

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

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

标签： haskellidris

解决方案

函子是一个接口。在 Idris 中，实现仅限于数据或类型构造函数，即使用data关键字定义。我不是依赖类型方面的专家，但我相信这个限制是必需的——至少实际上——对于一个健全的接口系统。

\a => Integer -> a当您在 REPL询问类型 时，您会得到

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

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

最接近你在伊德里斯的例子是

((*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在库中定义了一个实现。

推荐阅读