Dependent typing and Refinement Typing for D
sighoya
sighoya at gmail.com
Sat Dec 21 15:05:36 UTC 2019
>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).
Is an option, but release builds will be slow, runtime checking
isn't good in this case, as you would proof argument to return
value relationships each time a function is called.
I know that general dependent typing is from an idiomatic view
point right, but it has the following drawbacks:
1.) Function signatures become much more complicated with respect
to gradual dependent typed function signatures in that all return
values are related to their input arguments
2.) You can't characterize all properties of a function/type in
the signature, you don't know them immediately and the compiler
can't infer them for you, adding some properties later might
break your code.
3.) Signature become more sensible to changes (unstable),
changing them causes a cascade of errors following the stack
upwards.
4.) It doesn't fit to D, as D is already lazy (and unsafe) with
compile time duck typing, e.g. you can create generic entities
which can never be valid for any type parameter. Further type
errors are thrown at specialization time deep in the call stack
(unice), doing it differently for runtime values is an idomatic
break to how it is handled by D.
Theoretically, general dependent typing could replace all kinds
of unit testing, but to do so, you need to write the whole
function block as the return value in the function signature
which is unreadable and undecidable for the compiler to infer all
kinds of properties. It would further break the idiom of
encapsulation which is important for any kind of commercialism.
So practically, you still need to unit test.
More information about the Digitalmars-d
mailing list