{-|
Module      : Data.Default.Singletons
Description : Provides singleton-based default values and optional types.
Copyright   : (c) 2024, Eitan Chatav
License     : MIT
Maintainer  : eitan.chatav@gmail.com
Stability   : experimental
Portability : non-portable (GHC extensions)

This module defines an `Opt`ional type with
either a `Def`ault promoted value type,
or `Some` specific demoted value term.

>>> definite (Def :: Opt True)
True
>>> definite (Some False :: Opt (def :: Bool))
False
>>> definite (Some True :: Opt False)
True
>>> maybe "def" show (perhaps (Def :: Opt True))
"def"
>>> maybe "def" show (perhaps (Some True :: Opt True))
"True"
>>> maybe "def" show (perhaps (Some False :: Opt True))
"False"

The correspondence between promoted datakinds
and demoted datatypes is inexact.
Usually, `Demote` @t ~ t@, but not always such as:

>>> :kind! Demote Symbol
Demote Symbol :: *
= Text

Because there is no promoted `Integer` and `Rational` datakinds in base,
this module defines them as `Z` and `Q`.

>>> :kind! Demote Z
Demote Z :: *
= Integer
>>> :kind! Demote Q
Demote Q :: *
= Ratio Integer

The `Opt` type comes with
`Num`, `Integral`, `Fractional`, and `Real` instances,
using `definite` values to do arithmetic,
which let you use literals and arithmetic to construct
`Some` specific `Opt` value;

>>> 4 :: Opt 20
Some 4
>>> (Def + 0) * 1 :: Opt (Pos 8 :: Z)
Some 8
>>> 0.5 + Def :: Opt (Neg 1 % 3 :: Q)
Some (1 % 6)

and `IsString` and `IsList` instances.

>>> "text" :: Opt ("abc" :: Symbol)
Some "text"
>>> "string" :: Opt (['a','b','c'] :: String)
Some "string"
>>> [[1, 2],[3,4]] :: Opt ('[] :: [[Natural]])
Some [[1, 2],[3,4]]

`Opt` is a `Monoid` which yields
the leftmost specific value when there are `Some`,
and the `Def`ault value when there are none.

>>> definite (mempty :: Opt "xyz")
"xyz"
>>> definite (Def <> "abc" <> "qrs" <> Def :: Opt "xyz")
"abc"

You can use `Opt` as an optional function argument.

>>> :{
greet :: Opt "Anon" -> Text
greet name = "Welcome, " <> definite name <> "."
:}
>>> greet "Sarah"
"Welcome, Sarah."
>>> greet Def
"Welcome, Anon."

Or, you can use `Opt` as an optional field in your record type.

>>> :{
data Person = Person
  { name :: Text
  , age :: Natural
  , alive :: Opt (True :: Bool)
  }
:}
>>> let isAlive person = definite (alive person)
>>> let jim = Person {name = "Jim", age = 40, alive = Def}
>>> isAlive jim
True

You almost never need to include the datakind in your
type signatures since it's usually inferrable from @def@.

-}

{-# LANGUAGE
ConstraintKinds
, DataKinds
, FlexibleContexts
, FlexibleInstances
, GADTs
, LambdaCase
, PolyKinds
, RankNTypes
, ScopedTypeVariables
, StandaloneDeriving
, TypeApplications
, TypeFamilies
, TypeOperators
, UndecidableInstances
#-}

module Data.Default.Singletons
  ( -- | Optional Datatype
    Opt (..)
  , SingDef
  , optionally
  , definite
  , perhaps
    -- | Promoted Datakinds
  , Z (..)
  , Neg
  , Q (..)
  , type (%)
  , type Reduce
  , type GCD
  , SInteger (..)
  , SRational (..)
    -- | Reexport Demote
  , demote
  , type Demote
  ) where

import Control.Applicative
import Data.Default.Class
import GHC.IsList
import Data.Ratio
import GHC.TypeLits
import Data.Singletons
import Data.String
import Prelude.Singletons ()

{- |
`Opt`ional type with
either a `Def`ault promoted value @def@,
or `Some` specific `Demote`d value.
-}
data Opt (def :: k) where
  Def :: forall {k} def. SingDef def => Opt (def :: k)
  Some :: forall {k} def. Demote k -> Opt (def :: k)

{- | Constraint required to `demote` @@def@. -}
type SingDef (def :: k) = (SingI def, SingKind k)

instance Semigroup (Opt (def :: k)) where
  Opt def
Def <> :: Opt def -> Opt def -> Opt def
<> Opt def
opt = Opt def
opt
  Some Demote k
x <> Opt def
_ = Demote k -> Opt def
forall {k} (def :: k). Demote k -> Opt def
Some Demote k
x

instance SingDef def => Monoid (Opt def) where
  mempty :: Opt def
mempty = Opt def
forall k (def :: k). SingDef def => Opt def
Def

deriving instance (SingDef def, Show (Demote k))
  => Show (Opt (def :: k))

deriving instance (SingDef def, Read (Demote k))
  => Read (Opt (def :: k))

deriving instance (SingDef def, Eq (Demote k))
  => Eq (Opt (def :: k))

deriving instance (SingDef def, Ord (Demote k))
  => Ord (Opt (def :: k))

instance SingDef def
  => Default (Opt (def :: k)) where def :: Opt def
def = Opt def
forall k (def :: k). SingDef def => Opt def
Def

instance Num (Demote k)
  => Num (Opt (def :: k)) where
    Opt def
x + :: Opt def -> Opt def -> Opt def
+ Opt def
y = Demote k -> Opt def
forall {k} (def :: k). Demote k -> Opt def
Some (Demote k -> Opt def) -> Demote k -> Opt def
forall a b. (a -> b) -> a -> b
$ Opt def -> Demote k
forall {k} (def :: k). Opt def -> Demote k
definite Opt def
x Demote k -> Demote k -> Demote k
forall a. Num a => a -> a -> a
+ Opt def -> Demote k
forall {k} (def :: k). Opt def -> Demote k
definite Opt def
y
    Opt def
x * :: Opt def -> Opt def -> Opt def
* Opt def
y = Demote k -> Opt def
forall {k} (def :: k). Demote k -> Opt def
Some (Demote k -> Opt def) -> Demote k -> Opt def
forall a b. (a -> b) -> a -> b
$ Opt def -> Demote k
forall {k} (def :: k). Opt def -> Demote k
definite Opt def
x Demote k -> Demote k -> Demote k
forall a. Num a => a -> a -> a
* Opt def -> Demote k
forall {k} (def :: k). Opt def -> Demote k
definite Opt def
y
    abs :: Opt def -> Opt def
abs Opt def
x = Demote k -> Opt def
forall {k} (def :: k). Demote k -> Opt def
Some (Demote k -> Opt def) -> Demote k -> Opt def
forall a b. (a -> b) -> a -> b
$ Demote k -> Demote k
forall a. Num a => a -> a
abs (Opt def -> Demote k
forall {k} (def :: k). Opt def -> Demote k
definite Opt def
x)
    signum :: Opt def -> Opt def
signum Opt def
x = Demote k -> Opt def
forall {k} (def :: k). Demote k -> Opt def
Some (Demote k -> Opt def) -> Demote k -> Opt def
forall a b. (a -> b) -> a -> b
$ Demote k -> Demote k
forall a. Num a => a -> a
signum (Opt def -> Demote k
forall {k} (def :: k). Opt def -> Demote k
definite Opt def
x)
    fromInteger :: Integer -> Opt def
fromInteger Integer
x = Demote k -> Opt def
forall {k} (def :: k). Demote k -> Opt def
Some (Demote k -> Opt def) -> Demote k -> Opt def
forall a b. (a -> b) -> a -> b
$ Integer -> Demote k
forall a. Num a => Integer -> a
fromInteger Integer
x
    negate :: Opt def -> Opt def
negate Opt def
x = Demote k -> Opt def
forall {k} (def :: k). Demote k -> Opt def
Some (Demote k -> Opt def) -> Demote k -> Opt def
forall a b. (a -> b) -> a -> b
$ Demote k -> Demote k
forall a. Num a => a -> a
negate (Opt def -> Demote k
forall {k} (def :: k). Opt def -> Demote k
definite Opt def
x)
    Opt def
x - :: Opt def -> Opt def -> Opt def
- Opt def
y = Demote k -> Opt def
forall {k} (def :: k). Demote k -> Opt def
Some (Demote k -> Opt def) -> Demote k -> Opt def
forall a b. (a -> b) -> a -> b
$ Opt def -> Demote k
forall {k} (def :: k). Opt def -> Demote k
definite Opt def
x Demote k -> Demote k -> Demote k
forall a. Num a => a -> a -> a
- Opt def -> Demote k
forall {k} (def :: k). Opt def -> Demote k
definite Opt def
y

instance Fractional (Demote k)
  => Fractional (Opt (def :: k)) where
    recip :: Opt def -> Opt def
recip Opt def
x = Demote k -> Opt def
forall {k} (def :: k). Demote k -> Opt def
Some (Demote k -> Opt def) -> Demote k -> Opt def
forall a b. (a -> b) -> a -> b
$ Demote k -> Demote k
forall a. Fractional a => a -> a
recip (Opt def -> Demote k
forall {k} (def :: k). Opt def -> Demote k
definite Opt def
x)
    Opt def
x / :: Opt def -> Opt def -> Opt def
/ Opt def
y = Demote k -> Opt def
forall {k} (def :: k). Demote k -> Opt def
Some (Demote k -> Opt def) -> Demote k -> Opt def
forall a b. (a -> b) -> a -> b
$ Opt def -> Demote k
forall {k} (def :: k). Opt def -> Demote k
definite Opt def
x Demote k -> Demote k -> Demote k
forall a. Fractional a => a -> a -> a
/ Opt def -> Demote k
forall {k} (def :: k). Opt def -> Demote k
definite Opt def
y
    fromRational :: Rational -> Opt def
fromRational Rational
x = Demote k -> Opt def
forall {k} (def :: k). Demote k -> Opt def
Some (Demote k -> Opt def) -> Demote k -> Opt def
forall a b. (a -> b) -> a -> b
$ Rational -> Demote k
forall a. Fractional a => Rational -> a
fromRational Rational
x

instance IsString (Demote k)
  => IsString (Opt (def :: k)) where
    fromString :: String -> Opt def
fromString String
x = Demote k -> Opt def
forall {k} (def :: k). Demote k -> Opt def
Some (Demote k -> Opt def) -> Demote k -> Opt def
forall a b. (a -> b) -> a -> b
$ String -> Demote k
forall a. IsString a => String -> a
fromString String
x

instance IsList (Demote k)
  => IsList (Opt (def :: k)) where
    type Item (Opt (def :: k)) = Item (Demote k)
    fromList :: [Item (Opt def)] -> Opt def
fromList [Item (Opt def)]
xs = Demote k -> Opt def
forall {k} (def :: k). Demote k -> Opt def
Some (Demote k -> Opt def) -> Demote k -> Opt def
forall a b. (a -> b) -> a -> b
$ [Item (Demote k)] -> Demote k
forall l. IsList l => [Item l] -> l
fromList [Item (Demote k)]
[Item (Opt def)]
xs
    fromListN :: Int -> [Item (Opt def)] -> Opt def
fromListN Int
n [Item (Opt def)]
xs = Demote k -> Opt def
forall {k} (def :: k). Demote k -> Opt def
Some (Demote k -> Opt def) -> Demote k -> Opt def
forall a b. (a -> b) -> a -> b
$ Int -> [Item (Demote k)] -> Demote k
forall l. IsList l => Int -> [Item l] -> l
fromListN Int
n [Item (Demote k)]
[Item (Opt def)]
xs
    toList :: Opt def -> [Item (Opt def)]
toList Opt def
x = Demote k -> [Item (Demote k)]
forall l. IsList l => l -> [Item l]
toList (Demote k -> [Item (Demote k)]) -> Demote k -> [Item (Demote k)]
forall a b. (a -> b) -> a -> b
$ Opt def -> Demote k
forall {k} (def :: k). Opt def -> Demote k
definite Opt def
x

{- |
Constructs an `Opt` from a `Maybe`.
`Nothing` maps to `Def`,
and `Just` maps to `Some`.

>>> definite (optionally @'[ '[1,2],'[3]] Nothing)
[[1,2],[3]]
>>> definite (optionally @"foo" (Just "bar"))
"bar"
-}
optionally
  :: forall {k} def. SingDef def
  => Maybe (Demote k)
  -> Opt (def :: k)
optionally :: forall {k} (def :: k). SingDef def => Maybe (Demote k) -> Opt def
optionally = Opt def -> (Demote k -> Opt def) -> Maybe (Demote k) -> Opt def
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Opt def
forall k (def :: k). SingDef def => Opt def
Def Demote k -> Opt def
forall {k} (def :: k). Demote k -> Opt def
Some

{- |
Deconstructs an `Opt` to a `Demote`d value.
`Def` maps to `demote` @@def@,
and `Some` maps to its argument.
-}
definite :: forall {k} def. Opt (def :: k) -> Demote k
definite :: forall {k} (def :: k). Opt def -> Demote k
definite = \case
  Opt def
Def -> forall (a :: k). (SingKind k, SingI a) => Demote k
forall {k} (a :: k). (SingKind k, SingI a) => Demote k
demote @def
  Some Demote k
a -> Demote k
a

{- |
Deconstructs an `Opt` to an `Alternative` `Demote`d value.
`Def` maps to `empty`,
and `Some` maps to `pure`,
inverting `optionally`.
-}
perhaps
  :: forall {k} def m. Alternative m
  => Opt (def :: k) -> m (Demote k)
perhaps :: forall {k} (def :: k) (m :: * -> *).
Alternative m =>
Opt def -> m (Demote k)
perhaps = \case
  Opt def
Def -> m (Demote k)
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty
  Some Demote k
a -> Demote k -> m (Demote k)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Demote k
a

{- |
Datakind `Z`, promoting `Integer`,

>>> :kind! Demote Z
Demote Z :: *
= Integer

with `Pos` for constructing nonnegative integer types,
and `Neg` for constructing nonpositive integer types.

>>> demote @(Pos 90210)
90210
>>> demote @(Neg 5)
-5
>>> demote @(Neg 0)
0
>>> demote @(Pos 0)
0

Non`Neg`ative integer types are matched cardinally by `Pos`,

>>> :kind! Pos 9
Pos 9 :: Z
= Pos 9
>>> :kind! Neg 0
Neg 0 :: Z
= Pos 0

and `Neg`ative integer types are matched ordinally by `NegOneMinus`.

>>> :kind! Neg 6
Neg 6 :: Z
= NegOneMinus 5
>>> :kind! Neg 1
Neg 1 :: Z
= NegOneMinus 0

-}
data Z = Pos Natural | NegOneMinus Natural
  deriving (Z -> Z -> Bool
(Z -> Z -> Bool) -> (Z -> Z -> Bool) -> Eq Z
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Z -> Z -> Bool
== :: Z -> Z -> Bool
$c/= :: Z -> Z -> Bool
/= :: Z -> Z -> Bool
Eq, Eq Z
Eq Z =>
(Z -> Z -> Ordering)
-> (Z -> Z -> Bool)
-> (Z -> Z -> Bool)
-> (Z -> Z -> Bool)
-> (Z -> Z -> Bool)
-> (Z -> Z -> Z)
-> (Z -> Z -> Z)
-> Ord Z
Z -> Z -> Bool
Z -> Z -> Ordering
Z -> Z -> Z
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Z -> Z -> Ordering
compare :: Z -> Z -> Ordering
$c< :: Z -> Z -> Bool
< :: Z -> Z -> Bool
$c<= :: Z -> Z -> Bool
<= :: Z -> Z -> Bool
$c> :: Z -> Z -> Bool
> :: Z -> Z -> Bool
$c>= :: Z -> Z -> Bool
>= :: Z -> Z -> Bool
$cmax :: Z -> Z -> Z
max :: Z -> Z -> Z
$cmin :: Z -> Z -> Z
min :: Z -> Z -> Z
Ord, ReadPrec [Z]
ReadPrec Z
Int -> ReadS Z
ReadS [Z]
(Int -> ReadS Z)
-> ReadS [Z] -> ReadPrec Z -> ReadPrec [Z] -> Read Z
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS Z
readsPrec :: Int -> ReadS Z
$creadList :: ReadS [Z]
readList :: ReadS [Z]
$creadPrec :: ReadPrec Z
readPrec :: ReadPrec Z
$creadListPrec :: ReadPrec [Z]
readListPrec :: ReadPrec [Z]
Read, Int -> Z -> ShowS
[Z] -> ShowS
Z -> String
(Int -> Z -> ShowS) -> (Z -> String) -> ([Z] -> ShowS) -> Show Z
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Z -> ShowS
showsPrec :: Int -> Z -> ShowS
$cshow :: Z -> String
show :: Z -> String
$cshowList :: [Z] -> ShowS
showList :: [Z] -> ShowS
Show)

{- | `Neg`ate a `Natural` type . -}
type family Neg n where
  Neg 0 = Pos 0
  Neg n = NegOneMinus (n - 1)

instance Real Z where
  toRational :: Z -> Rational
toRational = Integer -> Rational
forall a. Real a => a -> Rational
toRational (Integer -> Rational) -> (Z -> Integer) -> Z -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Z -> Integer
forall a. Integral a => a -> Integer
toInteger

instance Integral Z where
  toInteger :: Z -> Integer
toInteger (Pos Natural
n) = Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
n
  toInteger (NegOneMinus Natural
n) = Integer -> Integer
forall a. Num a => a -> a
negate Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
n
  quotRem :: Z -> Z -> (Z, Z)
quotRem Z
x Z
y =
    let (Integer
q,Integer
r) = Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
quotRem (Z -> Integer
forall a. Integral a => a -> Integer
toInteger Z
x) (Z -> Integer
forall a. Integral a => a -> Integer
toInteger Z
y)
    in (Integer -> Z
forall a. Num a => Integer -> a
fromInteger Integer
q, Integer -> Z
forall a. Num a => Integer -> a
fromInteger Integer
r)
  divMod :: Z -> Z -> (Z, Z)
divMod Z
x Z
y =
    let (Integer
q,Integer
r) = Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod (Z -> Integer
forall a. Integral a => a -> Integer
toInteger Z
x) (Z -> Integer
forall a. Integral a => a -> Integer
toInteger Z
y)
    in (Integer -> Z
forall a. Num a => Integer -> a
fromInteger Integer
q, Integer -> Z
forall a. Num a => Integer -> a
fromInteger Integer
r)

instance Enum Z where
  toEnum :: Int -> Z
toEnum = Int -> Z
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  fromEnum :: Z -> Int
fromEnum = Z -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral

instance Num Z where
  Z
x + :: Z -> Z -> Z
+ Z
y = Integer -> Z
forall a. Num a => Integer -> a
fromInteger (Z -> Integer
forall a. Integral a => a -> Integer
toInteger Z
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Z -> Integer
forall a. Integral a => a -> Integer
toInteger Z
y)
  Z
x * :: Z -> Z -> Z
* Z
y = Integer -> Z
forall a. Num a => Integer -> a
fromInteger (Z -> Integer
forall a. Integral a => a -> Integer
toInteger Z
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Z -> Integer
forall a. Integral a => a -> Integer
toInteger Z
y)
  abs :: Z -> Z
abs Z
x = Integer -> Z
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer
forall a. Num a => a -> a
abs (Z -> Integer
forall a. Integral a => a -> Integer
toInteger Z
x))
  signum :: Z -> Z
signum Z
x = Integer -> Z
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer
forall a. Num a => a -> a
signum (Z -> Integer
forall a. Integral a => a -> Integer
toInteger Z
x))
  negate :: Z -> Z
negate Z
x = Integer -> Z
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer
forall a. Num a => a -> a
negate (Z -> Integer
forall a. Integral a => a -> Integer
toInteger Z
x))
  Z
