singletons-default 0.1.0.4 → 0.1.0.5
raw patch · 2 files changed
+125/−71 lines, 2 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- singletons-default.cabal +1/−1
- src/Data/Default/Singletons.hs +124/−70
singletons-default.cabal view
@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack name: singletons-default-version: 0.1.0.4+version: 0.1.0.5 synopsis: An optional type with type level default description: dependently typed optional values with default category: Data
src/Data/Default/Singletons.hs view
@@ -8,8 +8,8 @@ Portability : non-portable (GHC extensions) This module defines an `Opt`ional type with-either a `Def`ault promoted value,-or `Some` specific demoted value.+either a `Def`ault promoted value type,+or `Some` specific demoted value term. >>> definite (Def :: Opt True) True@@ -24,34 +24,15 @@ >>> maybe "def" show (perhaps (Some False :: Opt True)) "False" -Promoted datakinds and their `Demote`d datatypes include:+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->>> :kind! Demote Natural-Demote Natural :: *-= Natural->>> :kind! Demote Char-Demote Char :: *-= Char->>> :kind! Demote Bool-Demote Bool :: *-= Bool->>> :kind! Demote [k]-Demote [k] :: *-= [Demote k]->>> :kind! Demote String-Demote String :: *-= [Char]->>> :kind! Demote (Either k j)-Demote (Either k j) :: *-= Either (Demote k) (Demote j)->>> :kind! Demote (k,j)-Demote (k,j) :: *-= (Demote k, Demote j) -Because there is no promoted `Integer` and `Rational` datakinds,+Because there is no promoted `Integer` and `Rational` datakinds in base, this module defines them as `Z` and `Q`. >>> :kind! Demote Z@@ -63,21 +44,63 @@ The `Opt` type comes with `Num`, `Integral`, `Fractional`, and `Real` instances,-using `definite` values to do arithmetic;-and `IsString` and `IsList` instances,-which let you use literals to construct `Opt`.+using `definite` values to do arithmetic,+which let you use literals and arithmetic to construct+`Some` specific `Opt` value; ->>> "text" :: Opt ("hello" :: Symbol)+>>> 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] :: Opt ('[] :: [Natural])-Some [1,2]->>> Def + 0 :: Opt (Pos 1 :: Z)-Some 1->>> 0.5 + Def :: Opt (Neg 1 :% 3 :: Q)-Some (1 % 6)+>>> [[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@@ -108,6 +131,9 @@ , Z (..) , Neg , Q (..)+ , type (%)+ , type Reduce+ , type GCD , SInteger (..) , SRational (..) -- | Reexport Demote@@ -119,7 +145,7 @@ import Data.Default import GHC.IsList import Data.Ratio-import GHC.TypeNats+import GHC.TypeLits import Data.Singletons import Data.String import Prelude.Singletons ()@@ -128,36 +154,6 @@ `Opt`ional type with either a `Def`ault promoted value @def@, or `Some` specific `Demote`d value.--`Opt` is a `Monoid` which yields the leftmost `Some`.-->>> mempty :: Opt "xyz"-Def->>> Def <> "abc" <> "qrs" :: Opt "xyz"-Some "abc"--You can use `Opt` as an optional function argument.-->>> let greet (name :: Opt "Anon") = "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- -} data Opt (def :: k) where Def :: forall {k} def. SingDef def => Opt (def :: k)@@ -273,11 +269,29 @@ >>> 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 (Eq, Ord, Read, Show) -{- | Type family for negating a `Natural`.-}+{- | `Neg`ate a `Natural` type . -} type family Neg n where Neg 0 = Pos 0 Neg n = NegOneMinus (n - 1)@@ -338,16 +352,56 @@ Demote Q :: * = Ratio Integer -with `:%` for constructing rational types.+with `:%` for constructing (unreduced) and matching rational types, >>> demote @(Pos 7 :% 11) 7 % 11->>> demote @(Neg 4 :% 2)-(-2) % 1+>>> 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 (Eq, Ord, Show, 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 0 % 0 = Pos 0 :% 0+ 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 b = b+ GCD a 0 = a+ GCD a b = GCD b (Mod a b) instance Real Q where toRational (x :% y) = fromRational (toInteger x % toInteger y)