You can do this with phantom types, i.e.:<div><br><div><div>&gt; data Thing a = Thing Stuff</div><div>&gt; </div><div>&gt; instance Monoid (Thing a) where</div><div>&gt;   mappend (Thing stuff1) (Thing stuff2) = Thing (stuff1 `mappend` stuff2)</div>

<div>&gt;   mempty = Thing mempty</div><div>&gt;   </div><div>&gt; data ID1</div><div>&gt; data ID2</div><div>&gt; </div><div>&gt; thing1 :: Thing ID1</div><div>&gt; thing1 = Thing Stuff</div><div>&gt; </div><div>&gt; thing2 :: Thing ID2</div>

<div>&gt; thing2 = Thing Stuff</div><div>&gt; </div><div>&gt; -- will not typecheck:</div><div>&gt; f = thing1 `mappend` thing2</div><div><br><br><div class="gmail_quote">2011/11/23 Evan Laforge <span dir="ltr">&lt;<a href="mailto:qdunkan@gmail.com">qdunkan@gmail.com</a>&gt;</span><br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">So suppose I have a simple data type:<br>
<br>
&gt; data Thing {<br>
&gt;   thing_id :: ThingId<br>
&gt;   , thing_stuff :: Stuff<br>
&gt;   }<br>
&gt; newtype ThingId = ThingId String<br>
<br>
Stuff is a Monoid, and Things need to be combined as well, so:<br>
<br>
&gt; instance Monoid Thing where<br>
&gt;   mappend (Thing id1 stuff1) (Thing id2 stuff2)<br>
&gt;     | id1 /= id2 = error &quot;...&quot;<br>
&gt;     | otherwise = Thing id1 (stuff1 `mappend` stuff2)<br>
&gt;   mempty = Thing $ (ThingId &quot;dummy value?&quot;) mempty<br>
<br>
So clearly both the error and the &quot;dummy value?&quot; are not very nice<br>
(and mappend would need a special hack to treat the dummy as<br>
compatible with everything).  I&#39;d like to be able to lift that ID up<br>
to the type level, and then I don&#39;t have to worry about incompatible<br>
IDs and the mempty can figure out the ID from the type.<br>
<br>
Now if ThingId were a natural, I gather there&#39;s a new GHC feature for<br>
type level naturals that can do this kind of thing.  Of course any<br>
string could be encoded into a large natural, but the resulting type<br>
errors would be less than readable.  There is probably also a way to<br>
encode type level strings in the same way as the traditional way for<br>
type level naturals, e.g. &#39;data A; ... data Z;&#39; and then a type<br>
encoding for lists.  But I&#39;m guessing that would also lead to<br>
excessive compilation times and crazy type errors.<br>
<br>
In any case, I don&#39;t think this can work even if I used naturals<br>
instead of ints, because it seems to me I can&#39;t write a function<br>
&#39;(NatI n) =&gt; ThingId -&gt; Thing n&#39; without a statically knowable<br>
constant value for &#39;n&#39;.  Otherwise, the value has magically<br>
disappeared into the type system and I can&#39;t expect to get it back<br>
after types are erased.<br>
<br>
So I need a runtime value for the ThingId, but it still seems like it<br>
should be possible to do something better than the &#39;error&#39; and &quot;dummy<br>
value?&quot;.  Maybe there&#39;s a completely different way to ensure that<br>
incompatible Things can&#39;t be mappended.  Any ideas?<br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</blockquote></div><br></div></div></div>