store
store copied to clipboard
Type system information for statically known data size
It would be really cool to have compiletime info about datatype size. This has the potential to make both the generics and TH derivations more efficient. Certainly for TH it would cause the compiler to do less overall work. It'd also allow us to use functions that demand ConstSize and have them fail statically. This way the user can't accidentally make their values VarSize (can be much less efficient).
We might need to use some TH hacks to reify runtime Storable info as compiletime type info.
I'm imagining something like the following, using type nats, data kinds, and type families:
-- Can I use Nat here? You know what I mean.
data StaticSize = KnownSize Nat | UnknownSize
class Store a where
type StoreSize :: a -> StaticSize
type StoreSize a = UnknownSize
-- ...
type instance StoreSize () = 'KnownSize 0
type instance StoreSize Int32 = 'KnownSize 4
-- etc
Probably good to have it as an associated type family, so that it can be given the default of
We'd also likely want the Size a
type be a GADT that enforces that ConstSize
is yielded when StoreSize a ~ KnownSize n
. Marking this "breaking change" as such.
I came here to open this same Issue and fortunately found yours first. My motivation is to be able to use the type-checker to ensure that some serialization uses the more efficient ConstSize
path.
I suggest the following.
type family StoreConstSize a :: Maybe Nat
data Size :: * -> * where
ConstSize :: (StoreConstSize a ~ 'Just n,KnownNat n) => Proxy# n -> Size a
VarSize :: (StoreConstSize a ~ 'Nothing) => !(a -> Int) -> Size a
Though I'm worried that KnownNat
essentially being Integer
may cost performance. Thus, the following ought to be a better performing middle-ground.
type family StoreConstSize a :: Bool
data Size :: * -> * where
ConstSize :: (StoreConstSize a ~ 'True) => !Int -> Size a
VarSize :: (StoreConstSize a ~ 'False) => !(a -> Int) -> Size a
And last, I'm not sure how the pattern exhaustiveness checker will handle the new Size
. If it's troublesome, you may want to consider a route using a data family for Size
instead of a GADT.