MonomorphicRegistry.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Type.Equality
import GHC.Types qualified as Haskell

data Type
  = Bool
  | Function Type Type
  | Int
  | String

type (->>) a b = Function a b

type family Embed (t :: Type) :: Haskell.Type where
  Embed 'Bool     = Bool
  Embed (a ->> b) = Embed a -> Embed b
  Embed 'Int      = Int
  Embed 'String   = String

data TypeRepr :: Type -> Haskell.Type where
  BoolR     :: TypeRepr 'Bool
  FunctionR :: TypeRepr a -> TypeRepr b -> TypeRepr (a ->> b)
  IntR      :: TypeRepr 'Int
  StringR   :: TypeRepr 'String

infixr ->>>
(->>>) = FunctionR

eqTypeRepr :: TypeRepr ty1 -> TypeRepr ty2 -> Maybe (ty1 :~: ty2)
eqTypeRepr BoolR   BoolR   = Just Refl
eqTypeRepr (FunctionR a1 a2) (FunctionR b1 b2) = do
  Refl <- eqTypeRepr a1 b1
  Refl <- eqTypeRepr a2 b2
  Just Refl
eqTypeRepr IntR    IntR    = Just Refl
eqTypeRepr StringR StringR = Just Refl
eqTypeRepr _ _ = Nothing

data RegistryEntry = forall ty. RegistryEntry
  { entryName  :: String
  , entryType  :: TypeRepr ty
  , entryValue :: Embed ty
  }

type Registry = [RegistryEntry]

find :: Registry -> String -> TypeRepr ty -> Maybe (Embed ty)
find [] _ _ = Nothing
find (RegistryEntry eName eType eValue : entries) name ty
  | eName /= name = find entries name ty
  | otherwise     =
    case eqTypeRepr eType ty of 
      Just Refl -> Just eValue
      _         -> find entries name ty

addInt :: Int -> Int -> Int
addInt = (+)

addString :: String -> String -> String
addString = (<>)

myRegistry :: Registry
myRegistry =
  [ RegistryEntry "add" (IntR ->>> IntR ->>> IntR)          addInt
  , RegistryEntry "add" (StringR ->>> StringR ->>> StringR) addString
  ]

main = print $ do 
  add <- find myRegistry "add" (StringR ->>> StringR ->>> StringR)
  return $ add "abc" "def"