令人惊讶的伊德里斯统一失败 [英] Surprising failure of unification in Idris

问题描述

我正在尝试使人们可以称之为Idris中可判定的解析器.起初，我只是在分析自然数，但是遇到了意外的问题.产生它的代码的最小示例是:

I'm trying to make what one might call a decidable parser in Idris. At first I am just looking at parsing natural numbers, but have ran into an unexpected problem. A minimum example of the code that produces it is this:

data Digit : Char -> Type where
  Zero  : Digit '0'
  One   : Digit '1'

digitToNat : Digit a -> Nat
digitToNat Zero  = 0
digitToNat One   = 1

natToChar : Nat -> Char
natToChar Z = '0'
natToChar (S Z) = '1'

natToDigit : (n : Nat) -> Digit (natToChar n)
natToDigit Z = Zero
natToDigit (S Z) = One

我希望它可以编译，但是我得到了

I would expect this to compile, but instead I get

When elaborating right hand side of natToDigit:
Can't unify
        Digit '0'
with
        Digit (natToChar 0)

Specifically:
        Can't unify
                '0'
        with
                natToChar 0

但是natToChar 0显然等于'0'，所以我不明白这里是什么问题.

But natToChar 0 clearly equals '0', so I don't understand what the problem here is.

更新

我还问了一个与我正在尝试做的事情直接相关的问题

I have also asked a question more directly related to what I am trying to do here.

推荐答案

类型检查器不会减少natToChar，因为它不是总计的-基本上是为了防止您使用部分定义的函数来证明某些不正确的内容.是真的.

The type checker won't reduce natToChar because it isn't total - this is basically to prevent you using some partially defined function to prove something which isn't true.

如果您正在编写此代码以处理在运行时出现的数据，则可能需要的是Dec或Maybe:

If you're writing this to work on data which turns up at run-time, possibly what you need is Dec or Maybe:

natToChar : (n : Nat) -> Maybe Char

这篇关于令人惊讶的伊德里斯统一失败的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！