fractions - 如何在 Idris 中使用分数？

Question

当我尝试将一个整数除以另一个整数时，我收到以下消息:

Idris> 6 / 8
Can't find implementation for Fractional Integer

这到底是什么意思？ 如何在 Idris 中使用有理数？

Answer 1

Idris does not have a built-in type for rational numbers.您看到的错误消息意味着 (/) 函数，它是 Fractional 的一个方法。接口(interface)，要求其参数是实现该接口(interface)的类型；但是，当前实现 Fractional 接口(interface)的唯一类型是 Double:

Idris> :doc Fractional
Interface Fractional

Parameters:
    ty

Constraints:
    Num ty

Methods:
    (/) : Fractional ty => ty -> ty -> ty

        infixl 9

        The function is Total
    recip : Fractional ty => ty -> ty


        The function is Total
Implementations:
    Fractional Double