{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Data.TypeNums.Rats
( Rat((:%))
, KnownRat
, ratVal
, ratVal'
) where
import Data.TypeNums.Equality (type (/=))
import Data.TypeNums.Ints
import Data.Ratio (Rational, (%))
import GHC.Exts (Proxy#, proxy#)
import GHC.TypeLits (ErrorMessage (..), KnownNat, Nat, TypeError, natVal')
data Rat = forall k. k :% Nat
newtype SRat r =
SRat Rational
class KnownRat r where
ratSing :: SRat r
instance {-# OVERLAPPING #-} (TypeError ('Text "Denominator must not equal 0")) =>
KnownRat (n ':% 0) where
ratSing = error "Unreachable"
instance {-# OVERLAPS #-} forall (n :: k) d. (KnownInt n, KnownNat d, d /= 0) =>
KnownRat (n ':% d) where
ratSing = SRat $! intVal' (proxy# @k @n) % natVal' (proxy# @Nat @d)
instance {-# OVERLAPPABLE #-} forall (n :: k). (KnownInt n) => KnownRat n where
ratSing = SRat $! intVal' (proxy# @k @n) % 1
ratVal ::
forall proxy r. KnownRat r
=> proxy r
-> Rational
ratVal _ =
case ratSing :: SRat r of
SRat x -> x
ratVal' ::
forall r. KnownRat r
=> Proxy# r
-> Rational
ratVal' _ =
case ratSing :: SRat r of
SRat x -> x