singleraeh (empty) → 0.1.0

raw patch · 11 files changed

+246/−0 lines, 11 filesdep +base

Dependencies added: base

Files

• CHANGELOG.md +4/−0
• LICENSE +20/−0
• README.md +14/−0
• singleraeh.cabal +51/−0
• src/Singleraeh/Either.hs +19/−0
• src/Singleraeh/Equality.hs +21/−0
• src/Singleraeh/List.hs +18/−0
• src/Singleraeh/Maybe.hs +15/−0
• src/Singleraeh/Natural.hs +16/−0
• src/Singleraeh/Symbol.hs +53/−0
• src/Singleraeh/Tuple.hs +15/−0

@@ -0,0 +1,4 @@+## 0.1.0 (2024-05-21)+Initial release.++* new home for my assorted singletons

@@ -0,0 +1,20 @@+Copyright (c) 2024 Ben Orchard (@raehik) <thefirstmuffinman@gmail.com>++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be included+in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

@@ -0,0 +1,14 @@+# singleraeh+Explicit singletons. More manual than `singletons`, but potentially easier to+use because you can give GHC more explicit information (compared to `singletons`+which often threads things through the `Sing` type family and `SingI` type+class).++Uses phadej's `defun` package for defunctionalizing type families. (Edit,+actually doesn't require `defun` just yet. But I think that's just because I+haven't bothered defunctionalizing things.)++Requires GHC >= 9.6 for the builtin `SNat`, `SSymbol` etc. singletons.++## License+Provided under the MIT license. See `LICENSE` for license text.

@@ -0,0 +1,51 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.35.2.+--+-- see: https://github.com/sol/hpack++name:           singleraeh+version:        0.1.0+synopsis:       raehik's singletons+description:    Please see README.md.+category:       Types, Data+author:         Ben Orchard+maintainer:     Ben Orchard <thefirstmuffinman@gmail.com>+license:        MIT+license-file:   LICENSE+build-type:     Simple+tested-with:+    GHC==9.8+  , GHC==9.6+extra-source-files:+    README.md+    CHANGELOG.md++library+  exposed-modules:+      Singleraeh.Either+      Singleraeh.Equality+      Singleraeh.List+      Singleraeh.Maybe+      Singleraeh.Natural+      Singleraeh.Symbol+      Singleraeh.Tuple+  other-modules:+      Paths_singleraeh+  hs-source-dirs:+      src+  default-extensions:+      LambdaCase+      NoStarIsType+      DerivingVia+      DeriveAnyClass+      GADTs+      RoleAnnotations+      DefaultSignatures+      TypeFamilies+      DataKinds+      MagicHash+  ghc-options: -Wall -Wno-unticked-promoted-constructors+  build-depends:+      base >=4.18 && <5+  default-language: GHC2021

@@ -0,0 +1,19 @@+module Singleraeh.Either where++import Data.Kind ( Type )++-- | 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)++demoteSEither+    :: forall dl dr sl sr elr+    .  (forall l. sl l -> dl)+    -> (forall r. sr r -> dr)+    -> SEither sl sr elr+    -> Either dl dr+demoteSEither demoteSL demoteSR = \case+  SLeft  sl -> Left  $ demoteSL sl+  SRight sr -> Right $ demoteSR sr

@@ -0,0 +1,21 @@+module Singleraeh.Equality where++import Data.Type.Equality++-- | Do one thing if @a@ and @b@ are equal, else do something else.+--+-- Handy for chaining 'testEquality's e.g. when singling type family equation+-- lists.+--+-- Use like so:+--+-- > testEqN sn sm1 _ $ testEqN sn sm2 _ $ ...+--+-- TODO really handy. give a larger, concrete example+testEqElse+    :: forall f a b r. TestEquality f+    => f a -> f b -> (a ~ b => r) -> r -> r+testEqElse sa sb rEq rNEq =+    case testEquality sa sb of+      Just Refl -> gcastWith Refl rEq+      Nothing   -> rNEq

@@ -0,0 +1,18 @@+module Singleraeh.List where++import Data.Kind ( Type )++-- | Singleton list.+type SList :: (a -> Type) -> [a] -> Type+data SList sa as where+    SCons :: sa a -> SList sa as -> SList sa (a : as)+    SNil  ::                        SList sa '[]++demoteSList+    :: forall da sa as+    .  (forall a. sa a -> da)+    -> SList sa as+    -> [da]+demoteSList demoteSA = \case+  SCons sa sas -> demoteSA sa : demoteSList demoteSA sas+  SNil         -> []

