问题标签 [idris]

我试图在 Idris 中创建大小为 n 的元组：

但我在最后一行收到此错误：

有没有办法让这个功能发挥作用？

我正在 Idris 中编写一个基本的单子解析器，以适应 Haskell 的语法和差异。我有基本的工作正常，但我坚持尝试为解析器创建 VerifiedSemigroup 和 VerifiedMonoid 实例。

事不宜迟，这里是解析器类型、Semigroup 和 Monoid 实例，以及 VerifiedSemigroup 实例的开始。

我基本上被困在之后intros，具有以下证明者状态：

看起来我应该能够以某种方式rewrite一起使用appendAssociative，但我不知道如何“进入” lambda \s。

无论如何，我被困在练习的定理证明部分——而且我似乎找不到太多以 Idris 为中心的定理证明文档。我想也许我需要开始查看 Agda 教程（尽管 Idris 是我确信我想学习的依赖类型语言！）。

我有以下代码（主要是通过在 emacs 中使用 idris-mode 自动生成的）：

尝试将文件加载到 REPL (Cc Cl) 中时，我收到以下错误消息：

我想我做错了什么，但我不知道是什么。

根据我对依赖类型的了解，我认为这应该是可能的，但我以前从未见过依赖类型语言的例子，所以我不确定从哪里开始。

我想要的是表单的功能：

ETC...

此函数接受一个 n 列表Ints，并返回一个以 Ints 作为参数的元数 n 的谓词函数。这种事情在依赖类型语言中是可能的吗？这样的事情将如何实施？

我首先执行 cabal 更新/升级过程，所以我有 cabal-install-1.20.0.3。然后我做：

我得到：

（如果这很重要，我正在运行 OS X 10.9.4）

我是 emacs 的新手（来自 vim，我无法让 idris-vim 工作）并通过 el-get 安装了这些软件包：

我的 ~/.emacs.d/init.el 看起来像这样：

由于我使用的是 evil，并且 idris-mode 具有适用于 evil 的绑定，因此我尝试遵循 vim 的案例拆分示例。从新的会话开始，会发生以下情况：

1. 我打开 vadd.idr 文件，该文件已经包含 3 行（其中 1 行是空白的）。
2. 我移到最后一行并按\d。
3. 我收到一条很长的错误消息，在我阅读之前它就消失了。
4. Idris REPL 在新的拆分窗格中打开。
5. 命令行（在窗口底部）显示Buffer vadd.idr has no process. 我还尝试了 REPL，在插入模式下输入。按回车后，我得到Buffer *idris-repl* has no process，没有进一步的反应。

在 Linux shell 中，echo $PATH生成/home/james/bin /home/james/.cabal/bin /home/james/bin /usr/local/sbin /usr/local/bin /usr/bin /usr/bin/vendor_perl /usr/bin/core_perl，并按idris预期从 shell 工作。

退出 emacs 时（通过几个ZZs），我被告知存在活动进程。这是我显示的进程列表：

因为它可能已连接，所以这是我使用 idris-vim 从 vim 中的同一文件得到的错误：

我使用 ex 命令是因为领导绑定不起作用（我遇到的另一个问题）。

很抱歉提出这么长的问题。我想包括最相关的信息，即使这意味着添加不相关的东西。

编辑：更多；我找到了调试器（从菜单中设置“出错时输入调试器”）。

我按\d，然后在缓冲区中看到这个：

并在 ex 命令行中看到

我不知道它想做什么。

编辑：这是 vadd.idr 的缓冲区状态行的右端（正确的术语？）：

Not loaded看起来很担心，但我不知道更多。

编辑：回到 Vim 问题，我跑了

日志中的所有内容看起来都很正常，直到最后（由错误引起）：

所以，我发现日志文件包括

从 shell 运行这些 shell 命令，我得到：

顺便说一句， Plainidris vaddr.idr可以正常工作。

我目前正在通过cabal install idris. 响应输出：

我决定使用tail -f /home/me/.cabal/logs/idris-0.9.14.3.log.

虽然大部分输出是有意义的，但大致如下：

有很多行只包含

*** CPSZ:

因此，纯粹出于好奇，我想知道“ *** CPSZ:”代表什么。

在 Idris 中，Vect n a是一个数据类型，表示一个长度为 n 的向量，其中包含类型 a 的项。想象一下我有一个功能：

函数的主体并不重要，它可以是任何返回 4 个 Ints 的向量的东西。现在，我想将此函数与 concatMap 一起使用，如下所示：

Bar 是一个函数，它接受长度为 n 的 Int 向量并返回长度为 4*n 的向量。

concatMap 的类型签名是：

因此，如果我尝试编译 bar，我会收到错误消息：

这意味着 Vect n Int 不是幺半群的实例。为了使它成为一个幺半群的实例，我需要实现：

不幸的是，我不确定如何做到这一点。List实现了monoid，如下：

但是，如果我尝试为 Vect n Int 实现带有中性 = [] 的幺半群，我会收到错误消息：

所以我想知道，我将如何为 Vect 实现幺半群？

到目前为止，我所拥有的是：

但是在尝试加载文件时，我得到：

对这个错误有点惊讶，因为我认为 Idris 具有异构的“John Major”相等性，在 = 的左侧和右侧使用不同的类型很好。现在有一个不同的符号？

我们如何在函数中使用隐式变量？减少到最简单的情况，是否有可能：

没有得到错误：

有没有办法从内部访问那里的值？还是和要求ninside一样sin n？

在这种情况下，是否有可能证明这Vect是一个“双射”并从那里恢复变量？