It’s a principle that you try to apply as much as possible. Doesn’t mean it’s always possible with primitives. Applying this principle can mean only exposing APIs that check for a valid index at runtime.
Conversation
Even dependent types really boil down to “runtime checks the compiler knows well so are easier to remove via optimization”
2
1
9
Just to clarify: you don't really need to check everything at runtime in DTs. Stuff to the ‘right’ of the colon is evaluated statically. In this example, the addition in the types would be computed during type checking/elaboration:
Quote Tweet
Replying to @moonriseTK @maxdesiatov and @KaraLangOrg
It'd come down to the types you give your indexing and concatenation functions. Eg:
_[_] : {n} {A} -> Array n A -> Fin n -> A
_+_ : {n m} {A} -> Array n A -> Array m A ->
Array (n + m) A
2
3
Yes, thank you, I am speaking *very* loosely. I find that when folks first hear about dependent types they see it as a magic way to remove every runtime check, when it’s more a way to remove *many* runtime checks
2
2
i feel frustrated by this perspective, because there is a crisp and succinct characterization of what makes a type system dependent: if and only if its types can mention terms. this is unrelated to whether the compiler is able to erase types at runtime, or other optimizations.
1
2
it's not that a dependent type system isn't a way to magically remove every runtime check, it's that "removing runtime checks" and "being a dependent type system" are two orthogonal characteristics of a language.
2
1
I agree that they are orthogonal and I agree your description is succinct but I fear it is too jargon heavy to get the idea across to many people
2
1
I think that is more accessible but IMHO it explains the “what” but not the “why” or the “how”, which is why I tend to lean towards more when trying to explain something to someone who may not know about a topic yet
2
1
Yeah, by some definition, ‘dependent types’ refers to term-on-type and type-on-type dependency as well. It’s often conflated with ‘full spectrum dependent types’ though.