3 ms·
It is nothing new. See Dependent Types. Used by most formal proof assistants (Coq/LEAN/…) and languages like Agda and Idris. I highly recommend the book “Type
by deterministic 4y ago
It is nothing new. See Dependent Types. Used by most formal proof assistants (Coq/LEAN/…) and languages like Agda and Idris.
I highly recommend the book “Type Driven Development” if you want a great introduction to the power of DT.
- haliq 4y agoOh this is new because our notion of expressions; thus functions, are different. Sure you can have terms in types in dependent types; thus functions in types is nothing new. But again, we have a much different notion of function here. And if anything I would say types in Verse are much closer to refinement types because of its ability to apply constraints. But they are still not the same thing.
- deterministic 4y agoYes it is different but it doesn’t seem to give you anything that is better than what DT and refinement types give you. So why not simply use DT or refinement types? I know that in research you have to come up with something new to write papers about. Even if it isn’t actually better in practice. However this seems to be aimed at being a practical non-ivory tower language?
- haliq 4y agoI think your first question will be answered when spj releases details on the type system. And the second when he address the transactional distributed stuff. As of now all we have is a core language. But its not hard to read between the lines to anticipate how powerful it can be so that features that the industry needs can be built upon it.