diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,6 @@ +## 0.2.0 (2024-05-21) +* add singleton versions of various types, functions + ## 0.1.1 (2024-05-16) * add `Doc` type for `ErrorMessage`-like errors, except term level also diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -2,7 +2,7 @@ Utilities for writing `Show`-like type families i.e. instead of `showsPrec :: Int -> a -> ShowS`, we have `ShowsPrec :: Natural -> k -> Symbol`. -Requires at least GHC 9.2 for the type-level `Symbol` manipulation. +Requires at least GHC 9.6 for the builtin `SChar` etc. singletons. ## Why? [refined-hackage]: https://hackage.haskell.org/package/refined diff --git a/src/TypeLevelShow/Doc.hs b/src/TypeLevelShow/Doc.hs --- a/src/TypeLevelShow/Doc.hs +++ b/src/TypeLevelShow/Doc.hs @@ -1,10 +1,26 @@ {-# LANGUAGE AllowAmbiguousTypes #-} -- for reifying -module TypeLevelShow.Doc where +module TypeLevelShow.Doc + ( + -- * Term level + Doc(..) + , renderDoc + -- * Type level + , PDoc + , RenderPDoc + , ErrorPDoc + + -- * Singleton + , SDoc(..) + , SingDoc(singDoc) + , demoteDoc + , reifyDoc + , errorPDoc + ) where + import GHC.TypeLits qualified as TE -- TE = TypeError -import GHC.TypeLits ( Symbol, KnownSymbol, symbolVal' ) -import GHC.Exts ( proxy# ) +import GHC.TypeLits hiding ( ErrorMessage(..) ) -- | Simple pretty document ADT. -- @@ -25,29 +41,68 @@ -- ^ stack docs on top of each other (newline) deriving stock Show +-- | Render a 'Doc' as a 'String', formatted how 'ErrorMessage's get displayed. +renderDoc :: Doc String -> String +renderDoc doc = " • " <> go doc + where + go = \case + Text s -> s + l :<>: r -> go l <> go r + l :$$: r -> go l <> "\n " <> go r + -- | Promoted 'Doc'. type PDoc = Doc Symbol -- | Render a 'PDoc' as an 'ErrorMessage', for type-level error messages. -- -- 'PDoc' is a subset of 'ErrorMessage', so this is very boring. -type RenderDoc :: PDoc -> TE.ErrorMessage -type family RenderDoc doc where - RenderDoc (Text s) = TE.Text s - RenderDoc (l :<>: r) = RenderDoc l TE.:<>: RenderDoc r - RenderDoc (l :$$: r) = RenderDoc l TE.:$$: RenderDoc r +type RenderPDoc :: PDoc -> TE.ErrorMessage +type family RenderPDoc doc where + RenderPDoc (Text s) = TE.Text s + RenderPDoc (l :<>: r) = RenderPDoc l TE.:<>: RenderPDoc r + RenderPDoc (l :$$: r) = RenderPDoc l TE.:$$: RenderPDoc r --- | Reify a promoted 'Doc' to the corresponding term-level one. -class ReifyDoc (doc :: PDoc) where - -- TODO do we want to do IsString directly in here? will it guarantee better - -- performance, rather than mapping afterwards? hard to say - reifyDoc :: Doc String +-- | Render a 'PDoc' as an 'ErrorMessage', and wrap it in a 'TypeError'. +-- +-- Note that this must be a type family, or the 'PDoc' won't actually get +-- rendered. +type ErrorPDoc :: PDoc -> a +type family ErrorPDoc doc where ErrorPDoc doc = TypeError (RenderPDoc doc) -instance KnownSymbol s => ReifyDoc (Text s) where - reifyDoc = Text $ symbolVal' (proxy# @s) +-- | Singleton 'Doc'. +data SDoc (doc :: PDoc) where + SText :: SSymbol s -> SDoc (Text s) + (:$<>:) :: SDoc docl -> SDoc docr -> SDoc (docl :<>: docr) + (:$$$:) :: SDoc docl -> SDoc docr -> SDoc (docl :$$: docr) -instance (ReifyDoc l, ReifyDoc r) => ReifyDoc (l :<>: r) where - reifyDoc = reifyDoc @l :<>: reifyDoc @r +-- | Produce the singleton for the given promoted 'Doc'. +class SingDoc (doc :: PDoc) where + singDoc :: SDoc doc -instance (ReifyDoc l, ReifyDoc r) => ReifyDoc (l :$$: r) where - reifyDoc = reifyDoc @l :$$: reifyDoc @r +instance KnownSymbol s => SingDoc (Text s) where + singDoc = SText (SSymbol @s) + +instance (SingDoc l, SingDoc r) => SingDoc (l :<>: r) where + singDoc = singDoc @l :$<>: singDoc @r + +instance (SingDoc l, SingDoc r) => SingDoc (l :$$: r) where + singDoc = singDoc @l :$$$: singDoc @r + +-- | Demote an 'SDoc' singleton to the corresponding base 'Doc'. +demoteDoc :: SDoc doc -> Doc String +demoteDoc = \case + SText s -> Text $ fromSSymbol s + l :$<>: r -> demoteDoc l :<>: demoteDoc r + l :$$$: r -> demoteDoc l :$$: demoteDoc r + +-- | Reify a promoted 'Doc' to the corresponding term-level one. +reifyDoc :: forall (doc :: PDoc). SingDoc doc => Doc String +reifyDoc = demoteDoc (singDoc @doc) + +-- | Render a 'PDoc' as a 'String', and call 'error' on it. +-- +-- This enables using the same code for type- and term- "runtime" errors. +-- This can't be typechecked, naturally, but it's still nice. +errorPDoc :: forall (doc :: PDoc) a. SingDoc doc => a +-- add extra newline because runtime errors print like @*** Exception: _@ +errorPDoc = error $ ("\n" <>) $ renderDoc $ reifyDoc @doc diff --git a/src/TypeLevelShow/Natural.hs b/src/TypeLevelShow/Natural.hs --- a/src/TypeLevelShow/Natural.hs +++ b/src/TypeLevelShow/Natural.hs @@ -1,112 +1,72 @@ {-# LANGUAGE UndecidableInstances #-} +{- | Turn type-level 'Natural's into 'Symbol's. + +/Warning:/ GHC may error out if you pass an 'SNat' that's too large to the +singled functions, due to reduction stack size. Follow the error message +instructions if you think you need it. This seems not to happen with @:k!@, +probably due to different settings. +-} + module TypeLevelShow.Natural where +import TypeLevelShow.Natural.Digit +import Singleraeh.Natural +import Singleraeh.Equality ( testEqElse ) +import Singleraeh.Symbol ( sConsSymbol ) import GHC.TypeLits -import DeFun.Core ( type (~>), type App, type (@@) ) +import DeFun.Core +import Unsafe.Coerce ( unsafeCoerce ) -type ShowNatBin n = ShowNatBase 2 ShowNatBinaryDigitSym n -type ShowNatOct n = ShowNatBase 8 ShowNatOctalDigitSym n -type ShowNatDec n = ShowNatBase 10 ShowNatDecimalDigitSym n -type ShowNatHexLower n = ShowNatBase 16 ShowNatHexDigitLowerSym n -type ShowNatHexUpper n = ShowNatBase 16 ShowNatHexDigitUpperSym n +type ShowNatBin n = ShowNatBase 2 ShowNatDigitHexLowerSym n +type ShowNatOct n = ShowNatBase 8 ShowNatDigitHexLowerSym n +type ShowNatDec n = ShowNatBase 10 ShowNatDigitHexLowerSym n +type ShowNatHexLower n = ShowNatBase 16 ShowNatDigitHexLowerSym n +type ShowNatHexUpper n = ShowNatBase 16 ShowNatDigitHexUpperSym n +sShowNatBin :: SNat n -> SSymbol (ShowNatBin n) +sShowNatBin = sShowNatBase (SNat @2) sShowNatDigitHexLower + +sShowNatOct :: SNat n -> SSymbol (ShowNatOct n) +sShowNatOct = sShowNatBase (SNat @8) sShowNatDigitHexLower + +sShowNatDec :: SNat n -> SSymbol (ShowNatDec n) +sShowNatDec = sShowNatBase (SNat @10) sShowNatDigitHexLower + +sShowNatHexLower :: SNat n -> SSymbol (ShowNatHexLower n) +sShowNatHexLower = sShowNatBase (SNat @16) sShowNatDigitHexLower + +sShowNatHexUpper :: SNat n -> SSymbol (ShowNatHexUpper n) +sShowNatHexUpper = sShowNatBase (SNat @16) sShowNatDigitHexUpper + -- | Render a type-level 'Natural' in the given base using the given digit --- printer. +-- renderer. +-- +-- The digit renderer is guaranteed to be called with @0 <= n < base@. type family ShowNatBase base showDigit n where -- | Our algorithm returns the empty 'Symbol' for 0, so handle it here. ShowNatBase base showDigit 0 = "0" - ShowNatBase base showDigit n = ShowNatBase' base showDigit "" n +sShowNatBase + :: SNat base -> Lam SNat SChar showDigit -> SNat n + -> SSymbol (ShowNatBase base showDigit n) +sShowNatBase sbase sf sn = + testEqElse sn (SNat @0) (SSymbol @"0") + $ unsafeCoerce $ sShowNatBase' sbase sf (SSymbol @"") sn + type ShowNatBase' :: Natural -> (Natural ~> Char) -> Symbol -> Natural -> Symbol type family ShowNatBase' base showDigit acc n where ShowNatBase' base showDigit acc 0 = acc ShowNatBase' base showDigit acc n = ShowNatBase' base showDigit (ConsSymbol (showDigit @@ (n `Mod` base)) acc) (n `Div` base) --- TODO add TypeErrors to invalid usages of these digit printers --- should be free performance-wise so no harm --- low priority because they're internals anyway - -type family ShowNatBinaryDigit (d :: Natural) :: Char where - ShowNatBinaryDigit 0 = '0' - ShowNatBinaryDigit 1 = '1' - -type ShowNatBinaryDigitSym :: Natural ~> Char -data ShowNatBinaryDigitSym d -type instance App ShowNatBinaryDigitSym d = ShowNatBinaryDigit d - -type family ShowNatOctalDigit (d :: Natural) :: Char where - ShowNatOctalDigit 0 = '0' - ShowNatOctalDigit 1 = '1' - ShowNatOctalDigit 2 = '2' - ShowNatOctalDigit 3 = '3' - ShowNatOctalDigit 4 = '4' - ShowNatOctalDigit 5 = '5' - ShowNatOctalDigit 6 = '6' - ShowNatOctalDigit 7 = '7' - -type ShowNatOctalDigitSym :: Natural ~> Char -data ShowNatOctalDigitSym d -type instance App ShowNatOctalDigitSym d = ShowNatOctalDigit d - -type family ShowNatDecimalDigit (d :: Natural) :: Char where - ShowNatDecimalDigit 0 = '0' - ShowNatDecimalDigit 1 = '1' - ShowNatDecimalDigit 2 = '2' - ShowNatDecimalDigit 3 = '3' - ShowNatDecimalDigit 4 = '4' - ShowNatDecimalDigit 5 = '5' - ShowNatDecimalDigit 6 = '6' - ShowNatDecimalDigit 7 = '7' - ShowNatDecimalDigit 8 = '8' - ShowNatDecimalDigit 9 = '9' - -type ShowNatDecimalDigitSym :: Natural ~> Char -data ShowNatDecimalDigitSym d -type instance App ShowNatDecimalDigitSym d = ShowNatDecimalDigit d - -type family ShowNatHexDigitLower (d :: Natural) :: Char where - ShowNatHexDigitLower 0 = '0' - ShowNatHexDigitLower 1 = '1' - ShowNatHexDigitLower 2 = '2' - ShowNatHexDigitLower 3 = '3' - ShowNatHexDigitLower 4 = '4' - ShowNatHexDigitLower 5 = '5' - ShowNatHexDigitLower 6 = '6' - ShowNatHexDigitLower 7 = '7' - ShowNatHexDigitLower 8 = '8' - ShowNatHexDigitLower 9 = '9' - ShowNatHexDigitLower 10 = 'a' - ShowNatHexDigitLower 11 = 'b' - ShowNatHexDigitLower 12 = 'c' - ShowNatHexDigitLower 13 = 'd' - ShowNatHexDigitLower 14 = 'e' - ShowNatHexDigitLower 15 = 'f' - -type ShowNatHexDigitLowerSym :: Natural ~> Char -data ShowNatHexDigitLowerSym d -type instance App ShowNatHexDigitLowerSym d = ShowNatHexDigitLower d - -type family ShowNatHexDigitUpper (d :: Natural) :: Char where - ShowNatHexDigitUpper 0 = '0' - ShowNatHexDigitUpper 1 = '1' - ShowNatHexDigitUpper 2 = '2' - ShowNatHexDigitUpper 3 = '3' - ShowNatHexDigitUpper 4 = '4' - ShowNatHexDigitUpper 5 = '5' - ShowNatHexDigitUpper 6 = '6' - ShowNatHexDigitUpper 7 = '7' - ShowNatHexDigitUpper 8 = '8' - ShowNatHexDigitUpper 9 = '9' - ShowNatHexDigitUpper 10 = 'A' - ShowNatHexDigitUpper 11 = 'B' - ShowNatHexDigitUpper 12 = 'C' - ShowNatHexDigitUpper 13 = 'D' - ShowNatHexDigitUpper 14 = 'E' - ShowNatHexDigitUpper 15 = 'F' - -type ShowNatHexDigitUpperSym :: Natural ~> Char -data ShowNatHexDigitUpperSym d -type instance App ShowNatHexDigitUpperSym d = ShowNatHexDigitUpper d +sShowNatBase' + :: SNat base -> Lam SNat SChar showDigit -> SSymbol acc -> SNat n + -> SSymbol (ShowNatBase' base showDigit acc n) +sShowNatBase' sbase sShowDigit sacc sn = + testEqElse sn (SNat @0) sacc + $ unsafeCoerce $ + sShowNatBase' sbase sShowDigit + (sConsSymbol (sShowDigit @@ (sn `sMod` sbase)) sacc) + (sn `sDiv` sbase) diff --git a/src/TypeLevelShow/Natural/Digit.hs b/src/TypeLevelShow/Natural/Digit.hs new file mode 100644 --- /dev/null +++ b/src/TypeLevelShow/Natural/Digit.hs @@ -0,0 +1,118 @@ +{-# LANGUAGE UndecidableInstances #-} -- for ErrorPDoc + +{- | Unsafe 'Natural' digit renderers. + +These are used by "TypeLevelShow.Natural", where modulo arithmetic guarantees +that they are not used unsafely. +-} + +module TypeLevelShow.Natural.Digit + ( ShowNatDigitHexLower, ShowNatDigitHexLowerSym, sShowNatDigitHexLower + , ShowNatDigitHexUpper, ShowNatDigitHexUpperSym, sShowNatDigitHexUpper + , ENotDigitOfBase + ) where + +import GHC.TypeNats +import DeFun.Core +import Singleraeh.Equality ( testEqElse ) +import TypeLevelShow.Doc +import GHC.TypeLits hiding ( ErrorMessage(..) ) + +-- | Type-level error message displayed when a digit renderer receives a +-- digit not present in the base it handles. +-- +-- Note that we can't show the digit, unless we use 'ShowType'. Which +-- type-level-show is about avoiding. Not really an issue, it should be clear in +-- the type error. +type ENotDigitOfBase base = Text "got non-" :<>: Text base :<>: Text " digit" + +-- | Return the associated lower-case 'Char' for a 'Natural' hexadecimal digit. +-- +-- Unsafe. Must be called with 0-15. +type family ShowNatDigitHexLower (d :: Natural) :: Char where + ShowNatDigitHexLower 0 = '0' + ShowNatDigitHexLower 1 = '1' + ShowNatDigitHexLower 2 = '2' + ShowNatDigitHexLower 3 = '3' + ShowNatDigitHexLower 4 = '4' + ShowNatDigitHexLower 5 = '5' + ShowNatDigitHexLower 6 = '6' + ShowNatDigitHexLower 7 = '7' + ShowNatDigitHexLower 8 = '8' + ShowNatDigitHexLower 9 = '9' + ShowNatDigitHexLower 10 = 'a' + ShowNatDigitHexLower 11 = 'b' + ShowNatDigitHexLower 12 = 'c' + ShowNatDigitHexLower 13 = 'd' + ShowNatDigitHexLower 14 = 'e' + ShowNatDigitHexLower 15 = 'f' + ShowNatDigitHexLower n = ErrorPDoc (ENotDigitOfBase "hexadecimal") + +type ShowNatDigitHexLowerSym :: Natural ~> Char +data ShowNatDigitHexLowerSym d +type instance App ShowNatDigitHexLowerSym d = ShowNatDigitHexLower d + +sShowNatDigitHexLower :: Lam SNat SChar ShowNatDigitHexLowerSym +sShowNatDigitHexLower = Lam $ \sn -> + testEqElse sn (SNat @0) (SChar @'0') + $ testEqElse sn (SNat @1) (SChar @'1') + $ testEqElse sn (SNat @2) (SChar @'2') + $ testEqElse sn (SNat @3) (SChar @'3') + $ testEqElse sn (SNat @4) (SChar @'4') + $ testEqElse sn (SNat @5) (SChar @'5') + $ testEqElse sn (SNat @6) (SChar @'6') + $ testEqElse sn (SNat @7) (SChar @'7') + $ testEqElse sn (SNat @8) (SChar @'8') + $ testEqElse sn (SNat @9) (SChar @'9') + $ testEqElse sn (SNat @10) (SChar @'a') + $ testEqElse sn (SNat @11) (SChar @'b') + $ testEqElse sn (SNat @12) (SChar @'c') + $ testEqElse sn (SNat @13) (SChar @'d') + $ testEqElse sn (SNat @14) (SChar @'e') + $ testEqElse sn (SNat @15) (SChar @'f') + $ errorPDoc @(ENotDigitOfBase "hexadecimal") + +-- | Return the associated upper-case 'Char' for a 'Natural' hexadecimal digit. +-- +-- Unsafe. Must be called with 0-15. +type family ShowNatDigitHexUpper (d :: Natural) :: Char where + ShowNatDigitHexUpper 0 = '0' + ShowNatDigitHexUpper 1 = '1' + ShowNatDigitHexUpper 2 = '2' + ShowNatDigitHexUpper 3 = '3' + ShowNatDigitHexUpper 4 = '4' + ShowNatDigitHexUpper 5 = '5' + ShowNatDigitHexUpper 6 = '6' + ShowNatDigitHexUpper 7 = '7' + ShowNatDigitHexUpper 8 = '8' + ShowNatDigitHexUpper 9 = '9' + ShowNatDigitHexUpper 10 = 'A' + ShowNatDigitHexUpper 11 = 'B' + ShowNatDigitHexUpper 12 = 'C' + ShowNatDigitHexUpper 13 = 'D' + ShowNatDigitHexUpper 14 = 'E' + ShowNatDigitHexUpper 15 = 'F' + +type ShowNatDigitHexUpperSym :: Natural ~> Char +data ShowNatDigitHexUpperSym d +type instance App ShowNatDigitHexUpperSym d = ShowNatDigitHexUpper d + +sShowNatDigitHexUpper :: Lam SNat SChar ShowNatDigitHexUpperSym +sShowNatDigitHexUpper = Lam $ \sn -> + testEqElse sn (SNat @0) (SChar @'0') + $ testEqElse sn (SNat @1) (SChar @'1') + $ testEqElse sn (SNat @2) (SChar @'2') + $ testEqElse sn (SNat @3) (SChar @'3') + $ testEqElse sn (SNat @4) (SChar @'4') + $ testEqElse sn (SNat @5) (SChar @'5') + $ testEqElse sn (SNat @6) (SChar @'6') + $ testEqElse sn (SNat @7) (SChar @'7') + $ testEqElse sn (SNat @8) (SChar @'8') + $ testEqElse sn (SNat @9) (SChar @'9') + $ testEqElse sn (SNat @10) (SChar @'A') + $ testEqElse sn (SNat @11) (SChar @'B') + $ testEqElse sn (SNat @12) (SChar @'C') + $ testEqElse sn (SNat @13) (SChar @'D') + $ testEqElse sn (SNat @14) (SChar @'E') + $ testEqElse sn (SNat @15) (SChar @'F') + $ errorPDoc @(ENotDigitOfBase "hexadecimal") diff --git a/type-level-show.cabal b/type-level-show.cabal --- a/type-level-show.cabal +++ b/type-level-show.cabal @@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack name: type-level-show -version: 0.1.1 +version: 0.2.0 synopsis: Utilities for writing Show-like type families description: Please see README.md. category: Types, Data @@ -19,8 +19,6 @@ tested-with: GHC==9.8 , GHC==9.6 - , GHC==9.4 - , GHC==9.2 extra-source-files: README.md CHANGELOG.md @@ -33,6 +31,7 @@ exposed-modules: TypeLevelShow.Doc TypeLevelShow.Natural + TypeLevelShow.Natural.Digit TypeLevelShow.Utils other-modules: Paths_type_level_show @@ -53,4 +52,5 @@ build-depends: base >=4.16 && <5 , defun-core ==0.1.* + , singleraeh ==0.1.* default-language: GHC2021