I'm glad to see dependent types move a bit closer to practical programming. I read (well, skimmed) the tutorial and learned a little of what it's all about. Being able to pass around assertions as first-class objects seems pretty interesting.
However, I'm still confused about what's happening at compile time versus runtime. Apparently some functions can be used in proofs (and are therefore evaluated at compile time), while some proofs must be evaluated at runtime?
The notation isn't very helpful here. Since types are no longer strictly compile time and values are no longer strictly runtime, it seems like we need some other way to easily distinguish compile time and runtime.
See this page (https://github.com/idris-lang/Idris-dev/wiki/Erasure-by-usag...) for info on erasure. Unused proof values or indices in data types used for static checking are erased at compile time via usage analysis (if you don't use it in the RHS of a function definition, it gets erased).
If you want to ensure that the indices of your data type or arguments to your function are erased, you can use the new dot notation. E.g., if you give a function called "half" the following type
half : (n : Nat) -> .(pf : Even n) -> Nat
then the compiler will complain if the proof argument is actually used.
I may be misinterpreting your statement, but passing around assertion objects is a common feature of many DT languages (Coq, Agda, Idris, Epigram, ATS, etc)
However, I'm still confused about what's happening at compile time versus runtime. Apparently some functions can be used in proofs (and are therefore evaluated at compile time), while some proofs must be evaluated at runtime?
The notation isn't very helpful here. Since types are no longer strictly compile time and values are no longer strictly runtime, it seems like we need some other way to easily distinguish compile time and runtime.