Remix.run Logo
▲ jordan_bonecut 2 hours ago

Dependent types can be achieved via “ideal Generics”. Very undocumented and not ready to commit to how they work yet, but the basic idea is that a type can be generic on a value.

▲ch4s3 2 hours ago | parent [-]

How long have you been working on this?

▲jordan_bonecut 2 hours ago | parent [-]

I have been building little prototype languages for years. This iteration which is heavily AI powered is a couple weeks old

▲ch4s3 an hour ago | parent [-]

Oh cool, it's amazing how quickly you can stand up a language now, I love it. I'd love to exchange ideas, I really like what you're doing.

How are you doing resolution of your dependent(refined?) types? I've been using Z3, but you're clearly doing something else here.