Search code examples
haskelltypesbinary

Haskell binary datatype of specific bitwidth


I would like to create a datatype representing a binary number of specific bit width.

So a type bin3 --> 0bXXX, bin7 --> 0bXXXXXXX

Does anyone know how to do this? I have tried to install packages such as bv-sized but they will not build correctly. I do not need much functionality so I thought I could implement my own.

The error I got when trying to install bv-sized was

$ cabal install bv-sized
Resolving dependencies...
Configuring parameterized-utils-2.1.2.0...
Building parameterized-utils-2.1.2.0...
Failed to install parameterized-utils-2.1.2.0
Build log ( /home/.../.cabal/logs/ghc-8.2.2/parameterized-utils-2.1.2.0-4VdYssETRDcLceu2pgYcjQ.log ):
cabal: Entering directory '/tmp/cabal-tmp-99266/parameterized-utils-2.1.2.0'
Configuring parameterized-utils-2.1.2.0...
Preprocessing library for parameterized-utils-2.1.2.0..
Building library for parameterized-utils-2.1.2.0..
[ 1 of 32] Compiling Data.Parameterized.Compose ( src/Data/Parameterized/Compose.hs, dist/build/Data/Parameterized/Compose.o )

src/Data/Parameterized/Compose.hs:30:45: error:
    Type variable ‘k’ used in a kind.
    Did you mean to use TypeInType?
    the type signature for ‘testEqualityComposeBare’
   |
30 | testEqualityComposeBare :: forall k l (f :: k -> *) (g :: l -> k) x y.
   |                                             ^

src/Data/Parameterized/Compose.hs:30:59: error:
    Type variable ‘l’ used in a kind.
    Did you mean to use TypeInType?
    the type signature for ‘testEqualityComposeBare’
   |
30 | testEqualityComposeBare :: forall k l (f :: k -> *) (g :: l -> k) x y.
   |                                                           ^

src/Data/Parameterized/Compose.hs:30:64: error:
    Type variable ‘k’ used in a kind.
    Did you mean to use TypeInType?
    the type signature for ‘testEqualityComposeBare’
   |
30 | testEqualityComposeBare :: forall k l (f :: k -> *) (g :: l -> k) x y.
   |                                                                ^
cabal: Leaving directory '/tmp/cabal-tmp-99266/parameterized-utils-2.1.2.0'
cabal: Error: some packages failed to install:
bv-sized-1.0.3-Ip13iwUWQ7u421I8e2amlq depends on bv-sized-1.0.3 which failed
to install.
parameterized-utils-2.1.2.0-4VdYssETRDcLceu2pgYcjQ failed during the building
phase. The exception was:
ExitFailure 1

GHC 8.2.2


Solution

  • Given that there are at most 64 bits, we can easily encode that on a 64-bit word. This would mean that we can work with:

    {-# LANGUAGE DataKinds, KindSignatures #-}
    
    import Data.Word(Word64)
    import GHC.TypeNats (KnownNat, natVal)
    import Numeric.Natural (Natural)
    import Text.Printf (printf)
    
    newtype Bin (n :: Natural) = Bin Word64 deriving (Eq, Ord, Read)
    
    _sz :: KnownNat n => Bin n -> Int
    _sz = fromIntegral . natVal
    
    instance KnownNat n => Show (Bin n) where
      showsPrec d g@(Bin v) = showParen (d > 0) (("0b" ++ printf ("%0" ++ (show (_sz g)) ++ "b") v) ++)
    

    The _sz thus works with a Bin n and returns the n value as Int, regardless what the Bin n object is, this can even be undefined. And we then thus use that to show that number of bits, for example:

    ghci> Bin 3 :: Bin 3
    0b011
    ghci> Bin 3 :: Bin 5
    0b00011
    

    of course this is just a minimal example. For example it has no smart constructor. But we can complete this, with for example constructors, and extra instances to Num, Bits, etc.