-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
start on contravariant BLen (like store)
- Loading branch information
Showing
5 changed files
with
192 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,101 @@ | ||
{-# LANGUAGE UndecidableInstances #-} -- for 'CBLenly', 'TypeError' | ||
{-# LANGUAGE AllowAmbiguousTypes #-} -- for 'cblen' | ||
|
||
module Binrep.BLen.Ask where | ||
|
||
import Raehik.Contravariant.Ask | ||
import Data.Monoid ( Sum(Sum) ) | ||
import Data.Functor.Contravariant.Divisible ( divide ) | ||
|
||
import Binrep.CBLen | ||
import GHC.TypeNats | ||
import Util.TypeNats ( natValInt ) | ||
|
||
import Data.ByteString qualified as B | ||
import Data.Word | ||
import Data.Int | ||
|
||
type Builder = Ask (Sum Int) | ||
|
||
blenConst :: Int -> Builder a | ||
blenConst = Ignore . Sum | ||
|
||
class BLen a where blen :: Builder a | ||
|
||
-- | Deriving via wrapper for types which may derive a 'BLen' instance through | ||
-- an existing 'IsCBLen' instance. | ||
-- | ||
-- Examples of such types include machine integers, and explicitly-sized types | ||
-- (e.g. "Binrep.Type.Sized"). | ||
newtype CBLenly a = CBLenly { unCBLenly :: a } | ||
instance KnownNat (CBLen a) => BLen (CBLenly a) where | ||
{-# INLINE blen #-} | ||
blen = blenConst (cblen @a) | ||
|
||
-- | Reify a type's constant byte length to the term level. | ||
cblen :: forall a n. (n ~ CBLen a, KnownNat n) => Int | ||
cblen = natValInt @n | ||
{-# INLINE cblen #-} | ||
|
||
{- | ||
instance GenericContra (Ask (Sum Int)) where | ||
type GenericContraC (Ask (Sum Int)) a = BLen a | ||
genericContraF = contramap getSum blen | ||
-- | Measure the byte length of a term of the non-sum type @a@ via its 'Generic' | ||
-- instance. | ||
blenGenericNonSum | ||
:: forall {cd} {f} {asserts} a | ||
. ( Generic a, Rep a ~ D1 cd f, GFoldMapNonSum (BLen' Int) f | ||
, asserts ~ '[ 'NoEmpty, 'NoSum], ApplyGCAsserts asserts f) | ||
=> a -> Int | ||
blenGenericNonSum = getBLen' . genericFoldMapNonSum @asserts | ||
-- | Measure the byte length of a term of the sum type @a@ via its 'Generic' | ||
-- instance. | ||
-- | ||
-- You must provide a function to obtain the byte length for the prefix tag, via | ||
-- inspecting the reified constructor names. This is regrettably inefficient. | ||
-- Alas. Do write your own instance if you want better performance! | ||
blenGenericSum | ||
:: forall {cd} {f} {asserts} a | ||
. (Generic a, Rep a ~ D1 cd f, GFoldMapSum 'SumOnly (BLen' Int) f | ||
, asserts ~ '[ 'NoEmpty, 'NeedSum], ApplyGCAsserts asserts f) | ||
=> (String -> Int) -> a -> Int | ||
blenGenericSum f = getBLen' . genericFoldMapSum @'SumOnly @asserts (BLen' <$> f) | ||
instance TypeError ENoEmpty => BLen Void where blen = undefined | ||
instance TypeError ENoSum => BLen (Either a b) where blen = undefined | ||
-} | ||
|
||
-- | Unit type has length 0. | ||
instance BLen () where | ||
{-# INLINE blen #-} | ||
blen = blenConst 0 | ||
|
||
-- | Sum tuples. | ||
instance (BLen l, BLen r) => BLen (l, r) where | ||
{-# INLINE blen #-} | ||
blen = divide id blen blen | ||
|
||
-- | _O(n)_ Sum the length of each element of a list. | ||
instance BLen a => BLen [a] where | ||
{-# INLINE blen #-} | ||
blen = Use $ \as -> case blen @a of | ||
Ignore (Sum n) -> Sum $ n * length as | ||
Use fa -> foldMap fa as | ||
|
||
-- | Length of a bytestring is fairly obvious. | ||
instance BLen B.ByteString where | ||
{-# INLINE blen #-} | ||
blen = Use (Sum . B.length) | ||
|
||
-- Machine integers have a constant byte length. | ||
deriving via CBLenly Word8 instance BLen Word8 | ||
deriving via CBLenly Int8 instance BLen Int8 | ||
deriving via CBLenly Word16 instance BLen Word16 | ||
deriving via CBLenly Int16 instance BLen Int16 | ||
deriving via CBLenly Word32 instance BLen Word32 | ||
deriving via CBLenly Int32 instance BLen Int32 | ||
deriving via CBLenly Word64 instance BLen Word64 | ||
deriving via CBLenly Int64 instance BLen Int64 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,84 @@ | ||
-- | A funky contravariant functor I found which has its uses in binrep. | ||
|
||
module Raehik.Contravariant.Ask where | ||
|
||
import Data.Functor.Contravariant | ||
import Data.Functor.Contravariant.Divisible | ||
import Data.Void ( absurd ) | ||
|
||
{- | Obtain an @m@ either by mapping on @a@, or simply unwrapping a plain @m@. | ||
This type explicitly encodes the pattern where we have an operation on a type | ||
@a@, but sometimes we may not need to look at the argument to know the answer | ||
-- it's constant, independent of the argument's value. Usually, you do this | ||
by ignoring the argument with @_@ or @const@. Here, you may write 'Ignore' and | ||
never even accept an argument. Of course, you need to provide an @a@ to extract | ||
@m@, but this explicit "no argument thank you" might enable better combination | ||
behaviour. (I actually have no idea.) | ||
This is a contravariant functor. They are weird. You may combine them using | ||
operations over 'Contravariant's. They are funky. Hoogle 'Divisible'. | ||
@m@ should be a 'Monoid'. | ||
I don't know if it's useful, but this type is equivalent to: | ||
* 'Op' with an extra constructor. | ||
* @'Either' (a -> m) m@. | ||
* @Size a@ type in the store library, when @m ~ 'Sum' 'Int'@ | ||
TODO: unsure on type/cstr name. other ideas: need/known? | ||
-} | ||
data Ask m a | ||
-- | @m@ depends on @a@. | ||
= Use (a -> m) | ||
|
||
-- | @m@ is independent of @a@. | ||
-- | ||
-- TODO store used ! here | ||
| Ignore m | ||
|
||
instance Contravariant (Ask m) where | ||
contramap f = \case | ||
Ignore m -> Ignore m | ||
Use g -> Use $ \a -> g (f a) | ||
|
||
instance Monoid m => Divisible (Ask m) where | ||
conquer = Ignore mempty | ||
divide toLR ls rs = case (ls, rs) of | ||
(Ignore lc, Ignore rc) -> Ignore $ lc <> rc | ||
(Use lv, Ignore rc) -> Use $ \a -> | ||
let (l, _) = toLR a | ||
in lv l <> rc | ||
(Ignore lc, Use rv) -> Use $ \a -> | ||
let (_, r) = toLR a | ||
in lc <> rv r | ||
(Use lv, Use rv) -> Use $ \a -> | ||
let (l, r) = toLR a | ||
in lv l <> rv r | ||
|
||
instance Monoid m => Decidable (Ask m) where | ||
lose f = Use $ \a -> absurd (f a) | ||
choose split ls rs = case (ls, rs) of | ||
(Ignore lc, Ignore rc) -> Ignore $ lc <> rc | ||
(Use lv, Ignore rc) -> Use $ \a -> | ||
case split a of | ||
Left l -> lv l | ||
Right{} -> rc | ||
(Ignore lc, Use rv) -> Use $ \a -> | ||
case split a of | ||
Left{} -> lc | ||
Right r -> rv r | ||
(Use lv, Use rv) -> Use $ \a -> | ||
case split a of | ||
Left l -> lv l | ||
Right r -> rv r | ||
|
||
instance Semigroup m => Semigroup (Ask m a) where | ||
l <> r = case (l, r) of | ||
(Ignore lc, Ignore rc) -> Ignore $ lc <> rc | ||
(Use lv, Ignore rc) -> Use $ \a -> lv a <> rc | ||
(Ignore lc, Use rv) -> Use $ \a -> lc <> rv a | ||
(Use lv, Use rv) -> Use $ \a -> lv a <> rv a | ||
|
||
instance Monoid m => Monoid (Ask m a) where mempty = Ignore mempty |