Hello ! So my colleagues and I have some linear logical language engineering in various states of immaturity at github.com/hopper-lang Last fall Jeff polakow presented a paper at Haskell symposium or Icfp (forget which) for embedding linear types in Haskell , might be worth googling around for a copy of that paper (Google scholar might get you a non paywalled pdf) There's some cool stuff related to this I hope to share with the community in the near future, but that's all I can offer off the cuff On Saturday, May 28, 2016, Nicola Gigante wrote:

Hi all,

Quipper [1] is a well-known library that provides an EDSL for writing and simulating quantum algorithms in Haskell.

I was wondering if there was any other attempt to design an EDSL in Haskell to express quantum algorithms.

In particular, Quipper is not able to statically ensure that the algorithm written is physically meaningful, as one could violate the "non-cloning property", for example (a qubit cannot be copied, for those who do not speak quantumly). Violations like this are detected at runtime when simulating the algorithm or when producing the corresponding circuit as output.

Authors of Quipper already said that some of those properties could be possible to check “if Haskell had linear types”. The point is that Haskell's support for dependently typed programming has grown quite a lot in the last years, and I think that, at least theoretically, something better can now be achieved.

So do anyone know any more recent attempt to express quantum computations in an Haskell EDSL that leverages cutting-edge type-level features to statically check for physically meaningful programs?

Greetings, Nicola

[1]: http://www.mathstat.dal.ca/~selinger/quipper/ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org javascript:; http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe