The SBV library (https://hackage.haskell.org/package/sbv) uses the ideas in Andy Gill’s Observable sharing paper (http://www.ittc.ku.edu/~andygill/papers/reifyGraph.pdf) to safely observe sharing. Expressions remain pure, so long as “observation” of the sharing is done in the IO monad.

In my experience, this works really well and closely captures the application model: You want your users to program as if in a pure language, but the various backends (For SBV, this means C-compilation, SMTLib translation, Test-case generation etc.) already happens in a monadic framework, so it all works out rather nicely.

SBV doesn’t use Andy’s data-reify package (https://hackage.haskell.org/package/data-reify), but that’s mostly historic. I’d definitely give that package a try. But if it doesn’t work for you for whatever reason (maybe the API doesn’t quite fit), Andy’s paper is extremely well written and you can easily use his ideas to roll your own.

-Levent.

On Feb 5, 2020, at 9:40 AM, Tom Schouten <tom@zwizwa.be> wrote:

On 2/5/20 10:39 AM, Carter Schonwald wrote:
Try using clash, its its own thing, and overanalysis might be more challenging than just trying it out

Fair point.


- 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?

I was able to recover some information from my notes. I ran into this a while ago, then decided to keep the implementation simple and just use Monads:

A survey in Andy Gill's presentation on observable sharing:

http://www.ittc.ku.edu/~andygill/talks/20090903-hask.pdf

Just checked the Clash website and there is a link to Christiaan Baaij's master thesis, which has a description of the sharing problem in Appendix C:

https://essay.utwente.nl/59482/1/scriptie_C_Baaij.pdf


I think there is probably a use for a generic library that can do this kind of sharing recovery. Still I'm not quite happy with the "can be unsafe in some cases" remarks and would like to learn more. However there might be a tradeoff to use this as a simplified interface to something that is implemented in a safe monadic style under the hood.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.