[Agda] Blog post about agda2hs
mechvel at scico.botik.ru
mechvel at scico.botik.ru
Thu Oct 6 13:57:32 CEST 2022
On 2022-10-06 12:29, Jesper Cockx wrote:
> Hi Agda folks,
>
> I've just published a new blog post about agda2hs, a tool that
> originated from some of the previous Agda meetings and we recently
> presented at the Haskell Symposium. You can read the post here:
> https://jesper.sikanda.be/posts/agda2hs.html. I'm very curious to hear
> if you have any ideas or applications of the tool!
>
Jesper,
you write there
"
Sadly, in industry many people are forced to work in languages with a
weak type system, such as Haskell.
What should you do in such a situation? Quit your job? Give up and
despair?
Perhaps, but I have another suggestion that I’d like to explain in this
post: use our tool agda2hs.
What is this agda2hs, I hear you asking? Agda2hs is a tool for producing
verified and readable
Haskell code by extracting it from a (lightly annotated) Agda program.
This means you can write
your code using Agda’s support for dependent types, interactive editing,
and termination checking,
and from this agda2hs will generate clean and simply typed Haskell code
that looks like it was written
by hand. Your boss will be amazed that all of your code is correct from
the first try, and never even
suspect that you secretly proved its correctness in Agda!
"
It depends on the desired level of verification.
Most of the methods, that are programmed in Haskell in 5 days cannot be
programmed
in Agda as a totally verified program, say, in 50 days.
Often it is more practical to write a Haskell program, to supply it with
a non-formal proof,
and to test it on examples. This takes many times less effort than total
verification.
But if the goal is a totally verified program (probably a rare case in
industry, it costs much),
then yes, the idea looks all right.
Another question is performance. How often the program obtained by
problem -> Agda -> Haskell
runs many times slower than the one originally written in Haskell?
(mainly, I mean GHC).
Probably, people needs to try examples.
Also what about proofs internally accumulated in the function body and
being returned
as a part of the result? Many methods cannot be in practice programmed
in Agda in another way.
A contrived example:
gcd for Nat written in Agda, with accumulating recursively a proof
in its body.
And gcd! a b = proj1 (gcd a b)
that chooses the proper gcd value.
How will it look the converted Haskell program for gcd! ?
Regards,
------
Sergei
More information about the Agda
mailing list