After reading the paper and watching the lecture, I think I know what it means that Types are first class values.
In verse `=` is unification and not assignment or comparison. Meaning its a constraint on the lhs and rhs. Unification is also an expression meaning it can be normalized to a value e.g. `x=3` normalizes to `3`
Expressions can be sequenced with `;` but note this is nothing like imperative programming due to unification. These sequences normalize to the last expression in the sequence but the unifications in all subexpressions apply to the whole sequence. Thus `=` appearing in subexpressions in any order does not change the resulting value (since the compiler uses normalization)
Now functions can be seen as lambdas or anonymous functions to these sequences of expressions where the arguments are also constraints! These functions themselves are values. Thus functions are first class.
Another key aspect of unification is that functions can run backwards. Thus `swap<1,2>` will return `<2,1>. But so will `swap(p) = <1,2>` constrain `p` to `<2,1>. Thus the meaning of function is no longer just a procedure. But more of a specification or constraint.
And this is exactly what types are in Verse. Types are functions thus first class. When we say `i : Int` it is akin to saying `Int(i)` constraining the variable `i` based on the constraint `Int`.
Thus if you have a function that succeeds when given an even number, that function can be seen as a type of even numbers.
Oh 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.
Yes 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?
I 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.
In verse `=` is unification and not assignment or comparison. Meaning its a constraint on the lhs and rhs. Unification is also an expression meaning it can be normalized to a value e.g. `x=3` normalizes to `3`
Expressions can be sequenced with `;` but note this is nothing like imperative programming due to unification. These sequences normalize to the last expression in the sequence but the unifications in all subexpressions apply to the whole sequence. Thus `=` appearing in subexpressions in any order does not change the resulting value (since the compiler uses normalization)
Now functions can be seen as lambdas or anonymous functions to these sequences of expressions where the arguments are also constraints! These functions themselves are values. Thus functions are first class.
Another key aspect of unification is that functions can run backwards. Thus `swap<1,2>` will return `<2,1>. But so will `swap(p) = <1,2>` constrain `p` to `<2,1>. Thus the meaning of function is no longer just a procedure. But more of a specification or constraint.
And this is exactly what types are in Verse. Types are functions thus first class. When we say `i : Int` it is akin to saying `Int(i)` constraining the variable `i` based on the constraint `Int`.
Thus if you have a function that succeeds when given an even number, that function can be seen as a type of even numbers.