@@ -0,0 +1,15 @@+module Singleraeh.Maybe where++-- | Singleton 'Maybe'.+data SMaybe sa (ma :: Maybe a) where+    SJust    :: sa a -> SMaybe sa (Just a)+    SNothing ::         SMaybe sa Nothing++demoteSMaybe+    :: forall da sa ma+    .  (forall a. sa a -> da)+    -> SMaybe sa ma+    -> Maybe da+demoteSMaybe demoteSA = \case+  SJust sa -> Just $ demoteSA sa+  SNothing -> Nothing

@@ -0,0 +1,16 @@+module Singleraeh.Natural where++import GHC.TypeNats+import Unsafe.Coerce ( unsafeCoerce )++(%+) :: SNat n -> SNat m -> SNat (n + m)+n %+ m = withSomeSNat (fromSNat n + fromSNat m) unsafeCoerce++(%-) :: 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++sDiv :: SNat n -> SNat m -> SNat (Div n m)+sDiv n m = withSomeSNat (div (fromSNat n) (fromSNat m)) unsafeCoerce

@@ -0,0 +1,53 @@+{-# LANGUAGE UndecidableInstances #-} -- for RevCharsToSymbol'++module Singleraeh.Symbol where++import Singleraeh.List ( SList(..) )+import Singleraeh.Maybe ( SMaybe(..) )+import Singleraeh.Tuple ( STuple2(..) )+import GHC.TypeLits+import Unsafe.Coerce ( unsafeCoerce )++sConsSymbol :: SChar ch -> SSymbol str -> SSymbol (ConsSymbol ch str)+sConsSymbol ch str =+    withSomeSSymbol (fromSChar ch : fromSSymbol str) unsafeCoerce++-- TODO test!!!+sUnconsSymbol+    :: SSymbol str+    -> SMaybe (STuple2 SChar SSymbol) (UnconsSymbol str)+sUnconsSymbol sstr =+    case fromSSymbol sstr of+      []        -> unsafeCoerce SNothing+      ch : str' -> unsafeCoerce $ SJust $ STuple2+        (withSomeSChar ch unsafeCoerce)+        (withSomeSSymbol str' unsafeCoerce)++-- | Re-construct the output from 'UnconsSymbol'.+type family ReconsSymbol msym where+    ReconsSymbol (Just '(ch, sym)) = ConsSymbol ch sym+    ReconsSymbol Nothing           = ""++sReconsSymbol+    :: SMaybe (STuple2 SChar SSymbol) msym+    -> SSymbol (ReconsSymbol msym)+sReconsSymbol = \case+  SJust (STuple2 ch sym) -> sConsSymbol ch sym+  SNothing               -> SSymbol @""++-- TODO we can write this with @Foldl (FlipSym1 ConsSymbolSym) "" chs@, but+-- we need more singletons then. check it out later :)+type RevCharsToSymbol chs = RevCharsToSymbol' "" chs+type family RevCharsToSymbol' sym chs where+    RevCharsToSymbol' sym (ch : chs) = RevCharsToSymbol' (ConsSymbol ch sym) chs+    RevCharsToSymbol' sym '[]        = sym++revCharsToSymbol :: SList SChar chs -> SSymbol (RevCharsToSymbol chs)+revCharsToSymbol = revCharsToSymbol' (SSymbol @"")++revCharsToSymbol'+    :: SSymbol str+    -> SList SChar chs -> SSymbol (RevCharsToSymbol' str chs)+revCharsToSymbol' sacc = \case+  SCons sch sstr -> revCharsToSymbol' (sConsSymbol sch sacc) sstr+  SNil           -> sacc

@@ -0,0 +1,15 @@+module Singleraeh.Tuple where++import Data.Kind ( Type )++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)++demoteSTuple2+    :: forall da db sa sb ab+    .  (forall a. sa a -> da)+    -> (forall b. sb b -> db)+    -> STuple2 sa sb ab+    -> (da, db)+demoteSTuple2 demoteSA demoteSB (STuple2 sa sb) = (demoteSA sa, demoteSB sb)