On Tue, Mar 17, 2009 at 6:14 AM, Wolfgang Jeltsch <span dir="ltr">&lt;<a href="mailto:g9ks157k@acme.softbase.org">g9ks157k@acme.softbase.org</a>&gt;</span> wrote:<br><div class="gmail_quote"><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
Am Dienstag, 17. März 2009 11:49 schrieb Yandex:<br>
<div class="im">&gt; data (a :=: a&#39;) where<br>
&gt;   Refl :: a :=: a<br>
&gt;   Comm :: (a :=: a&#39;) -&gt; (a&#39; :=: a)<br>
&gt;   Trans :: (a :=: a&#39;) -&gt; (a&#39; :=: a&#39;&#39;) -&gt; (a :=: a&#39;&#39;)<br>
<br>
</div>I don’t think, Comm and Trans should go into the data type. They are not<br>
axioms but can be proven. Refl says that each type equals itself. Since GADTs<br>
are closed, Martijn’s definition also says that two types can *only* be equal<br>
if they are actually the same.<br>
<br>
Here are the original definition and the proofs of comm and trans. Compiles<br>
fine with GHC 6.10.1.<br>
<div class="im"><br>
    data (a :=: a&#39;) where<br>
<br>
        Refl :: a :=: a<br>
<br>
</div>    comm :: (a :=: a&#39;) -&gt; (a&#39; :=: a)<br>
    comm Refl = Refl<br>
<div class="im"><br>
    trans :: (a :=: a&#39;) -&gt; (a&#39; :=: a&#39;&#39;) -&gt; (a :=: a&#39;&#39;)<br>
</div>    trans Refl Refl = Refl</blockquote><div><br>These two theorems should be in the package.<br> </div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<br>
<br>
Best wishes,<br>
<font color="#888888">Wolfgang<br>
</font><div><div></div><div class="h5">_______________________________________________<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>
</div></div></blockquote></div><br>