Hacker News new | past | comments | ask | show | jobs | submit login

So, how do these advanced types work?

For their `add` example, I imagine just having x<y somewhere is sufficient. But let's say I write a sorting implementation but the compiler can't quite figure out that it is correct. Is there a provided way to tell the compiler 'trust me, this property is now true'?

Also, I'm assuming the compiler has two classes of errors here: a counter example vs. unable to prove?

Can anyone point me to documentation on these (in Idris, preferably)?




In Idris, there are functions `believe_me` and `really_believe_me`, which assert things to the compiler. They're generally only used for FFI code, or for extremely tedious proofs.

If you wanted to prove that a list was sorted, you'd write another datatype:

    IsSorted : Ord a => List a -> Type
which represents the proposition that the input list is sorted. You could encode this by requiring that any new element in the list is either the first element, or less than or equal to the previous element. Then, your sorting function could return a dependent pair:

    (l : List a ** IsSorted l)
which can be read as the list, accompanied by a proof that it is, in fact, sorted. Since your `IsSorted` type requires that the list is sorted, via construction, you won't be able to supply the output of the function unless your code is correct (or you use `believe_me`!).

The compiler doesn't generally come up with counterexamples for you; with this style, if the proof isn't complete, it won't compile.




Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: