5 ms·

Verified Functional Programming in Agda

lightgreen 7y ago
One thing I love about Agda is that it translates to Idris (which is much more friendly to a regular programmer) almost mechanically. Once I needed to write a proof of permutation transitivity in Idris. I’m not smart enough to write it myself, but I found a proof in Agda and translated it to Idris in 20 minutes. https://github.com/stepancheg/idris-sort/blob/master/PermHard.idr https://github.com/stepancheg/idris-sort/blob/master/PermHar...
- riedel 7y ago
  I was delighted to see that both idris and agda have JavaScript backends. Is there actually any productive use for that? Particularly looking at all the excitement around Reason .
  - gergoerdi 7y ago
    Here's a toy example: a single-page web app written in Idris. https://github.com/gergoerdi/icfp-bingo-2017-idris https://github.com/gergoerdi/icfp-bingo-2017-idris
thekhatribharat 7y ago
I put a related question on Computer Science Stack Exchange a week ago. Linking it here in the hopes that HN users roll-calling here will shed some light. Ref: https://cs.stackexchange.com/questions/122066/does-the-underlying-computational-calculus-in-type-theories-affect-decidability https://cs.stackexchange.com/questions/122066/does-the-under...
- guerrilla 7y ago
  I'm surprised Andrej didn't give a longer answer. He usually does. In a type theory the type system and calculus are the same thing, not really two things glued together (although there are some of those.) Those used for theorem proving and programming (CIC, MLTT, etc) aren't Turing complete by themselves. Different type theories do differ in computational strength. How is this possible? Well think about it, if you couldn't express the type of the Y combinator then you couldn't use it. Schemes like recursion, induction-recursion and induction-induction allow more power to be added to the language. To answer you more directly, one starts with the most powerful system, the lambda calculus and then one restricts its power using types. Finding the goldilocks zone of the right amount of power is one of the primary things type theory research has been about. Type theories vary in decidability, those that aren't decidable aren't usually used for theorem provers or as substrata for programming languages.
evolveyourmind 7y ago
How can I prove dfs graph termination in Agda? I tried passing "visited" subset but nothing
- Kutta 7y ago
  You need something which decreases on each step. You could try to recurse on the number of unvisited nodes in the graph. You can try well-founded recursion if this does not work for some reason.
  - evolveyourmind 7y ago
    The decreasing number worked, ty. Writing proofs with this will be impossible tho :D
FrankyHollywood 7y ago
thx a lot, found some other interesting books along the way! https://dl.acm.org/acmbooks https://dl.acm.org/acmbooks
JadeNB 7y ago
Reminder that all ACM Digital Library resources, including books, are free until June 30. https://www.acm.org/articles/bulletins/2020/march/dl-access-during-covid-19 https://www.acm.org/articles/bulletins/2020/march/dl-access-...

One thing I love about Agda is that it translates to Idris (which is much more friendly to a regular programmer) almost mechanically. Once I needed to write a proof of permutation transitivity in Idris. I’m not smart enough to write it myself, but I found a proof in Agda and translated it to Idris in 20 minutes. https://github.com/stepancheg/idris-sort/blob/master/PermHard.idr https://github.com/stepancheg/idris-sort/blob/master/PermHar...

riedel 7y ago
I was delighted to see that both idris and agda have JavaScript backends. Is there actually any productive use for that? Particularly looking at all the excitement around Reason .
- gergoerdi 7y ago
  Here's a toy example: a single-page web app written in Idris. https://github.com/gergoerdi/icfp-bingo-2017-idris https://github.com/gergoerdi/icfp-bingo-2017-idris

thekhatribharat 7y ago

I put a related question on Computer Science Stack Exchange a week ago. Linking it here in the hopes that HN users roll-calling here will shed some light. Ref: https://cs.stackexchange.com/questions/122066/does-the-underlying-computational-calculus-in-type-theories-affect-decidability https://cs.stackexchange.com/questions/122066/does-the-under...

guerrilla 7y ago
I'm surprised Andrej didn't give a longer answer. He usually does. In a type theory the type system and calculus are the same thing, not really two things glued together (although there are some of those.) Those used for theorem proving and programming (CIC, MLTT, etc) aren't Turing complete by themselves. Different type theories do differ in computational strength. How is this possible? Well think about it, if you couldn't express the type of the Y combinator then you couldn't use it. Schemes like recursion, induction-recursion and induction-induction allow more power to be added to the language. To answer you more directly, one starts with the most powerful system, the lambda calculus and then one restricts its power using types. Finding the goldilocks zone of the right amount of power is one of the primary things type theory research has been about. Type theories vary in decidability, those that aren't decidable aren't usually used for theorem provers or as substrata for programming languages.

evolveyourmind 7y ago

How can I prove dfs graph termination in Agda? I tried passing "visited" subset but nothing

Kutta 7y ago
You need something which decreases on each step. You could try to recurse on the number of unvisited nodes in the graph. You can try well-founded recursion if this does not work for some reason.
- evolveyourmind 7y ago
  The decreasing number worked, ty. Writing proofs with this will be impossible tho :D

FrankyHollywood 7y ago

thx a lot, found some other interesting books along the way! https://dl.acm.org/acmbooks https://dl.acm.org/acmbooks

JadeNB 7y ago

Reminder that all ACM Digital Library resources, including books, are free until June 30. https://www.acm.org/articles/bulletins/2020/march/dl-access-during-covid-19 https://www.acm.org/articles/bulletins/2020/march/dl-access-...