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

Maybe an analogy to a more mainstream language helps. I like using Kotlin these days:

http://kotlinlang.org/

which has nullable types. Imagine this code:

    fun useMessage(msg: Message) { .... }

    val s: Message? = someSocket.readNextMessage()   // Returns null if the socket has been closed.
    useMessage(s)
In Kotlin this would be a type error, the type of 's' is Message? and the question mark means it's possibly null. It won't compile. You can fix it by doing this:

    if (s != null) useMessage(s)
The act of testing 's' restricts its type inside the if block: we've proven it's not null, therefore the compiler will now accept this proof as evidence that the code is safe.

Idris isn't quite the same because it's a lot more general and the proofs are explicit instead of being implicit in the control flow: Idris types don't change when you test them, you get given a proof 'object' instead. But the basic idea is the same; your program does something that proves something about the type of a runtime value and that data can be used to improve program correctness.




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

Search: