diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,4 @@ +## 0.1.0 (2024-05-21) +Initial release. + +* new home for my assorted singletons diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,20 @@ +Copyright (c) 2024 Ben Orchard (@raehik) + +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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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. diff --git a/singleraeh.cabal b/singleraeh.cabal new file mode 100644 --- /dev/null +++ b/singleraeh.cabal @@ -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 +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 diff --git a/src/Singleraeh/Either.hs b/src/Singleraeh/Either.hs new file mode 100644 --- /dev/null +++ b/src/Singleraeh/Either.hs @@ -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 diff --git a/src/Singleraeh/Equality.hs b/src/Singleraeh/Equality.hs new file mode 100644 --- /dev/null +++ b/src/Singleraeh/Equality.hs @@ -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 diff --git a/src/Singleraeh/List.hs b/src/Singleraeh/List.hs new file mode 100644 --- /dev/null +++ b/src/Singleraeh/List.hs @@ -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 -> [] diff --git a/src/Singleraeh/Maybe.hs b/src/Singleraeh/Maybe.hs new file mode 100644 --- /dev/null +++ b/src/Singleraeh/Maybe.hs @@ -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 diff --git a/src/Singleraeh/Natural.hs b/src/Singleraeh/Natural.hs new file mode 100644 --- /dev/null +++ b/src/Singleraeh/Natural.hs @@ -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 diff --git a/src/Singleraeh/Symbol.hs b/src/Singleraeh/Symbol.hs new file mode 100644 --- /dev/null +++ b/src/Singleraeh/Symbol.hs @@ -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 diff --git a/src/Singleraeh/Tuple.hs b/src/Singleraeh/Tuple.hs new file mode 100644 --- /dev/null +++ b/src/Singleraeh/Tuple.hs @@ -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)