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 <
nicola.gigante@gmail.com> 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
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe