On Friday, 23 October 2020 at 16:56:46 UTC, Kagamin wrote:
On Thursday, 22 October 2020 at 18:24:47 UTC, Bruce Carneal
wrote:
Per the wiki on termination analysis some languages with
dependent types (Agda, Coq) have built-in termination checkers.
What they do with code that does, say, a hash
On Thursday, 22 October 2020 at 18:24:47 UTC, Bruce Carneal wrote:
Per the wiki on termination analysis some languages with
dependent types (Agda, Coq) have built-in termination checkers.
What they do with code that does, say, a hash preimage attack?
On Friday, 23 October 2020 at 04:24:09 UTC, Paul Backus wrote:
On Friday, 23 October 2020 at 00:53:19 UTC, Bruce Carneal wrote:
When you write functions, the compiler helps you out with
fully automated constraint checking. When you write templates
you can write them so that they look like
On Friday, 23 October 2020 at 00:53:19 UTC, Bruce Carneal wrote:
When you write functions, the compiler helps you out with fully
automated constraint checking. When you write templates you
can write them so that they look like simple functions, in
which case you're on pretty solid ground.
On Thursday, 22 October 2020 at 20:37:22 UTC, Paul Backus wrote:
On Thursday, 22 October 2020 at 19:24:53 UTC, Bruce Carneal
wrote:
On a related topic, I believe that type functions enable a
large amount of code in the "may be hard to prove decidable"
category (templates) to be (re)written as
On Thursday, 22 October 2020 at 19:24:53 UTC, Bruce Carneal wrote:
On a related topic, I believe that type functions enable a
large amount of code in the "may be hard to prove decidable"
category (templates) to be (re)written as clearly decidable
code. Easier for the compiler to deal with
On Thursday, 22 October 2020 at 19:24:53 UTC, Bruce Carneal wrote:
I dont think it is any easier to prove the "will increase
faster" proposition than it is to prove the whole thing.
They probably just impose restrictions so that they prove that
there is reduction and progress over time. One
On Thursday, 22 October 2020 at 18:46:07 UTC, Ola Fosheim Grøstad
wrote:
On Thursday, 22 October 2020 at 18:38:12 UTC, Stefan Koch wrote:
On Thursday, 22 October 2020 at 18:33:52 UTC, Ola Fosheim
Grøstad wrote:
In general, it is hard to tell if a computation is
long-running or unsolvable.
On Thursday, 22 October 2020 at 18:38:12 UTC, Stefan Koch wrote:
On Thursday, 22 October 2020 at 18:33:52 UTC, Ola Fosheim
Grøstad wrote:
In general, it is hard to tell if a computation is
long-running or unsolvable.
You could even say ... it's undecidable :)
:-) Yes, although you can
On Thursday, 22 October 2020 at 17:25:44 UTC, Bruce Carneal wrote:
Is type checking in D undecidable? Per the wiki on dependent
types it sure looks like it is.
It is indeed undecidable. Imagine you had a decider for it.
Because CTFE is clearly turing-complete, you can express that in
a D
On Thursday, 22 October 2020 at 18:33:52 UTC, Ola Fosheim Grøstad
wrote:
In general, it is hard to tell if a computation is long-running
or unsolvable.
You could even say ... it's undecidable :)
On Thursday, 22 October 2020 at 18:24:47 UTC, Bruce Carneal wrote:
Per the wiki on termination analysis some languages with
dependent types (Agda, Coq) have built-in termination checkers.
I assume that DMD employs something short of such a checker,
some combination of cycle detection backed up
On Thursday, 22 October 2020 at 18:04:32 UTC, Ola Fosheim Grøstad
wrote:
On Thursday, 22 October 2020 at 17:25:44 UTC, Bruce Carneal
wrote:
Is type checking in D undecidable? Per the wiki on dependent
types it sure looks like it is.
Even if it is, you can still write something that is
On Thursday, 22 October 2020 at 17:25:44 UTC, Bruce Carneal wrote:
Is type checking in D undecidable? Per the wiki on dependent
types it sure looks like it is.
Even if it is, you can still write something that is decidable in
D, but impractical in terms of compile time.
You probably mean
14 matches
Mail list logo
