<div dir="ltr"><br><div class="gmail_extra">On Tue, Feb 19, 2013 at 9:28 PM, Anton Kholomiov <span dir="ltr">&lt;<a href="mailto:anton.kholomiov@gmail.com" target="_blank">anton.kholomiov@gmail.com</a>&gt;</span> wrote:<br>

<div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><br><div class="gmail_quote"><div class="im"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">

<div dir="ltr"><div>Do you think the approach can be extended for non-regular (nested) algebraic types (where the recursive data type is sometimes at a different type instance)? For instance, it&#39;s very handy to use GADTs to capture embedded language types in host language (Haskell) types, which leads to non-regularity.<span><font color="#888888"><br>




<br></font></span></div></div></blockquote></div><div><br>I&#39;m not sure I understand the case you are talking about. Can you write a simple example<br>of the types like this?<br></div></div></blockquote><div><br></div>

<div>Here&#39;s an example of a type-embedded DSEL, represented as a GADT:<br></div><div><br>&gt; data E :: * -&gt; * where<br>&gt;   Lit :: Show a =&gt; a -&gt; E a<br>&gt;   Op  :: Op a -&gt; E a<br>&gt;   App :: E (a -&gt; b) -&gt; E a -&gt; E b<br>

&gt;   ...<br>&gt; <br>&gt; data Op :: * -&gt; * where<br>&gt;   Add :: Num a =&gt; E (a -&gt; a -&gt; a)<br>&gt;   Mul :: Num a =&gt; E (a -&gt; a -&gt; a)<br>&gt;   Neg :: Num a =&gt; E (a -&gt; a)<br>&gt;   ...<br><br>

</div></div>-- Conal<br></div></div>