x - :: Z -> Z -> Z
- Z
y = Integer -> Z
forall a. Num a => Integer -> a
fromInteger (Z -> Integer
forall a. Integral a => a -> Integer
toInteger Z
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Z -> Integer
forall a. Integral a => a -> Integer
toInteger Z
y)
  fromInteger :: Integer -> Z
fromInteger Integer
x =
    if Integer -> Integer
forall a. Num a => a -> a
signum Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0
    then Natural -> Z
Pos (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
x)
    else Natural -> Z
NegOneMinus (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer
forall a. Num a => a -> a
negate (Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
x)))

{- | Singleton representation for the `Z` kind. -}
data SInteger (n :: Z) where
  SPos :: SNat n -> SInteger (Pos n)
  SNegOneMinus :: SNat n -> SInteger (NegOneMinus n)

type instance Sing = SInteger

instance SingKind Z where
  type Demote Z = Integer
  fromSing :: forall (a :: Z). Sing a -> Demote Z
fromSing = \case
    SPos SNat n
n -> Demote Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Sing n -> Demote Natural
forall (a :: Natural). Sing a -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing SNat n
Sing n
n)
    SNegOneMinus SNat n
n -> Integer -> Integer
forall a. Num a => a -> a
negate Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Demote Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Sing n -> Demote Natural
forall (a :: Natural). Sing a -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing SNat n
Sing n
n)
  toSing :: Demote Z -> SomeSing Z
