<div dir="ltr">Try using clash, its its own thing, and overanalysis might be more challenging than just trying it out <br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Feb 5, 2020 at 10:37 AM Tom Schouten <<a href="mailto:tom@zwizwa.be">tom@zwizwa.be</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div bgcolor="#FFFFFF">
<p><br>
</p>
<div>On 2/5/20 8:17 AM, Carter Schonwald
wrote:<br>
</div>
<blockquote type="cite">
<div dir="auto"><br>
</div>
<div dir="auto">Have you looked at how stuff like the ivory/tower
edsl libraries do their embedding? </div>
<div dir="auto"><br>
</div>
</blockquote>
<p>That is a nice project! Thanks for pointing it out.<br>
</p>
<p>For Ivory, the embedding is monadic so not any different in that
respect, and this is also much more expressive than what I need.</p>
<p><br>
</p>
<p>I guess I don't know what exactly I don't know...<br>
</p>
<p>I'm doing something quite straightforward. Basically I know that
the language I'm embedding only has pure functions mapping pairs
of sequences to pairs of sequences with the restriction that the
mapping is causal when you look at individual elements in a
stream, but I dont' think this fact is even observable after
abstracting to streams.<br>
</p>
<p>Keeping track of the sharing information necessary to be able to
compile it to an external target introduces an effect. But this
is the _only_ effect, and it is an implementation detail that
makes me loose all the nice properties of pure functions. That
just feels wrong. I'm sure I'm missing something.<br>
</p>
<p>I believe the core issue is that I'm not understanding something
quite fundamental. Why is it so hard to recover sharing
information if the thing that is embedded is pure? I suspect the
answer is something something referential transparency but how
exactly?</p>
<p><br>
</p>
<p>This is what I sort of understand:</p>
<p>- Compiling to categories fixes the problem completely using a
big gun: abstracting over function abstraction and application.
It's great, but can't be done in Haskell as is. This is probably
the cleanest solution. I suspect this also has the answer to my
question above but I don't quite see it.<br>
</p>
<p>- There is another Functional HDL that solves this using some
unsafe reference trick to keep track of the sharing. I believe it
is CλaSH but I'm not sure. I believe you can get away with this
because the semantics is pure so in practice doesn't cause any
inconsistencies, but it really doesn't sound like something I
would do without some kind of proof that it is actually ok. If it
is ok, it would probably make sense to abstract this in a library.
Maybe someone has done that already?<br>
</p>
<p>- You can try to recover sharing later by doing common
subexpression elimination. This works but has complexity issues
and doesn't scale to large systems.<br>
</p>
<p>- Maybe it is possible to hide the compiler using existential
types. I tried something along these lines but I couldn't figure
it out so I don't know if it's just lack of insight or just
impossible. Probably the latter.</p>
<p><br>
</p>
<p><br>
</p>
<br>
<p><br>
</p>
<p><br>
</p>
<p><br>
</p>
</div>
</blockquote></div>