伊德里斯：订单/编号问题答案

【问题标题】：Idris: issue with Ord/Num伊德里斯：订单/编号问题
【发布时间】：2020-09-10 15:26:56
【问题描述】：

我有一个非常简单的示例，作为演示如何使用不进行类型检查的case _ of，我无法理解问题所在：

data ZeroOrSign = Zero | Pos | Neg

sign : Ord elem => elem -> ZeroOrSign
sign x = case compare x 0 of
            LT => Neg
            EQ => Zero
            GT => Pos

函数compare在Prelude、compare : Ord ty => ty -> ty -> Ordering中定义，其中Ordering只是LT、EQ和GT。我得到的错误如下：

When checking right hand side of sign with expected type
        ZeroOrSign

When checking an application of function Prelude.Interfaces.compare:
        Ord elem is not a numeric type

如果我尝试定义 sign : Num elem => elem -> ZeroOrSign，那么这当然会产生问题，因为 idris 找不到为 Num 类型定义的函数 compare。

我很疑惑，有什么提示吗？

【问题讨论】：

标签： idris

【解决方案1】：

compare 的类型要求 x 与 0 的类型*相同，但您尚未指定。试试

sign : (Ord elem, Num elem) => elem -> ZeroOrSign

* 或有适当的转换。我不太明白这是如何工作的，但Num 似乎就足够了，可能是因为fromInteger 将0 转换为elem 类型

【讨论】：

感谢这项工作。我是否正确理解 (Ord elem, Num elem) => 将 elem 的类型限制为序数和数字？
没错，见the docs