toSing Demote Z
n = Demote Z -> (forall (a :: Z). Sing a -> SomeSing Z) -> SomeSing Z
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Z
n Sing a -> SomeSing Z
forall k (a :: k). Sing a -> SomeSing k
forall (a :: Z). Sing a -> SomeSing Z
SomeSing

instance KnownNat n => SingI (Pos n) where
  sing :: Sing ('Pos n)
sing = SNat n -> SInteger ('Pos n)
forall (n :: Natural). SNat n -> SInteger ('Pos n)
SPos SNat n
Sing n
forall {k} (a :: k). SingI a => Sing a
sing

instance KnownNat n => SingI (NegOneMinus n) where
  sing :: Sing ('NegOneMinus n)
sing = SNat n -> SInteger ('NegOneMinus n)
forall (n :: Natural). SNat n -> SInteger ('NegOneMinus n)
SNegOneMinus SNat n
Sing n
forall {k} (a :: k). SingI a => Sing a
sing

{- |
Datakind `Q`, promoting `Rational`,

>>> :kind! Demote Q
Demote Q :: *
= Ratio Integer

with `:%` for constructing (unreduced) and matching rational types,

>>> demote @(Pos 7 :% 11)
7 % 11
>>> demote @(Neg 4 :% 6)
(-2) % 3
>>> :kind Pos 10 :% 10
Pos 10 :% 10 :: Q

and `%` and `Reduce` for constructing reduced rational types.

>>> :kind! Pos 14 % 49
Pos 14 % 49 :: Q
= Pos 2 :% 7
>>> type Percent n = Pos n :% 100
>>> :kind! Percent 10
Percent 10 :: Q
= Pos 10 :% 100
>>> :kind! Reduce (Percent 10)
Reduce (Percent 10) :: Q
= Pos 1 :% 10
-}
data Q = (:%) Z Natural
  deriving (Q -> Q -> Bool
(Q -> Q -> Bool) -> (Q -> Q -> Bool) -> Eq Q
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Q -> Q -> Bool
== :: Q -> Q -> Bool
$c/= :: Q -> Q -> Bool
/= :: Q -> Q -> Bool
Eq, Eq Q
Eq Q =>
(Q -> Q -> Ordering)
-> (Q -> Q -> Bool)
-> (Q -> Q -> Bool)
-> (Q -> Q -> Bool)
-> (Q -> Q -> Bool)
-> (Q -> Q -> Q)
-> (Q -> Q -> Q)
-> Ord Q
Q -> Q -> Bool
Q -> Q -> Ordering
Q -> Q -> Q
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Q -> Q -> Ordering
compare :: Q -> Q -> Ordering
$c< :: Q -> Q -> Bool
< :: Q -> Q -> Bool
$c<= :: Q -> Q -> Bool
<= :: Q -> Q -> Bool
$c> :: Q -> Q -> Bool
> :: Q -> Q -> Bool
$c>= :: Q -> Q -> Bool
>= :: Q -> Q -> Bool
$cmax :: Q -> Q -> Q
max :: Q -> Q -> Q
$cmin :: Q -> Q -> Q
min :: Q -> Q -> Q
Ord, Int -> Q -> ShowS
[Q] -> ShowS
Q -> String
(Int -> Q -> ShowS) -> (Q -> String) -> ([Q] -> ShowS) -> Show Q
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Q -> ShowS
showsPrec :: Int -> Q -> ShowS
$cshow :: Q -> String
show :: Q -> String
$cshowList :: [Q] -> ShowS
showList :: [Q] -> ShowS
Show, ReadPrec [Q]
ReadPrec Q
Int -> ReadS Q
ReadS [Q]
(Int -> ReadS Q)
-> ReadS [Q] -> ReadPrec Q -> ReadPrec [Q] -> Read Q
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS Q
readsPrec :: Int -> ReadS Q
$creadList :: ReadS [Q]
readList :: ReadS [Q]
$creadPrec :: ReadPrec Q
readPrec :: ReadPrec Q
$creadListPrec :: ReadPrec [Q]
readListPrec :: ReadPrec [Q]
Read)

{- |
Perform reduction on a rational type, idempotently.

prop> Reduce (Reduce q) ~ Reduce q
-}
type family Reduce q :: Q where
  Reduce (z :% n) = z % n

{- |
Construct a rational type in reduced form.
-}
type family (%) z n :: Q where
  Pos p % q = Pos (Div p (GCD p q)) :% Div q (GCD p q)
  NegOneMinus p % q
    = Neg (Div (1 + p) (GCD (1 + p) q))
    :% Div q (GCD (1 + p) q)

{- |
Construct the greatest common divisor of `Natural` types.
-}
type family GCD (a :: Natural) (b :: Natural) :: Natural where
  GCD 0 0 = 1
  GCD 0 b = b
  GCD a 0 = a
  GCD a b = GCD b (Mod a b)

instance Real Q where
  toRational :: Q -> Rational
toRational (Z
x :% Natural
y) = Rational -> Rational
forall a. Fractional a => Rational -> a
fromRational (Z -> Integer
forall a. Integral a => a -> Integer
toInteger Z
x Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
y)

instance Fractional Q where
  recip :: Q -> Q
recip (Pos Natural
x :% Natural
y) = (Natural -> Z
Pos Natural
y Z -> Natural -> Q
:% Natural
x)
  recip (NegOneMinus Natural
x :% Natural
y) = (Natural -> Z
NegOneMinus (Natural
y Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1) Z -> Natural -> Q
:% (Natural
1 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
x))
  fromRational :: Rational -> Q
fromRational Rational
x = (Integer -> Z
forall a. Num a => Integer -> a
fromInteger (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
x) Z -> Natural -> Q
:% Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
x))

instance Num Q where
  Q
x + :: Q -> Q -> Q
+ Q
y = Rational -> Q
forall a. Fractional a => Rational -> a
fromRational (Q -> Rational
forall a. Real a => a -> Rational
toRational Q
x Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ Q -> Rational
forall a. Real a => a -> Rational
toRational Q
y)
  Q
x * :: Q -> Q -> Q
* Q
y = Rational -> Q
forall a. Fractional a => Rational -> a
fromRational (Q -> Rational
forall a. Real a => a -> Rational
toRational Q
x Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Q -> Rational
forall a. Real a => a -> Rational
toRational Q
y)
  abs :: Q -> Q
abs Q
x = Rational -> Q
forall a. Fractional a => Rational -> a
fromRational (Rational -> Rational
forall a. Num a => a -> a
abs (Q -> Rational
forall a. Real a => a -> Rational
toRational Q
x))
  signum :: Q -> Q
signum Q
x = Rational -> Q
forall a. Fractional a => Rational -> a
fromRational (Rational -> Rational
forall a. Num a => a -> a
signum (Q -> Rational
forall a. Real a => a -> Rational
toRational Q
x))
  negate :: Q -> Q
negate Q
x = Rational -> Q
forall a. Fractional a => Rational -> a
fromRational (Rational -> Rational
forall a. Num a => a -> a
negate (Q -> Rational
forall a. Real a => a -> Rational
toRational Q
x))
  Q
x - :: Q -> Q -> Q
- Q
y = Rational -> Q
forall a. Fractional a => Rational -> a
fromRational (Q -> Rational
forall a. Real a => a -> Rational
toRational Q
x Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Q -> Rational
forall a. Real a => a -> Rational
toRational Q
y)
  fromInteger :: Integer -> Q
fromInteger Integer
x = Rational -> Q
forall a. Fractional a => Rational -> a
fromRational (Integer -> Rational
forall a. Num a => Integer -> a
fromInteger Integer
x)

{- | Singleton representation for the `Q` kind. -}
data SRational (n :: Q) where
  SRational :: SInteger n -> SNat m -> SRational (n :% m)

type instance Sing = SRational

instance SingKind Q where
  type Demote Q = Rational
  fromSing :: forall (a :: Q). Sing a -> Demote Q
fromSing (SRational SInteger n
num SNat m
denom)
    = Rational -> Demote Q
forall a. Fractional a => Rational -> a
fromRational
    (Rational -> Demote Q) -> Rational -> Demote Q
forall a b. (a -> b) -> a -> b
$ Demote Z -> Rational
forall a. Real a => a -> Rational
toRational (Sing n -> Demote Z
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Z). Sing a -> Demote Z
fromSing Sing n
SInteger n
num)
    Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ Demote Natural -> Rational
forall a. Real a => a -> Rational
toRational (Sing m -> Demote Natural
forall (a :: Natural). Sing a -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing SNat m
Sing m
denom)
  toSing :: Demote Q -> SomeSing Q
toSing Demote Q
q = Demote Q -> (forall (a :: Q). Sing a -> SomeSing Q) -> SomeSing Q
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Q
q Sing a -> SomeSing Q
forall k (a :: k). Sing a -> SomeSing k
forall (a :: Q). Sing a -> SomeSing Q
SomeSing

instance (SingI num, SingI denom) => SingI (num :% denom) where
  sing :: Sing (num ':% denom)
sing = SInteger num -> SNat denom -> SRational (num ':% denom)
forall (n :: Z) (m :: Natural).
SInteger n -> SNat m -> SRational (n ':% m)
SRational Sing num
SInteger num
forall {k} (a :: k). SingI a => Sing a
sing SNat denom
Sing denom
forall {k} (a :: k). SingI a => Sing a
sing