Proposal: First class types (at compiletime)

[MrJay]

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.