singleraeh 0.2.1 → 0.3.0

raw patch · 8 files changed

+153/−37 lines, 8 filesdep +singletonsPVP ok

version bump matches the API change (PVP)

Dependencies added: singletons

API changes (from Hackage documentation)

Files

• CHANGELOG.md +5/−0
• singleraeh.cabal +4/−2
• src/Singleraeh/Bool.hs +21/−0
• src/Singleraeh/Either.hs +3/−8
• src/Singleraeh/Maybe.hs +18/−1
• src/Singleraeh/Sing.hs +0/−25
• src/Singleraeh/SingI.hs +48/−0
• src/Singleraeh/Tuple.hs +54/−1

@@ -1,3 +1,8 @@+## 0.3.0 (2024-06-01)+* remove `Sing`, provide `SingI` instead+* add `SBool` (singled booleans)+* add `STuple3`+ ## 0.2.1 (2024-05-27) * add `Reverse` for lists 

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           singleraeh-version:        0.2.1+version:        0.3.0 synopsis:       raehik's singletons description:    Please see README.md. category:       Types, Data@@ -23,13 +23,14 @@  library   exposed-modules:+      Singleraeh.Bool       Singleraeh.Demote       Singleraeh.Either       Singleraeh.Equality       Singleraeh.List       Singleraeh.Maybe       Singleraeh.Natural-      Singleraeh.Sing+      Singleraeh.SingI       Singleraeh.Symbol       Singleraeh.Tuple   other-modules:@@ -50,4 +51,5 @@   ghc-options: -Wall -Wno-unticked-promoted-constructors   build-depends:       base >=4.18 && <5+    , singletons >=3.0.2 && <3.1   default-language: GHC2021

@@ -0,0 +1,21 @@+module Singleraeh.Bool where++import Data.Kind ( Type )+import Singleraeh.Demote++-- | Singleton 'Bool'.+type SBool :: Bool -> Type+data SBool b where+    STrue  :: SBool True+    SFalse :: SBool False++demoteSBool :: SBool b -> Bool+demoteSBool = \case STrue -> True; SFalse -> False++instance Demotable SBool where+    type Demote SBool = Bool+    demote = demoteSBool++class SingBool (b :: Bool) where singBool :: SBool b+instance SingBool True  where singBool = STrue+instance SingBool False where singBool = SFalse

@@ -1,7 +1,6 @@ module Singleraeh.Either where  import Singleraeh.Demote-import Singleraeh.Sing import Data.Kind ( Type, Constraint )  -- | Singleton 'Either'.@@ -34,15 +33,11 @@     -> SEither sl sr elr singEither = singEither' @_ @_ @cl @cr -instance (Demotable sl, Demotable sr) => Demotable (SEither sl sr) where-    type Demote (SEither sl sr) = Either (Demote sl) (Demote sr)-    demote = demoteSEither demote demote- instance cl l => SingEither cl cr sl sr (Left  l) where     singEither'  singL _singR = SLeft  singL instance cr r => SingEither cl cr sl sr (Right r) where     singEither' _singL  singR = SRight singR -instance (Sing sl, Sing sr) => Sing (SEither sl sr) where-    type SingC (SEither sl sr) = SingEither (SingC sl) (SingC sr) sl sr-    sing' = singEither @(SingC sl) @(SingC sr) sing sing+instance (Demotable sl, Demotable sr) => Demotable (SEither sl sr) where+    type Demote (SEither sl sr) = Either (Demote sl) (Demote sr)+    demote = demoteSEither demote demote

@@ -1,6 +1,6 @@ module Singleraeh.Maybe where -import Data.Kind ( Type )+import Data.Kind ( Type, Constraint ) import Singleraeh.Demote  -- | Singleton 'Maybe'.@@ -21,3 +21,20 @@ instance Demotable sa => Demotable (SMaybe sa) where     type Demote (SMaybe sa) = Maybe (Demote sa)     demote = demoteSMaybe demote++class SingMaybe (ca :: ak -> Constraint) (sa :: ak -> Type) (ma :: Maybe ak) where+    singMaybe'+        :: (forall a. ca a => sa a)+        -> SMaybe sa ma++singMaybe+    :: forall ca sa ma. SingMaybe ca sa ma+    => (forall a. ca a => sa a)+    -> SMaybe sa ma+singMaybe = singMaybe' @_ @ca++instance ca a => SingMaybe ca sa (Just a) where+    singMaybe' sa = SJust sa++instance SingMaybe ca sa Nothing where+    singMaybe' _  = SNothing

@@ -1,25 +0,0 @@-module Singleraeh.Sing where--import Data.Kind ( Type, Constraint )-import GHC.TypeLits--class Sing (sa :: ak -> Type) where-    type SingC sa :: ak -> Constraint-    sing' :: forall (a :: ak). SingC sa a => sa a--sing-    :: forall {ak} (sa :: ak -> Type) (a :: ak)-    .  (Sing sa, SingC sa a) => sa a-sing = sing' @_ @sa @a--instance Sing SNat where-    type SingC SNat = KnownNat-    sing' = natSing--instance Sing SSymbol where-    type SingC SSymbol = KnownSymbol-    sing' = symbolSing--instance Sing SChar where-    type SingC SChar = KnownChar-    sing' = charSing

