Add casting implementations

src/Data/Ratio.idr

@@ -135,3 +135,18 @@ IntegralGCD a => Fractional (Ratio a) where
   recip (MkRatio n d) = case n /= 0 of True => MkRatio d n
   MkRatio n d / MkRatio m b = case m /= 0 of
     True => reduce $ MkRatio (n*b) (m*d)
+
+-- ## Casting
+
+export
+Num a => Cast a (Ratio a) where
+  cast x = MkRatio x 1
+
+export
+Cast a b => Cast (Ratio a) (Ratio b) where
+  cast (MkRatio n d) = MkRatio (cast n) (cast d)
+
+-- Special case: `Cast Rational Double`
+export
+(Cast a b, Fractional b) => Cast (Ratio a) b where
+  cast (MkRatio n d) = cast n / cast d