On Monday, 13 October 2014 at 03:48:45 UTC, Meta wrote:
On Monday, 13 October 2014 at 00:01:02 UTC, Timon Gehr wrote:
On 10/13/2014 01:48 AM, Meta wrote:
On Sunday, 12 October 2014 at 20:58:58 UTC, Timon Gehr wrote:
Yes it is. Why wouldn't it be? Values needn't be completely
determined
in order to be reasoned about.
They do if you want to check, for example, n < 3. D doesn't
currently
support the type of analysis necessary to implement something
like that.
(bearophile isn't discussing current language features.)
Ridiculous, I'm positive that D fully supports refined types in
the language. Please check your facts.
Meta, go home, you're drunk.
This technique is for statically checking certain conditions for
the runtime values. This is what dependently typed languages do
using some proofs (ATS is worth mentioning here, it solves linear
integer conditions automatically using Presburger arithmetic and
lets using more involved proofs to solve nonlinear ones) and
languages with liquid/refined types do using an external SAT
solver. Other than simple value range propagation D doesn't do
anything like this. Arithmetic and conditions in the compile-time
part of the language is not it.
