Dependent typing and Refinement Typing for D

[Ola Fosheim Grøstad]

On Saturday, 21 December 2019 at 12:52:47 UTC, sighoya wrote:
>>So you can start with a runtime checked prototype
>> and end up with a statically checked final program.
>
> No, I would only use runtime checking. Even general dependent 
> typing requires at some point runtime assertions aka Path 
> Dependent typing ala Scala.

I don't know Scala, how does that work?


>> You need more machinery and annotations than just a SAT solver.
>
> Why?
> You only need SAT solving in cases where you want to up 
> propagate runtime assertion inserted by the compiler or for 
> overload resolution. It don't have to be perfect though and we 
> may can help with some kind of annotation, i.e. manually 
> specifying the overload order.

It will be very limited considering you can call functions in 
assertions. So you need to emit verification conditions to get 
anywhere, and that takes quite a bit of machinery.

> At first, it is very compile time consuming because of 
> tracking, e.g. proofing a list is extended with m additional 
> members requires to track the count of push functions called in 
> scope.

Verification is time consuming, dataflow/abstract interpretion is 
more reasonable (but less powerful).

> At second, it is generally undecidable you need to insert 
> manually proofs for it which you don't need for gradual 
> dependent typing as all runtime variables become constants at 
> runtime.

Yes, it will not always succeed. However,  you might be able to 
cache results from previous compiles or make it optional (i.e. 
just emit dynamic checks where applicable).

> No, return values depending on input values would be evaluated 
> at runtime before the function is called.

After?

> The point is the following, it seems to add additional runtime 
> checking, but you do it anyway in Lists and Vectors to throw 
> IndexOutOfBoundException or NullPointerException, instead of 
> doing this manually, the compiler can automate these exception 
> handling by inserting runtime asserts at compile time before 
> the function is called.

Contracts are supposed to have their asserts evaluated at the 
calling point, just not implemented in D IIRC.