What are Types? Kinds? Constraints? Propositions? Are these always values?
-
This Tweet is unavailable.
-
-
This Tweet is unavailable.
-
Replying to @jdegoes
I'm not sure I agree so universally. Values are granted a lot of power, and consequently need to be evaluated (implying some sort of runtime). Having more constraints on what these things can do can remove the need for evaluation (and its fragility, partiality and performance).
1 reply 0 retweets 3 likes -
Replying to @propensive @jdegoes
c.f. reflection macros, where types are values. But having said that, one person's compiletime is the next person's runtime!
3 replies 0 retweets 0 likes -
Replying to @propensive @jdegoes
I think it's nicer when types and kinds can be manipulated with the same operational semantics (and even syntax!) we use for normal values. Haskell at least now has DataKinds. Scala had path-dependent types since very early, but it's really bulky to use.
1 reply 0 retweets 1 like -
Yes, but the more freedom you have to manipulate them arbitrarily, the less freedom you have to reason about them quickly... it's definitely a trade-off! :)
1 reply 0 retweets 1 like -
Replying to @propensive @jdegoes
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.
1 reply 0 retweets 2 likes -
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.
3 replies 0 retweets 0 likes -
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...
1 reply 0 retweets 0 likes
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.
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.