Hello !<div>So my colleagues and I have some linear logical language engineering in various states of immaturity at <a href="http://github.com/hopper-lang">github.com/hopper-lang</a></div><div><br></div><div>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)</div><div><br></div><div>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<span></span><br><br>On Saturday, May 28, 2016, Nicola Gigante <<a href="mailto:nicola.gigante@gmail.com">nicola.gigante@gmail.com</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi all,<br>
<br>
Quipper [1] is a well-known library that provides an EDSL for writing and<br>
simulating quantum algorithms in Haskell.<br>
<br>
I was wondering if there was any other attempt to design an EDSL in Haskell<br>
to express quantum algorithms.<br>
<br>
In particular, Quipper is not able to statically ensure that the algorithm<br>
written is physically meaningful, as one could violate the "non-cloning property",<br>
for example (a qubit cannot be copied, for those who do not speak quantumly).<br>
Violations like this are detected at runtime when simulating the algorithm<br>
or when producing the corresponding circuit as output.<br>
<br>
Authors of Quipper already said that some of those properties could be<br>
possible to check “if Haskell had linear types”. The point is that Haskell's<br>
support for dependently typed programming has grown quite a lot in<br>
the last years, and I think that, at least theoretically, something better can<br>
now be achieved.<br>
<br>
So do anyone know any more recent attempt to express quantum computations<br>
in an Haskell EDSL that leverages cutting-edge type-level features to<br>
statically check for physically meaningful programs?<br>
<br>
Greetings,<br>
Nicola<br>
<br>
<br>
[1]: <a href="http://www.mathstat.dal.ca/~selinger/quipper/" target="_blank">http://www.mathstat.dal.ca/~selinger/quipper/</a><br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="javascript:;" onclick="_e(event, 'cvml', 'Haskell-Cafe@haskell.org')">Haskell-Cafe@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
</blockquote></div>