packages feed

singleraeh 0.1.0 → 0.2.0

raw patch · 9 files changed

+128/−7 lines, 9 files

Files

CHANGELOG.md view
@@ -1,3 +1,9 @@+## 0.2.0 (2024-05-25)+* add more singled `Natural` operations+* add `Sing` for automatic singling+* add `Demotable` for automatic demoting+* add `SUnit`+ ## 0.1.0 (2024-05-21) Initial release.
singleraeh.cabal view
@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           singleraeh-version:        0.1.0+version:        0.2.0 synopsis:       raehik's singletons description:    Please see README.md. category:       Types, Data@@ -23,11 +23,13 @@  library   exposed-modules:+      Singleraeh.Demote       Singleraeh.Either       Singleraeh.Equality       Singleraeh.List       Singleraeh.Maybe       Singleraeh.Natural+      Singleraeh.Sing       Singleraeh.Symbol       Singleraeh.Tuple   other-modules:
+ src/Singleraeh/Demote.hs view
@@ -0,0 +1,26 @@+module Singleraeh.Demote where++import Data.Kind ( Type, Constraint )+import GHC.TypeLits+import GHC.TypeNats qualified as TN++-- | Singleton types which may be demoted.+type Demotable :: (k -> Type) -> Constraint+class Demotable sk where+    -- | Demoted type.+    type Demote sk :: Type++    -- | Demote a term of the singleton @sk@.+    demote :: forall k. sk k -> Demote sk++instance Demotable SNat where+    type Demote SNat = Natural+    demote = TN.fromSNat++instance Demotable SSymbol where+    type Demote SSymbol = String+    demote = fromSSymbol++instance Demotable SChar where+    type Demote SChar = Char+    demote = fromSChar
src/Singleraeh/Either.hs view
@@ -1,12 +1,14 @@ module Singleraeh.Either where -import Data.Kind ( Type )+import Singleraeh.Demote+import Singleraeh.Sing+import Data.Kind ( Type, Constraint )  -- | Singleton 'Either'.-type SEither :: (a -> Type) -> (b -> Type) -> Either a b -> Type-data SEither sa sb eab where-    SLeft  :: sa a -> SEither sa sb (Left  a)-    SRight :: sb b -> SEither sa sb (Right b)+type SEither :: (l -> Type) -> (r -> Type) -> Either l r -> Type+data SEither sl sr elr where+    SLeft  :: sl l -> SEither sl sr (Left  l)+    SRight :: sr r -> SEither sl sr (Right r)  demoteSEither     :: forall dl dr sl sr elr@@ -17,3 +19,30 @@ demoteSEither demoteSL demoteSR = \case   SLeft  sl -> Left  $ demoteSL sl   SRight sr -> Right $ demoteSR sr++class SingEither (cl :: lk -> Constraint) (cr :: rk -> Constraint) (sl :: lk -> Type) (sr :: rk -> Type) (elr :: Either lk rk) where+    singEither'+        :: (forall l. cl l => sl l)+        -> (forall r. cr r => sr r)+        -> SEither sl sr elr++-- reordered types (hidden lk, rk because implied)+singEither+    :: forall cl cr sl sr elr. SingEither cl cr sl sr elr+    => (forall l. cl l => sl l)+    -> (forall r. cr r => sr r)+    -> 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
src/Singleraeh/List.hs view
@@ -1,6 +1,7 @@ module Singleraeh.List where  import Data.Kind ( Type )+import Singleraeh.Demote  -- | Singleton list. type SList :: (a -> Type) -> [a] -> Type@@ -16,3 +17,7 @@ demoteSList demoteSA = \case   SCons sa sas -> demoteSA sa : demoteSList demoteSA sas   SNil         -> []++instance Demotable sa => Demotable (SList sa) where+    type Demote (SList sa) = [Demote sa]+    demote = demoteSList demote
src/Singleraeh/Maybe.hs view
@@ -1,7 +1,11 @@ module Singleraeh.Maybe where +import Data.Kind ( Type )+import Singleraeh.Demote+ -- | Singleton 'Maybe'.-data SMaybe sa (ma :: Maybe a) where+type SMaybe :: (a -> Type) -> Maybe a -> Type+data SMaybe sa ma where     SJust    :: sa a -> SMaybe sa (Just a)     SNothing ::         SMaybe sa Nothing @@ -13,3 +17,7 @@ demoteSMaybe demoteSA = \case   SJust sa -> Just $ demoteSA sa   SNothing -> Nothing++instance Demotable sa => Demotable (SMaybe sa) where+    type Demote (SMaybe sa) = Maybe (Demote sa)+    demote = demoteSMaybe demote
src/Singleraeh/Natural.hs view
@@ -3,11 +3,17 @@ import GHC.TypeNats import Unsafe.Coerce ( unsafeCoerce ) +infixl 6 %+ (%+) :: SNat n -> SNat m -> SNat (n + m) n %+ m = withSomeSNat (fromSNat n + fromSNat m) unsafeCoerce +infixl 6 %- (%-) :: SNat n -> SNat m -> SNat (n - m) n %- m = withSomeSNat (fromSNat n - fromSNat m) unsafeCoerce++infixl 7 %*+(%*) :: SNat n -> SNat m -> SNat (n * m)+n %* m = withSomeSNat (fromSNat n * fromSNat m) unsafeCoerce  sMod :: SNat n -> SNat m -> SNat (Mod n m) sMod n m = withSomeSNat (mod (fromSNat n) (fromSNat m)) unsafeCoerce
+ src/Singleraeh/Sing.hs view
@@ -0,0 +1,25 @@+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
src/Singleraeh/Tuple.hs view
@@ -1,7 +1,17 @@ module Singleraeh.Tuple where +import Singleraeh.Demote import Data.Kind ( Type ) +data SUnit (unit :: ()) where SUnit :: SUnit '()++demoteSUnit :: SUnit unit -> ()+demoteSUnit SUnit = ()++instance Demotable SUnit where+    type Demote SUnit = ()+    demote = demoteSUnit+ type STuple2 :: (a -> Type) -> (b -> Type) -> (a, b) -> Type data STuple2 sa sb ab where     STuple2 :: sa a -> sb b -> STuple2 sa sb '(a, b)@@ -13,3 +23,7 @@     -> STuple2 sa sb ab     -> (da, db) demoteSTuple2 demoteSA demoteSB (STuple2 sa sb) = (demoteSA sa, demoteSB sb)++instance (Demotable sa, Demotable sb) => Demotable (STuple2 sa sb) where+    type Demote (STuple2 sa sb) = (Demote sa, Demote sb)+    demote = demoteSTuple2 demote demote