Comment puis-je utiliser des fractions dans Idris?

Question

Lorsque je tente de diviser un entier par un autre, je reçois le message suivant:

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

Qu'est-ce que cela signifie exactement? Comment puis-je utiliser des nombres rationnels dans Idris?

Answer 1

Idris does not have a built-in type for rational numbers. Le message d'erreur que vous voyez signifie que la fonction (/), qui est une méthode de l'interface Fractional, exige que ses arguments soient d'un type qui implémente cette interface; cependant, le seul type qui implémente actuellement l'interface Fractional est 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