Re: is type checking in D undecidable?
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 simple functions, in which case you're on pretty solid ground. Your manual constraints will probably work. Hard to screw up a four line eponymous template with constraints. Hard to screw up a "leaf" template with a small number of template args. Possible but hard. Not so hard to screw up "wanna-be-as-general-as-possible-but-special-case-performant-and-sometimes-wierdly-recursive-cuz-otherwise-the-compiler-blows-up" templates. This is true, but it has nothing at all to do with decidability--which is a term with a precise technical definition in computer science. Yep. The thread started with the technical definition, as you'll note in the wiki articles that I cited, and then moved on. I probably should have started another thread. The reason writing correct generic code using templates (or any macro system) is so difficult is that templates (and macros in general) are, effectively, dynamically typed. Unlike regular functions, templates are not type checked when they are declared, but when they are "executed" (that is, instantiated). In that sense, writing templates in D is very similar to writing code in a dynamically-typed language like Python or Javascript. Yep. Good observations. Functions offer some nice benefits. I'd like to see their use increase (type functions displacing templates wherever appropriate).
Re: is type checking in D undecidable?
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. Your manual constraints will probably work. Hard to screw up a four line eponymous template with constraints. Hard to screw up a "leaf" template with a small number of template args. Possible but hard. Not so hard to screw up "wanna-be-as-general-as-possible-but-special-case-performant-and-sometimes-wierdly-recursive-cuz-otherwise-the-compiler-blows-up" templates. This is true, but it has nothing at all to do with decidability--which is a term with a precise technical definition in computer science. The reason writing correct generic code using templates (or any macro system) is so difficult is that templates (and macros in general) are, effectively, dynamically typed. Unlike regular functions, templates are not type checked when they are declared, but when they are "executed" (that is, instantiated). In that sense, writing templates in D is very similar to writing code in a dynamically-typed language like Python or Javascript.
Re: is type checking in D undecidable?
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 clearly decidable code. Easier for the compiler to deal with and, more importantly, easier to teach. Type functions, like regular functions, are Turing-complete, and therefore undecidable in the general case. Sure, most languages are Turing complete at run time. A few are Turing complete at compile time but templates are also pattern matching code expanders. Polymorphic. By design templates are open ended and powerful (in both the practical and theoretical sense). In some situations they're exactly what you need. They are also harder to employ correctly than functions. 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. Your manual constraints will probably work. Hard to screw up a four line eponymous template with constraints. Hard to screw up a "leaf" template with a small number of template args. Possible but hard. Not so hard to screw up "wanna-be-as-general-as-possible-but-special-case-performant-and-sometimes-wierdly-recursive-cuz-otherwise-the-compiler-blows-up" templates. It'd be great if we could get rid of many such templates, and, even more importantly, avoid writing a lot more. That is likely when we start asking if type functions can reduce bugs long term, both those experienced in the currently tortured template subsystem and those experienced in user code. The performance gains exhibited by type functions are, to me, just gravy.
static alias this and if/do/while/for
There is a funny feature (or bug) in the D language:
static alias this and static operator overloading.
For example
interface Foo {
static {
int value;
void opAssign(int v) { value = v; }
int get() { return value; }
alias get this;
}
}
Now we can use type Foo as if it were an lvalue/rvalue:
Foo = 5;
int a = Foo;
int b = Foo + a;
I heavily use this feature in my MCU library.
But it doesn't work inside conditionals:
if(Foo) {}// Error: type Foo is not an expression
while(Foo) {} // Error: type Foo is not an expression
Even if we define `static opCast!bool()`. It doesn't help.
Should this be fixed?
Re: Recommended way to use __FILE__/__LINE__ etc.
Thanks for all your answers!
Re: is type checking in D undecidable?
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 and, more importantly, easier to teach. Type functions, like regular functions, are Turing-complete, and therefore undecidable in the general case.
Re: is type checking in D undecidable?
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 common for strategy for proving termination is that something is reduced every iteration (or at some points in the program that is passed through).
Re: is type checking in D undecidable?
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. You could even say ... it's undecidable :) :-) Yes, although ... [...] Also, some advanced systems might be able to detect that no real progress is possible. For example being able to prove that the number of "subqueries" to be tried will increase faster than the number of "subqueries" that can be resolved. I dont think it is any easier to prove the "will increase faster" proposition than it is to prove the whole thing. But this is really the frontier of programming language design... Agree. As I see it, D is on the frontier of practical (meta) programming. A very exciting place to be. 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 and, more importantly, easier to teach.
Re: is type checking in D undecidable?
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 impose restrictions on the language. Something that is desirable for type systems. For instance, a Prolog program may perhaps not terminate, but all Datalog programs will terminate. But is Datalog expressive enough? Not sure. Could be cool to try it out though. Also, some advanced systems might be able to detect that no real progress is possible. For example being able to prove that the number of "subqueries" to be tried will increase faster than the number of "subqueries" that can be resolved. But this is really the frontier of programming language design...
Re: is type checking in D undecidable?
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 function `bool typeChecks(string code)` and then do this (similar to the halting problem): ``` enum int x = typeChecks(import(__FILE__)) ? "abc" : 100; ```
Re: mysql-native Help required
On 10/22/20 11:00 AM, Vino wrote:
On Thursday, 22 October 2020 at 14:08:30 UTC, Steven Schveighoffer wrote:
On 10/22/20 7:04 AM, Vino wrote:
Hi All,
Request your help on the below code as it is not working as expected.
GetConnections.d
module common.GetConnections;
import mysql;
class Connections
{
private Connection conn;
auto constr =
"host=localhost;port=3910;user=user;pwd=password#;db=testdb";
I'd declare this immutable, so it's not stored in the class:
immutable constr = "...";
this.conn = new Connection(constr);
You are trying to assign an instance member at compile time, with no
actual instance.
You need a constructor
this() { this.conn = new Connection(constr); }
}
GetHost.d
import common.GetConnections;
import std.array : array;
import std.variant;
import mysql;
import std.stdio: writeln;
void main()
{
auto conn = new Connections();
Row[] data = conn.query("SELECT * FROM hostlog").array;
writeln(data[]);
}
The rest should work.
-Steve
Hi Steve,
Thank you very much, I tried your solution, still not working
File: GetConnections.d
module common.GetConnections;
import mysql;
class Connections
{
private Connection conn;
immutable constr =
"host=localhost;port=3910;user=user;pwd=password#;db=testdb";
this() { this.conn = new Connection(constr); }
}
Error:
source/common/GetHost.d(11,25): Error: none of the overloads of query
are callable using argument types (Connections, string), candidates are:
/root/.dub/packages/mysql-native-3.0.0/mysql-native/source/mysql/commands.d(321,13):
mysql.commands.query(Connection conn, const(char[]) sql,
ColumnSpecialization[] csa = null)
/root/.dub/packages/mysql-native-3.0.0/mysql-native/source/mysql/commands.d(334,13):
mysql.commands.query(Connection conn, const(char[]) sql, VariantN!32LU[]
args)
/root/.dub/packages/mysql-native-3.0.0/mysql-native/source/mysql/commands.d(342,13):
mysql.commands.query(Connection conn, ref Prepared prepared)
/root/.dub/packages/mysql-native-3.0.0/mysql-native/source/mysql/commands.d(357,13):
mysql.commands.query(Connection conn, ref Prepared prepared,
VariantN!32LU[] args)
/root/.dub/packages/mysql-native-3.0.0/mysql-native/source/mysql/commands.d(364,13):
mysql.commands.query(Connection conn, ref BackwardCompatPrepared prepared)
source/common/GetParams.d(11,25): ... (2 more, -v to show)
Different error:
Row[] data = conn.query("SELECT * FROM hostlog").array;
This is trying to call mysql-native's UFCS query function on
Connections, which isn't valid. You need to call it on conn.conn.
But there's no access to the private Connection conn inside the
Connections class. I'm not sure what the class is for anyway, so it's
hard for me to suggest a proper alternative. Are you just trying to
encapsulate the connection string? I'd suggest instead of a whole class,
just a factory function:
Connection getConnection()
{
return new Connection("...");
}
-Steve
Re: is type checking in D undecidable?
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 :)
Re: is type checking in D 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 by resource bounds? "Decidable" is a term that means that there are some cases which cannot be decided even if you had near infinite computational resources at your disposal. So it is a very theoretical term, and not very practical. I don't know what kind of solvers those languages use, so I am not exactly sure what they mean by "termination checker". In general, it is hard to tell if a computation is long-running or unsolvable.
Re: is type checking in D undecidable?
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 decidable in D, but impractical in terms of compile time. Yep. Within some non-exponential CTFE speed factor that's equivalent to saying your program might run too long. You probably mean more advanced type systems where these things are expressed more implicitly. Basically type systems where you can express and resolve properties related to infinite sizes. D does not have such capabilities, so you have to go out of your way to end up in that territory in D. Where "out of your way" means what? Use of templates with potentially unbounded recursive expression? Other? 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 by resource bounds?
Re: is type checking in D undecidable?
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 more advanced type systems where these things are expressed more implicitly. Basically type systems where you can express and resolve properties related to infinite sizes. D does not have such capabilities, so you have to go out of your way to end up in that territory in D.
is type checking in D undecidable?
Is type checking in D undecidable? Per the wiki on dependent types it sure looks like it is. I assume that it's well known to the compiler contributors that D type checking is undecidable which, among other reasons, is why we have things like template recursion limits. Confirmation of the assumption or refutation would be most welcome.
Re: Recommended way to use __FILE__/__LINE__ etc.
On Thursday, 22 October 2020 at 16:03:45 UTC, H. S. Teoh wrote: On Thu, Oct 22, 2020 at 03:32:57PM +, Andrey Zherikov via Digitalmars-d-learn wrote: There are two ways how __FILE__, __LINE__ etc. can se used in function parameters: as regular parameters and as template parameters: [...] What is recommended way? What are pros/cons of each case? I don't know what's the "recommended" way, but generally, I prefer to pass them as regular parameters. Otherwise you will get a lot of template bloat: one instantiation per file/line combination. However, sometimes there is not much choice: if your function is variadic, then you pretty much have to use template parameters, 'cos otherwise you won't be able to pick up the __FILE__/__LINE__ of the caller with default arguments. T You will. This is possible since v2.079.0 (March 2018): https://dlang.org/changelog/2.079.0.html#default_after_variadic So yeah, always pass them as function parameters to avoid bloat.
Re: Recommended way to use __FILE__/__LINE__ etc.
On Thu, Oct 22, 2020 at 03:32:57PM +, Andrey Zherikov via Digitalmars-d-learn wrote: > There are two ways how __FILE__, __LINE__ etc. can se used in function > parameters: as regular parameters and as template parameters: [...] > What is recommended way? > What are pros/cons of each case? I don't know what's the "recommended" way, but generally, I prefer to pass them as regular parameters. Otherwise you will get a lot of template bloat: one instantiation per file/line combination. However, sometimes there is not much choice: if your function is variadic, then you pretty much have to use template parameters, 'cos otherwise you won't be able to pick up the __FILE__/__LINE__ of the caller with default arguments. T -- Knowledge is that area of ignorance that we arrange and classify. -- Ambrose Bierce
Recommended way to use __FILE__/__LINE__ etc.
There are two ways how __FILE__, __LINE__ etc. can se used in
function parameters: as regular parameters and as template
parameters:
void rt(string file=__FILE__, int line=__LINE__, string
func=__FUNCTION__)
{
writeln(file,"(",line,"): ",func);
}
void ct(string file=__FILE__, int line=__LINE__, string
func=__FUNCTION__)()
{
writeln(file,"(",line,"): ",func);
}
What is recommended way?
What are pros/cons of each case?
Re: mysql-native Help required
On Thursday, 22 October 2020 at 14:08:30 UTC, Steven
Schveighoffer wrote:
On 10/22/20 7:04 AM, Vino wrote:
Hi All,
Request your help on the below code as it is not working as
expected.
GetConnections.d
module common.GetConnections;
import mysql;
class Connections
{
private Connection conn;
auto constr =
"host=localhost;port=3910;user=user;pwd=password#;db=testdb";
I'd declare this immutable, so it's not stored in the class:
immutable constr = "...";
this.conn = new Connection(constr);
You are trying to assign an instance member at compile time,
with no actual instance.
You need a constructor
this() { this.conn = new Connection(constr); }
}
GetHost.d
import common.GetConnections;
import std.array : array;
import std.variant;
import mysql;
import std.stdio: writeln;
void main()
{
auto conn = new Connections();
Row[] data = conn.query("SELECT * FROM hostlog").array;
writeln(data[]);
}
The rest should work.
-Steve
Hi Steve,
Thank you very much, I tried your solution, still not working
File: GetConnections.d
module common.GetConnections;
import mysql;
class Connections
{
private Connection conn;
immutable constr =
"host=localhost;port=3910;user=user;pwd=password#;db=testdb";
this() { this.conn = new Connection(constr); }
}
Error:
source/common/GetHost.d(11,25): Error: none of the overloads of
query are callable using argument types (Connections, string),
candidates are:
/root/.dub/packages/mysql-native-3.0.0/mysql-native/source/mysql/commands.d(321,13):
mysql.commands.query(Connection conn, const(char[]) sql,
ColumnSpecialization[] csa = null)
/root/.dub/packages/mysql-native-3.0.0/mysql-native/source/mysql/commands.d(334,13):
mysql.commands.query(Connection conn, const(char[]) sql,
VariantN!32LU[] args)
/root/.dub/packages/mysql-native-3.0.0/mysql-native/source/mysql/commands.d(342,13):
mysql.commands.query(Connection conn, ref Prepared prepared)
/root/.dub/packages/mysql-native-3.0.0/mysql-native/source/mysql/commands.d(357,13):
mysql.commands.query(Connection conn, ref Prepared prepared,
VariantN!32LU[] args)
/root/.dub/packages/mysql-native-3.0.0/mysql-native/source/mysql/commands.d(364,13):
mysql.commands.query(Connection conn, ref BackwardCompatPrepared
prepared)
source/common/GetParams.d(11,25):... (2 more, -v to show)
...
From,
Vino.B
Re: mysql-native Help required
On 10/22/20 7:04 AM, Vino wrote:
Hi All,
Request your help on the below code as it is not working as expected.
GetConnections.d
module common.GetConnections;
import mysql;
class Connections
{
private Connection conn;
auto constr =
"host=localhost;port=3910;user=user;pwd=password#;db=testdb";
I'd declare this immutable, so it's not stored in the class:
immutable constr = "...";
this.conn = new Connection(constr);
You are trying to assign an instance member at compile time, with no
actual instance.
You need a constructor
this() { this.conn = new Connection(constr); }
}
GetHost.d
import common.GetConnections;
import std.array : array;
import std.variant;
import mysql;
import std.stdio: writeln;
void main()
{
auto conn = new Connections();
Row[] data = conn.query("SELECT * FROM hostlog").array;
writeln(data[]);
}
The rest should work.
-Steve
Re: mysql-native Help required
On Thursday, 22 October 2020 at 11:04:53 UTC, Vino wrote:
class Connections
{
private Connection conn;
auto constr =
"host=localhost;port=3910;user=user;pwd=password#;db=testdb";
this.conn = new Connection(constr);
}
where Connections class constructor implemented?
Re: More elaborate asserts in unittests?
On Thursday, 22 October 2020 at 04:20:35 UTC, Mathias LANG wrote: Unfortunately this switch still has some bugs, so you can easily run into linker errors. I'm hoping to ultimately make it the default though. Which is more of a template emission problem because `-checkaction=context` uses a templated hook in druntime (`core.internal.dassert._d_assert_fail`). `-checkaction=context` should support any unary and binary expression and properly format all data types (unless we've missed some special case). Note that it currently does not support complex expressions (e.g `assert(0 <= a && a < 10);` but I/someone else might implement that in the future.
mysql-native Help required
Hi All,
Request your help on the below code as it is not working as
expected.
GetConnections.d
module common.GetConnections;
import mysql;
class Connections
{
private Connection conn;
auto constr =
"host=localhost;port=3910;user=user;pwd=password#;db=testdb";
this.conn = new Connection(constr);
}
GetHost.d
import common.GetConnections;
import std.array : array;
import std.variant;
import mysql;
import std.stdio: writeln;
void main()
{
auto conn = new Connections();
Row[] data = conn.query("SELECT * FROM hostlog").array;
writeln(data[]);
}
From,
Vino