@@ -0,0 +1,48 @@+{-# LANGUAGE UndecidableInstances #-} -- for recursive SingI constraints++-- Orphan instances when we define them elsewhere, so here they shall stay.++module Singleraeh.SingI where++import Data.Kind ( Type )+import GHC.TypeLits++import Singleraeh.Bool+import Singleraeh.Tuple+import Singleraeh.Either+import Singleraeh.Maybe++class SingI (a :: k) where+    type Sing :: k -> Type+    sing' :: Sing a++sing :: forall {k} (a :: k). SingI a => Sing a+sing = sing' @_ @a++instance KnownNat n => SingI n where+    type Sing = SNat+    sing' = SNat++instance KnownSymbol str => SingI str where+    type Sing = SSymbol+    sing' = SSymbol++instance KnownChar ch => SingI ch where+    type Sing = SChar+    sing' = SChar++instance SingBool b => SingI b where+    type Sing = SBool+    sing' = singBool++instance SingTuple2 SingI SingI Sing Sing lr => SingI lr where+    type Sing = STuple2 Sing Sing+    sing' = singTuple2 @SingI @SingI sing sing++instance SingEither SingI SingI Sing Sing elr => SingI elr where+    type Sing = SEither Sing Sing+    sing' = singEither @SingI @SingI sing sing++instance SingMaybe SingI Sing ma => SingI ma where+    type Sing = SMaybe Sing+    sing' = singMaybe @SingI sing

@@ -1,7 +1,7 @@ module Singleraeh.Tuple where  import Singleraeh.Demote-import Data.Kind ( Type )+import Data.Kind ( Type, Constraint )  data SUnit (unit :: ()) where SUnit :: SUnit '() @@ -27,3 +27,56 @@ instance (Demotable sa, Demotable sb) => Demotable (STuple2 sa sb) where     type Demote (STuple2 sa sb) = (Demote sa, Demote sb)     demote = demoteSTuple2 demote demote++class SingTuple2 (cl :: lk -> Constraint) (cr :: rk -> Constraint) (sl :: lk -> Type) (sr :: rk -> Type) (lr :: (lk, rk)) where+    singTuple2'+        :: (forall l. cl l => sl l)+        -> (forall r. cr r => sr r)+        -> STuple2 sl sr lr++singTuple2+    :: forall cl cr sl sr lr. SingTuple2 cl cr sl sr lr+    => (forall l. cl l => sl l)+    -> (forall r. cr r => sr r)+    -> STuple2 sl sr lr+singTuple2 = singTuple2' @_ @_ @cl @cr++instance (cl l, cr r) => SingTuple2 cl cr sl sr '(l, r) where+    singTuple2' sl sr = STuple2 sl sr++type STuple3 :: (a -> Type) -> (b -> Type) -> (c -> Type) -> (a, b, c) -> Type+data STuple3 sa sb sc abc where+    STuple3 :: sa a -> sb b -> sc c -> STuple3 sa sb sc '(a, b, c)++demoteSTuple3+    :: forall da db dc sa sb sc abc+    .  (forall a. sa a -> da)+    -> (forall b. sb b -> db)+    -> (forall c. sc c -> dc)+    -> STuple3 sa sb sc abc+    -> (da, db, dc)+demoteSTuple3 demoteSA demoteSB demoteSC (STuple3 sa sb sc) =+    (demoteSA sa, demoteSB sb, demoteSC sc)++instance (Demotable sa, Demotable sb, Demotable sc)+  => Demotable (STuple3 sa sb sc) where+    type Demote (STuple3 sa sb sc) = (Demote sa, Demote sb, Demote sc)+    demote = demoteSTuple3 demote demote demote++class SingTuple3 (ca :: ak -> Constraint) (cb :: bk -> Constraint) (cc :: ck -> Constraint) (sa :: ak -> Type) (sb :: bk -> Type) (sc :: ck -> Type) (abc :: (ak, bk, ck)) where+    singTuple3'+        :: (forall a. ca a => sa a)+        -> (forall b. cb b => sb b)+        -> (forall c. cc c => sc c)+        -> STuple3 sa sb sc abc++singTuple3+    :: forall ca cb cc sa sb sc abc. SingTuple3 ca cb cc sa sb sc abc+    => (forall a. ca a => sa a)+    -> (forall b. cb b => sb b)+    -> (forall c. cc c => sc c)+    -> STuple3 sa sb sc abc+singTuple3 = singTuple3' @_ @_ @_ @ca @cb @cc++instance (ca a, cb b, cc c) => SingTuple3 ca cb cc sa sb sc '(a, b, c) where+    singTuple3' sa sb sc = STuple3 sa sb sc