On 2/5/20 8:17 AM, Carter Schonwald wrote:
Have you looked at how stuff like the ivory/tower edsl libraries do their embedding?
That is a nice project! Thanks for pointing it out.
For Ivory, the embedding is monadic so not any different in that respect, and this is also much more expressive than what I need.
I guess I don't know what exactly I don't know...
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.
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.
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?
This is what I sort of understand:
- 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.
- 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?
- 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.
- 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.