On Wed, Nov 23, 2011 at 4:03 PM, Holger Reinhardt wrote:

You can do this with phantom types, i.e.:

...

data Thing a = Thing Stuff

instance Monoid (Thing a) where   mappend (Thing stuff1) (Thing stuff2) = Thing (stuff1 `mappend` stuff2)   mempty = Thing mempty

data ID1 data ID2

thing1 :: Thing ID1 thing1 = Thing Stuff

thing2 :: Thing ID2 thing2 = Thing Stuff

-- will not typecheck: f = thing1 `mappend` thing2

Well yes, but the key feature is that the IDs are arbitrary strings. And they're not knowable at compile time, since they are read from user input...

On Wed, Nov 23, 2011 at 4:25 PM, Julian Beaumont wrote:

On Thu, Nov 24, 2011 at 10:06 AM, Evan Laforge wrote:

...

Well yes, but the key feature is that the IDs are arbitrary strings. And they're not knowable at compile time, since they are read from user input...

You can still use phantom types for this, you just need existentials as well. For example, you could define a type for indexed strings/id's as:

data IString s  = IString String

data Exists f  = forall x. Exists (f x)

read :: String -> Exists IString read stuff = Exists (IString stuff)

I assume you'll also want to compare strings/id's, in which case you'll also need (using GADT's):

data Equal a b where  Refl :: Equal a a

equal :: IString s -> IString t -> Maybe (Equal s t) equal (IString x) (IString y) | x == y = Just (unsafeCoerce Refl) equal _ _ = Nothing

I don't fully understand this but it looks interesting! I guess 'read' is a constructor for a sort of witness of the id, but I don't see how to get this value into the type parameter, or how Equal would be used in my mappend example. Could you help me figure out how it relates? Here's the closest I could get: data Thing thing_id = Thing { thing_id :: Exists IString , thing_stuff :: [Int] } thing :: String -> [Int] -> Thing thing_id thing thing_id stuff = Thing (istring thing_id) stuff instance Monoid.Monoid (Thing thing_id) where mempty = Thing undefined [] mappend (Thing id1 stuff1) (Thing _ stuff2) = Thing id1 (Monoid.mappend stuff1 stuff2) istring :: String -> Exists IString istring thing_id = Exists (IString thing_id) data IString s = IString String data Exists f = forall x. Exists (f x) data Equal a b where Refl :: Equal a a equal :: IString s -> IString t -> Maybe (Equal s t) equal (IString x) (IString y) | x == y = Just (Coerce.unsafeCoerce Refl) equal _ _ = Nothing But as you can see it's not right, because the 'thing_id' goes into the existential but is not expressed in the type parameter to Thing (the real usage is that Things are Pitches which have a Scale and a Signal, and it only makes sense to combine Pitches with the same scale, which is probably a more interesting example, but I started with Stuff and Things so I guess I should stick with it). I don't see how I could use Equal, because the signature for mappend already expresses that the arguments should be the same type. And while I can see how to extract the String from the IString, I don't see how to figure out the String from the *type* of the IString, as I would need to do in mempty, since IString has no type parameter.