type-level-show 0.1.1 → 0.2.0
raw patch · 6 files changed
+252/−116 lines, 6 filesdep +singleraeh
Dependencies added: singleraeh
Files
- CHANGELOG.md +3/−0
- README.md +1/−1
- src/TypeLevelShow/Doc.hs +74/−19
- src/TypeLevelShow/Natural.hs +53/−93
- src/TypeLevelShow/Natural/Digit.hs +118/−0
- type-level-show.cabal +3/−3
CHANGELOG.md view
@@ -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
README.md view
@@ -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
src/TypeLevelShow/Doc.hs view
@@ -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
src/TypeLevelShow/Natural.hs view
@@ -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)
+ src/TypeLevelShow/Natural/Digit.hs view
@@ -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")
type-level-show.cabal view
@@ -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