How can I use fractions in Idris?

When I attempt to divide one integer by another, I get the following message:

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

What exactly does this mean? How can I use rational numbers in Idris?

Solution

Idris does not have a built-in type for rational numbers. The error message you are seeing means that the (/) function, which is a method of the Fractional interface, requires that its arguments be of a type that implements that interface; however, the only type that currently implements the Fractional interface is 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