Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
import qualified Data.Dependent.Map as DM
import Data.Dependent.Sum (DSum (..))
import Data.GADT.Compare
import Data.Kind
import Data.Typeable
import Unsafe.Coerce
------------------------------------------
-- 1. The types of our problem.
-- Some arbitrary enum value.
data Label = Foo | Bar | Baz
deriving (Show, Eq, Ord, Bounded, Enum, Typeable)
-- A GADT that defines "singletons" (kinda): one constructor for each label.
data Tag (l :: Label) where
FooTag :: Tag Foo
BarTag :: Tag Bar
BazTag :: Tag Baz
deriving instance Show (Tag l)
------------------------------------------
-- 2. Example usage
-- Mapping from label to type (à la Trees That Grow).
class Show (ValueType l) => Representation (l :: Label) where
type ValueType l :: Type
instance Representation 'Foo where type ValueType 'Foo = Int
instance Representation 'Bar where type ValueType 'Bar = String
instance Representation 'Baz where type ValueType 'Baz = ()
-- Example use case: a value whose representation is parametric over the label.
data Value l where
Value :: Representation l =>
{ vName :: String
, vValue :: ValueType l
} -> Value l
deriving instance Show (Value l)
-- We want to use Tag as the key in a dependent map; the value thing is just an example.
type LabeledValueMap = DM.DMap Tag Value
-- Example usage: create a map, print its content
main :: IO ()
main = do
let dmap = DM.fromList [ FooTag :=> Value "answer" 42
, BarTag :=> Value "answer" "42"
, BazTag :=> Value "answer" ()
]
sequence_ $ do
(tag :=> value) <- DM.toList dmap
pure $ putStrLn $ show tag ++ ": " ++ show value
------------------------------------------
-- 3. Tthe Problem ™
-- How to write instances of GEq and GCompare for Tag?
#if 1
-- This works: we explictly reify, and use unsafe coerce.
reify :: Tag l -> Label
reify FooTag = Foo
reify BarTag = Bar
reify BazTag = Baz
instance GEq Tag where
geq b1 b2
| reify b1 == reify b2 = unsafeCoerce $ Just Refl
| otherwise = Nothing
instance GCompare Tag where
gcompare b1 b2 = case compare (reify b1) (reify b2) of
EQ -> unsafeCoerce GEQ
LT -> GLT
GT -> GGT
#endif
#if 0
-- But THIS DOESN'T!
-- No suitable instance of Tyepable is found?
deriving instance Typeable (Tag l)
deriving instance Typeable 'Foo
deriving instance Typeable 'Bar
deriving instance Typeable 'Baz
instance GEq Tag where
geq (_ :: Tag l1) (_ :: Tag l2)
| Just Refl <- eqT @l1 @l2 = Just Refl
| otherwise = Nothing
instance GCompare Tag where
gcompare b1 b2 = undefined
#endif
#if 0
-- This works, but is horrible?
-- And what about gcompare?
deriving instance Typeable (Tag l)
instance GEq Tag where
geq FooTag FooTag = Just Refl
geq BarTag BarTag = Just Refl
geq BazTag BazTag = Just Refl
geq _ _ = Nothing
instance GCompare Tag where
gcompare b1 b2 = undefined
#endif
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment