Evan Laforge has defined

data Thing { thing_id :: ThingId , thing_stuff :: Stuff } newtype ThingId = ThingId String

and wishes to statically preclude binary operations with things that have different ThingIds. However, Things and their Ids can be loaded from files and so cannot be known to the compiler. He wished for type-level strings -- which is what the enclosed code gives. When we've got two Things loaded from two different files we must do a run-time check to see if these two things have in fact the same ThingId. That is inevitable. The question is how frequently do we have to make such a test? One approach is to do such a ruin-time test on each binary operation on things. The original Thing above was of that approach:

instance Monoid Thing where mappend (Thing id1 stuff1) (Thing id2 stuff2) | id1 /= id2 = error "..." | otherwise = Thing id1 (stuff1 `mappend` stuff2)

Every time we mappend things, we must check their ids. It has been suggested to use existentials. We get the the following code:

maybeAppend :: Exists Thing -> Exists Thing -> Maybe (Exists Thing) maybeAppend (Exists t1) (Exists t2) = case thing_id t1 `equal` thing_id t2 of Just Refl -> Just $ Exists (t1 `mappend` t2) Nothing -> Nothing

How different is this from the original mappend? Every time we wish to mappend two things, we have to do the run-time test of their ids! We added phantom times, existentials, GADTs -- and got nothing in return. No improvement to the original code, and no static guarantees. When we have to mappend things several times, it seems optimal to do the run-time ID check only once (we have to do that check anyway) and then mappend the results without any checks, and with full static assurance that only Identical things are mappended. The enclosed code implements that approach. The instance for Monoid makes patent only things with the same id may be mappended. Moreover, there is no run-time id check, and we do not have to think up the id to give to mempty. The test does read two things from a `file' (a string) and does several operations on them. The run-time test is done only once. The ideas of the code are described in the papers with Chung-chieh Shan on lightweight static capabilities and implicit configurations. {-# LANGUAGE RankNTypes, ScopedTypeVariables #-} module Thing where import Data.Monoid import Data.Char -- The data constructor Thing should not be exported newtype Thing id = Thing{ thingStuff :: Stuff } type Stuff = [Int] -- or any monoid class IDeal id where get_id :: id -> String -- The user should use make_thing make_thing :: IDeal id => id -> Stuff -> Thing id make_thing _ t = Thing t -- It is statically assured that only things with the same id -- may be mappended. Moreover, there is no run-time id check -- And we do not have to think up the id to give to mempty instance Monoid (Thing id) where Thing t1 `mappend` Thing t2 = Thing (t1 `mappend` t2) mempty = Thing mempty instance IDeal id => Show (Thing id) where show (Thing t) = show $ (get_id (undefined::id),t) -- A statically-known Id (just in case) data Id1 = Id1 instance IDeal Id1 where get_id _ = "Id1" -- Reading a thing from a file (or at least, a string) data DynId id = DynId instance Nat id => IDeal (DynId id) where get_id _ = int_to_str $ nat (undefined::id) read_thing :: String -> (forall id. IDeal id => Thing id -> w) -> w read_thing str k = reify_ideal i (\iD -> k (make_thing iD t)) where (i,t) = read str -- Run-time equality check -- If id and id' are the same, cast the second to the same id eqid_check :: forall id id'. (IDeal id, IDeal id') => Thing id -> Thing id' -> Maybe (Thing id) eqid_check _ (Thing t) | get_id (undefined::id) == get_id (undefined::id') = Just (Thing t) eqid_check _ _ = Nothing test file1 file2 = read_thing file1 (\t1 -> read_thing file2 (\t2 -> do_things t1 t2)) where -- A run-time test is inevitable, but it is done only once do_things t1 t2 | Just t2' <- eqid_check t1 t2 = do_things' t1 t2' do_things _ _ = error "bad things" -- Now it is assured we have the same id -- we can do things many times do_things' :: IDeal id => Thing id -> Thing id -> String do_things' t1 t2 = show $ mempty `mappend` t1 `mappend` t2 `mappend` t2 `mappend` t1 t1 = test "(\"id1\",[1,2])" "(\"id1\",[3,4])" -- "(\"id1\",[1,2,3,4,3,4,1,2])" t2 = test "(\"id1\",[1,2])" "(\"id2\",[3,4])" -- "*** Exception: bad things -- Reifying strings to types -- They say String kinds are already in a GHC branch. -- Edward Kmett maintains a Hackage package for these sort of things -- Assume ASCII for simplicity str_to_int :: String -> Integer str_to_int "" = 0 str_to_int (c:t) = fromIntegral (ord c) + 128 * str_to_int t int_to_str :: Integer -> String int_to_str = loop "" where loop acc 0 = reverse acc loop acc n | (n',c) <- quotRem n 128 = loop (chr (fromIntegral c) : acc) n' data Z = Z data S a = S a data T a = T a class Nat a where nat :: a -> Integer instance Nat Z where nat _ = 0 instance Nat a => Nat (S a) where nat _ = 1 + nat (undefined::a) instance Nat a => Nat (T a) where nat _ = 2 * nat (undefined::a) reify_integer :: Integer -> (forall x. Nat x => x -> w ) -> w reify_integer 0 k = k Z reify_integer n k | even n = reify_integer (n `div` 2) (\x -> k (T x)) reify_integer n k = reify_integer (n-1) (\x -> k (S x)) reify_ideal :: String -> (forall x. IDeal x => x -> w) -> w reify_ideal str k = reify_integer (str_to_int str) (k . dynid) where dynid :: x -> DynId x dynid = undefined tr1 = reify_integer 10 nat tr2 = int_to_str $ reify_integer (str_to_int "id1") nat