What are Types? Kinds? Constraints? Propositions? Are these always values?
-
This Tweet is unavailable.
-
This Tweet is unavailable.
-
I think we have to be careful about this meta-argument. We want the freedom to make constraints! Conversely, we don't want constraint from making constraints. And this is why I really want more unification of values, types, kinds, etc.
But my argument is that by unifying everything to the most general, we lose the advantages we get from constraints, e.g. being able to do declarative type calculations without run-like evaluation, and having tooling which supports that.
-
-
Sure, we can add constraints, but it's then just a constrained subsystem within a more general one, and you probably wouldn't get the advantages of being able to reason easily (and fast) about the constrained subsystem...
-
I have to say that the idea that "it's just values all the way down" is nice, but at least in a Scala context, there are plenty of reasons why we prefer compile errors to runtime errors: debugging the former is in a much more constrained domain.
End of conversation
New conversation -
-
-
When we unify everything with values... we also have to unify all the value-oriented tooling as well. Not doing so would be a huge loss. I think if we do this, your concern will be addressed.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
In Idris it only evaluates expressions which are known to terminate at compile time.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.