On Thursday, 20 July 2023 at 13:44:15 UTC, Commander Zot wrote:
>wouldn't it be possible to have something like first class types (at compile time) to replace tamplates for type logic with regular functions executed at CTFE?
In some programming languages I have used in the past specifically Lisp when you define a type you can give it a list of predicates to define the type, its mostly the same except slightly fancier in scala and haskell, in D we already have support for predicates they are called contracts, and you can apply type checking using in, out, assert, and invariant, this gets you most of the way there.
when you click on references you will also find one mentions theorem proving using contracts, so its been used in that same area before, if you use mixins and anonymous/voldemort types I bet you could create a nicer way of applying these contracts, getting 95% the way there. that last 5 percent would be recursive peano types and verifying coverage etc... which both are still probably possible using structs.
https://dlang.org/spec/contracts.html
reference I mentioned:
https://web.archive.org/web/20080919174640/http://people.cs.uchicago.edu/~robby/contract-reading-list/
I guess the next question is, how far can you take contracts for type level programming, and at that point would first class types be necessary.
//basic example
auto test(float a)
in (a < 255)
out(r; r.x > 0)
{
Struct S {
float x;
float y;
float z;
invariant {
assert(x < 255 && x > -60);
assert(y < 255 && y > -60);
assert(z < 255 && z > -60);
}
}
S ret = S(a, 100.0, 100.0);
return ret;
}
I did not check if the code compiled but that is the basic idea, there are also examples on the docs I linked, hopefully this gave you some more stuff you can try out / research, and this is also something I am interested in so I would like to see updates if you come up with anything.