Hacker News Reader

Comment by mrkgnao | Hacker News Reader

> What you get "for free" from such languages may not be significant enough to justify the cost of adoption

Idris can often infer entire functions from their types if the domain is amenable to accurate type-based specification. For instance, taking the common "sized vector" example, where `Vec n a` refers to a length-n vector of values of type a, functions like

    zip : Vec n a -> Vec n b -> Vec n (a, b)

can be automatically generated via the interactive "proof search" mechanism that the Emacs integration for Idris provides. Similar things are possible in Agda, which is however squarely aimed away from the "practical use" market.

View on HN

> Idris can often infer entire functions from their types if the domain is amenable to accurate type-based specification.

This is a great example of what I'm talking about. The kind of functions Idris can generate is that of functions that you could manually write with only marginally more effort -- if that -- than the effort required to write the precise type. I don't think those functions ever form a significant portion of a significant program, if at all (those functions must be so generic, or else there would be a search problem that Idris can't solve, that they would already likely be in the standard libraries). When Idris is able to generate an efficient sorting function given some constraints, then I'd be impressed.

> can be automatically generated via the interactive "proof search" mechanism

If you've spent a significant amount of time with such proof assistants, you'd see that the proof search is rather pitiful.

> If you've spent a significant amount of time with such proof assistants, you'd see that the proof search is rather pitiful.

Afaik, Idris' proof search was hacked together in an afternoon just to see if it would work. And it did, surprisingly well considering. Don't know how much it has been worked on since then though. But yes, still leaves a bit to be desired compared to other systems.

I wasn't just talking about Idris. There isn't a single tool out there that can automatically prove that your quicksort implementation actually sorts without pretty significant work.

Reply on news.ycombinator.com