Skip to content

Commit

Permalink
Refactor CanHold(Un)Signed Typeclass Instances (#23)
Browse files Browse the repository at this point in the history
- Avoided redundant transitive instances by doing type-level natural
number comparisons
- Use custom type errors to explain why the instance is not available 
- The downside is that the constraints are not extensible - i.e. users
cannot create their own instances for their own numeric types. I think
the only way to solve this while keeping the nice type errors would be
to rely on overlapping instances (but there might be a trick that I am
unaware of)

Note that GHC now (as of `9.8.1`) supports a slightly more principled
way of adding custom type errors via `Unsatisfiable` constraints. The
main trouble with trying to use it here is `BitWidth` (which doesn't
return `Constraint`). We could create another constraint family with an
appropriate error message, or perhaps have it take a `b :: Bits`
standing for the return value and return equality constraints (`b ~
B8`/`b ~ B16`, etc...) in the successful cases, hoping Haskell's
constraint solver makes everything work out nicely.
  • Loading branch information
j-mie6 authored Jan 17, 2024
2 parents 58a0689 + bc23641 commit 3099e8c
Showing 1 changed file with 78 additions and 41 deletions.
119 changes: 78 additions & 41 deletions src/Text/Gigaparsec/Token/Numeric.hs
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
{-# LANGUAGE Safe #-}
{-# LANGUAGE DataKinds, KindSignatures, ConstraintKinds, MultiParamTypeClasses, AllowAmbiguousTypes, FlexibleInstances, FlexibleContexts, UndecidableInstances, ApplicativeDo #-}
{-# LANGUAGE DataKinds, KindSignatures, ConstraintKinds, MultiParamTypeClasses, AllowAmbiguousTypes, FlexibleInstances, FlexibleContexts, UndecidableInstances, ApplicativeDo, TypeFamilies, TypeOperators, CPP #-}
-- TODO: refine, move to Internal
module Text.Gigaparsec.Token.Numeric (module Text.Gigaparsec.Token.Numeric) where

Expand All @@ -22,81 +22,118 @@ import Numeric.Natural (Natural)
import Data.Proxy (Proxy(Proxy))
import Control.Monad (when, unless)

#if __GLASGOW_HASKELL__ >= 904

import GHC.TypeLits (type (<=?), Nat)
import GHC.TypeError (TypeError, ErrorMessage(Text, (:<>:), ShowType), Assert)

#else

import GHC.TypeLits (type (<=?), Nat, TypeError, ErrorMessage(Text, (:<>:), ShowType))

type Assert :: Bool -> Constraint -> Constraint
type family Assert b c where
Assert 'True _ = ()
Assert 'False c = c

#endif

type Bits :: *
data Bits = B8 | B16 | B32 | B64

type BitWidth :: * -> Bits
type family BitWidth t where
BitWidth Integer = 'B64
BitWidth Int = 'B64
BitWidth Word = 'B64
BitWidth Word64 = 'B64
BitWidth Natural = 'B64
BitWidth Int32 = 'B32
BitWidth Word32 = 'B32
BitWidth Int16 = 'B16
BitWidth Word16 = 'B16
BitWidth Int8 = 'B8
BitWidth Word8 = 'B8
BitWidth a
= TypeError ('Text "The type '" ' :<>: 'ShowType a
' :<>: 'Text "' is not a numeric type supported by Gigaparsec")

type Signedness :: *
data Signedness = Signed | Unsigned

type IsSigned :: * -> Signedness -> Constraint
type family IsSigned t s where
IsSigned Integer 'Signed = ()
IsSigned Int 'Signed = ()
IsSigned Word 'Unsigned = ()
IsSigned Word64 'Unsigned = ()
IsSigned Natural 'Unsigned = ()
IsSigned Int32 'Signed = ()
IsSigned Word32 'Unsigned = ()
IsSigned Int16 'Signed = ()
IsSigned Word16 'Unsigned = ()
IsSigned Int8 'Signed = ()
IsSigned Word8 'Unsigned = ()
IsSigned a 'Signed
= TypeError ('Text "The type '" ' :<>: 'ShowType a ' :<>: 'Text "' does not hold signed data")
IsSigned a 'Unsigned
= TypeError ('Text "The type '" ' :<>: 'ShowType a
' :<>: 'Text "' does not hold unsigned data")

type ShowBits :: Bits -> ErrorMessage
type ShowBits b = 'ShowType (BitsNat b)

-- This is intentionally not a type alias. On GHC versions < 9.4.1 it appears that TypeErrors are
-- reported slightly more eagerly and we get an error on this definition because
-- > BitsNat b <=? BitsNat (BitWidth t)
-- cannot be solved
type SatisfiesBound :: * -> Bits -> Constraint
type family SatisfiesBound t b where
SatisfiesBound t b
= Assert (BitsNat b <=? BitsNat (BitWidth t)) (TypeError ('Text "The type '"
' :<>: 'ShowType t ' :<>: 'Text "' does not have enough bit-width to store "
' :<>: ShowBits (BitWidth t) ' :<>: 'Text " bits of data (can only store up to "
' :<>: ShowBits b ' :<>: 'Text " bits)."))

type BitBounds :: Bits -> Constraint
class BitBounds b where
upperSigned :: Integer
lowerSigned :: Integer
upperUnsigned :: Integer
bits :: Int
type BitsNat b :: Nat
instance BitBounds 'B8 where
upperSigned = fromIntegral (maxBound @Int8)
lowerSigned = fromIntegral (minBound @Int8)
upperUnsigned = fromIntegral (maxBound @Word8)
bits = 8
type BitsNat 'B8 = 8
instance BitBounds 'B16 where
upperSigned = fromIntegral (maxBound @Int16)
lowerSigned = fromIntegral (minBound @Int16)
upperUnsigned = fromIntegral (maxBound @Word16)
bits = 16
type BitsNat 'B16 = 16
instance BitBounds 'B32 where
upperSigned = fromIntegral (maxBound @Int32)
lowerSigned = fromIntegral (minBound @Int32)
upperUnsigned = fromIntegral (maxBound @Word32)
bits = 32
type BitsNat 'B32 = 32
instance BitBounds 'B64 where
upperSigned = fromIntegral (maxBound @Int64)
lowerSigned = fromIntegral (minBound @Int64)
upperUnsigned = fromIntegral (maxBound @Word64)
bits = 64
type BitsNat 'B64 = 64

type CanHoldSigned :: Bits -> * -> Constraint
class (BitBounds b, Num a) => CanHoldSigned b a where
instance CanHoldSigned 'B8 Int8
instance CanHoldSigned 'B8 Int16
instance CanHoldSigned 'B8 Int32
instance CanHoldSigned 'B8 Int64
instance CanHoldSigned 'B8 Int
instance CanHoldSigned 'B8 Integer
instance CanHoldSigned 'B16 Int16
instance CanHoldSigned 'B16 Int32
instance CanHoldSigned 'B16 Int64
instance CanHoldSigned 'B16 Int
instance CanHoldSigned 'B16 Integer
instance CanHoldSigned 'B32 Int32
instance CanHoldSigned 'B32 Int64
instance CanHoldSigned 'B32 Int
instance CanHoldSigned 'B32 Integer
instance CanHoldSigned 'B64 Int64
instance CanHoldSigned 'B64 Int
instance CanHoldSigned 'B64 Integer
instance (BitBounds b, Num a, IsSigned a 'Signed, SatisfiesBound a b) => CanHoldSigned b a

type CanHoldUnsigned :: Bits -> * -> Constraint
class (BitBounds b, Num a) => CanHoldUnsigned b a where
instance CanHoldUnsigned 'B8 Word8
instance CanHoldUnsigned 'B8 Word16
instance CanHoldUnsigned 'B8 Word32
instance CanHoldUnsigned 'B8 Word64
instance CanHoldUnsigned 'B8 Word
instance CanHoldUnsigned 'B8 Integer
instance CanHoldUnsigned 'B8 Natural
instance CanHoldUnsigned 'B16 Word16
instance CanHoldUnsigned 'B16 Word32
instance CanHoldUnsigned 'B16 Word64
instance CanHoldUnsigned 'B16 Word
instance CanHoldUnsigned 'B16 Integer
instance CanHoldUnsigned 'B16 Natural
instance CanHoldUnsigned 'B32 Word32
instance CanHoldUnsigned 'B32 Word64
instance CanHoldUnsigned 'B32 Word
instance CanHoldUnsigned 'B32 Integer
instance CanHoldUnsigned 'B32 Natural
instance CanHoldUnsigned 'B64 Word64
instance CanHoldUnsigned 'B64 Word
instance CanHoldUnsigned 'B64 Integer
instance CanHoldUnsigned 'B64 Natural
instance (BitBounds b, Num a, IsSigned a 'Unsigned, SatisfiesBound a b) => CanHoldUnsigned b a

type IntegerParsers :: (Bits -> * -> Constraint) -> *
data IntegerParsers canHold = IntegerParsers { decimal :: Parsec Integer
Expand Down

0 comments on commit 3099e8c

Please sign in to comment.