From 91443f21a4729bb672fdef3455de9f678298b377 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Thu, 9 Jan 2025 18:43:44 +0100 Subject: [PATCH] sing.hs without separate Mode --- sing.hs | 52 ++++++++++++++++++---------------------------------- 1 file changed, 18 insertions(+), 34 deletions(-) diff --git a/sing.hs b/sing.hs index 5fc21b2..3ac8202 100644 --- a/sing.hs +++ b/sing.hs @@ -1,49 +1,33 @@ {-# language GHC2024, AllowAmbiguousTypes, TypeAbstractions #-} --- AllowAmbiguousTypes for dispatch :: Dispatchable d => String +import Data.Maybe +import Data.Type.Equality +import GHC.TypeLits import System.Environment main = do [s] <- getArgs - putStrLn $ maybe "not found" dispatchDyn $ fromString s - - -data Mode = A | B - -data SMode m where SA :: SMode A; SB :: SMode B - -class KnownMode m where knownMode :: SMode m -instance KnownMode A where knownMode = SA -instance KnownMode B where knownMode = SB - - -withMode :: Mode -> (forall m. KnownMode m => r) -> r -withMode A f = f @A -withMode B f = f @B - - -fromString :: String -> Maybe Mode -fromString "a" = Just A -fromString "b" = Just B -fromString _ = Nothing + putStrLn $ fromMaybe "some default value" $ dispatchDyn s class Dispatchable d where dispatch :: String -instance Dispatchable A where dispatch = "A" -instance Dispatchable B where dispatch = "B" +instance Dispatchable "a" where dispatch = "A" +instance Dispatchable "b" where dispatch = "B" -dispatchDyn :: Mode -> String -dispatchDyn m = withMode m $ \ @m -> dispatch @m \\ allModesDispatchable @m +dispatchDyn :: String -> Maybe String +dispatchDyn m = withSomeSSymbol m $ \(SSymbol @m) -> + case stringDispatchable @m of + Just Dict -> Just $ dispatch @m + Nothing -> Nothing -allModesDispatchable :: KnownMode m :- Dispatchable m -allModesDispatchable @m = - Sub $ case knownMode @m of SA -> Dict; SB -> Dict +stringDispatchable :: KnownSymbol m => Maybe (Dict (Dispatchable m)) +stringDispatchable @m + | Just Refl <- is @"a" @m = Just Dict + | Just Refl <- is @"b" @m = Just Dict + | otherwise = Nothing + where is :: (KnownSymbol a, KnownSymbol b) => Maybe (a :~: b) + is @a @b = sameSymbol (SSymbol @a) (SSymbol @b) --- this stuff taken from the `constraints` package data Dict c = c => Dict -data c :- d = Sub (c => Dict d) - -(\\) :: c => (d => r) -> c :- d -> r -r \\ Sub Dict = r