Typeable - A long journey to type-safe dynamic type representation

Dynamic.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}

module Type.Dynamic where

import Control.Monad
import Data.Maybe 
import Data.Map as Map
import Type.Reflection hiding (SomeTypeRep)
import Type.Reflection.Unsafe

data Dynamic where
  Dyn :: TypeRep a -> a -> Dynamic

toDynamic :: Typeable a => a -> Dynamic
toDynamic = Dyn typeRep

fromDynamic :: forall d. Typeable d => Dynamic -> Maybe d
fromDynamic (Dyn (ra :: TypeRep a) (x :: a))
  = case eqTypeRep ra (typeRep :: TypeRep d) of 
      Nothing -> Nothing
      Just HRefl -> Just x

cast :: forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast = castR (typeRep :: TypeRep a) (typeRep :: TypeRep b)

castR :: forall a b. TypeRep a -> TypeRep b -> a -> Maybe b
castR ra rb x =  do
  HRefl <- eqTypeRep ra rb
  return x

dynFst :: Dynamic -> Maybe Dynamic
dynFst (Dyn (App (App rp ra) rb) x) =
  case eqTypeRep rp (typeRep :: TypeRep (,)) of
    Just HRefl -> Just $ Dyn ra (fst x)
    Nothing -> Nothing
dynFst _ = Nothing

dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
dynApply (Dyn (App (App rf ra1) ra) f) (Dyn rx x) = do
  HRefl <- eqTypeRep rf (typeRep :: TypeRep (->))
  HRefl <- eqTypeRep ra1 rx
  return $ Dyn ra (f x)


data SomeTypeRep where
  SomeTypeRep :: TypeRep a -> SomeTypeRep
 
instance Eq SomeTypeRep where
  (==) (SomeTypeRep ra) (SomeTypeRep rb) =
    isJust $ eqTypeRep ra rb

instance Ord SomeTypeRep where
  compare (SomeTypeRep ra) (SomeTypeRep rb) =
    compareTypeRep ra rb 

compareTypeRep :: forall a b. TypeRep a -> TypeRep b -> Ordering
compareTypeRep ra rb = compare (typeRepFingerprint ra) (typeRepFingerprint rb)


type TyMap = Map SomeTypeRep Dynamic

empty' :: TyMap
empty' = Map.empty

insert :: forall a. Typeable a => a -> TyMap -> TyMap
insert a = Map.insert (SomeTypeRep ra) (Dyn ra a)
  where
    ra = typeRep :: TypeRep a

lookup :: forall a. Typeable a => TyMap -> Maybe a
lookup = fromDynamic
  <=< Map.lookup (SomeTypeRep (typeRep :: TypeRep a))

data TyTree = Empty
            | Node Dynamic TyTree TyTree

lookupTree :: forall a. TypeRep a -> TyTree -> Maybe a
lookupTree _ Empty = Nothing
lookupTree tr (Node (Dyn ra v) left right) =
  case compareTypeRep tr ra of
    EQ -> castR ra tr v
    LT -> lookupTree tr left
    GT -> lookupTree tr right