Opened 2 years ago

Last modified 22 months ago

#14255 new feature request

Type-indexed type fingerprints

Reported by: dfeuer Owned by:
Priority: normal Milestone:
Component: Core Libraries Version: 8.2.1
Keywords: Typeable Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


I have the feeling that it might well be possible to reduce the size of the trusted codebase somewhat by introducing type-indexed fingerprints. Imagine

data TypeRep (a :: k) where
    TrTyCon :: {-# UNPACK #-} !FingerprintIx a -> !TyCon -> [SomeTypeRep]
            -> TypeRep (a :: k)
    TrApp   :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
               {-# UNPACK #-} !FingerprintIx (a b)
            -> TypeRep (a :: k1 -> k2)
            -> TypeRep (b :: k1)
            -> TypeRep (a b)
    TrFun   :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
                      (a :: TYPE r1) (b :: TYPE r2).
               {-# UNPACK #-} !FingerprintIx (a -> b)
            -> TypeRep a
            -> TypeRep b
            -> TypeRep (a -> b)

We could have some primitive operations like

mkFunFP :: FingerPrintIx a -> FingerPrintIx b -> FingerPrintIx (a -> b)
mkAppFP :: FingerPrintIx (a -> b) -> FingerPrintIx a -> FingerPrintIx b

eq :: FingerPrintIx a -> FingerPrintIx b -> Maybe (a :~~: b)
eqE :: FingerPrintIx a -> FingerPrintIx b -> Either (a :~~: b -> c) (a :~~: b)

Change History (5)

comment:1 Changed 2 years ago by simonpj

I'm 100% lost. What is a fingerprint? How do you create them? How does it reduce the size of the TCB?

comment:2 in reply to:  1 Changed 2 years ago by dfeuer

Replying to simonpj:

I'm 100% lost. What is a fingerprint? How do you create them? How does it reduce the size of the TCB?

A fingerprint is just a number (a sort of hash) assigned to a type. Fingerprints are used to allow fast comparisons between TypeReps. But they're not really attached to the types they represent, and the unsafe bits of handling them are woven into the larger/more complex TypeRep code. I hypothesize that we could compact, if not technically reduce, the TCB by using a separate module for a simple newtype

newtype FingerprintIx a = FingerprintIx Fingerprint

comment:3 Changed 2 years ago by RyanGlScott

I assume that by "reduce the size of the trusted codebase", you mean eliminating uses of unsafeCoerce. But I don't see how indexing fingerprints with types would accomplish this. For example, fingerprints are used in eqTypeRep:

eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2).
             TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep a b
  | typeRepFingerprint a == typeRepFingerprint b = Just (unsafeCoerce HRefl)
  | otherwise                                    = Nothing

Are you envisioning changing this to the following?

eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2).
             TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep a b = eq (typeRepFingerprint a) (typeRepFingerprint b)

eq :: FingerPrintIx a -> FingerPrintIx b -> Maybe (a :~~: b)

If so, then that would axe one use of unsafeCoerce... but how are you planning to implement eq? I'm not sure how you would aside from using unsafeCoerce again! So we've traded one use of unsafeCoerce for another.

Perhaps I'm way off base in my assumptions, so please correct me if you had a different vision in mind.

comment:4 Changed 23 months ago by dfeuer

Whether or not we can reduce the size of the trusted code base, I think this is a good thing to offer. In particular, applications that use deserialized Dynamic very heavily, but that don't use dynApply or other reflection-based operations can be much more efficient if they stick to fingerprints instead of full TypeReps. Indexing these fingerprints by type supports a friendly and modern, though necessarily limited, API.

comment:5 Changed 22 months ago by dfeuer

Just so I don't lose the idea, we can implement a Typeable-alike for such fingerprints that leverages the existing Typeable infrastructure but avoids the cost of manipulating any more TypeReps than necessary:

data FingerprintIx (a :: k)

appFingerprintIx :: forall j k (f :: j -> k) (x :: j).
       FingerprintIx f -> FingerprintIx x -> FingerprintIx (f x)
appFingerprintIx _ _ = undefined

funFingerprintIx :: forall r1 r2 (arg :: TYPE r1) (res :: TYPE r2).
       FingerprintIx arg -> FingerprintIx res -> FingerprintIx (arg -> res)
funFingerprintIx _ _ = undefined

foo :: TypeRep a -> FingerprintIx a
foo _ = undefined

class HasFingerprintIx (a :: k) where
  fpi :: FingerprintIx a

data Expr where
  Base :: Expr  
  FunE :: Expr -> Expr -> Expr
  AppE :: Expr -> Expr -> Expr

type family From (a :: k) :: Expr where
  From (a -> b) = 'FunE (From a) (From b)
  From (f x) = 'AppE (From f) (From x)
  From x = 'Base

class HasFingerprintIx' (e :: Expr) (a :: k) where
  fpi' :: FingerprintIx a
instance Typeable a => HasFingerprintIx' 'Base a where
  fpi' = foo typeRep
instance    (HasFingerprintIx' e1 f, HasFingerprintIx' e2 x)
         => HasFingerprintIx' ('AppE e1 e2) ((f :: j -> k) x) where
  fpi' = appFingerprintIx (fpi' @_ @e1) (fpi' @_ @e2)
instance    (HasFingerprintIx' e1 arg, HasFingerprintIx' e2 res)
         => HasFingerprintIx' ('FunE e1 e2)
                    ((arg :: TYPE r1) -> (res :: TYPE r2)) where
  fpi' = funFingerprintIx (fpi' @_ @e1) (fpi' @_ @e2)

instance (e ~ From a, HasFingerprintIx' e a) => HasFingerprintIx (a :: k) where
  fpi = fpi' @_ @e
Note: See TracTickets for help on using tickets.