Conversation

Lucretiel 🦀
@Lucretiel
Okay here's one for the "make impossible states unrepresentable" crowd: I have a list of items, precisely one of which is always selected. How to represent this? - per-item bool allows for 0 or more selection - separate "selected" ID or index allows for invalid selection
10
17
steveklabnik
@steveklabnik
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.
1
20
Brendan Zabarauskas
@brendanzab
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
Brendan Zabarauskas
@brendanzab
·
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
steveklabnik
@steveklabnik
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
/plæd•fɪnʧ/ is (somewhat) offline 🌙
@plaidfinch
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
steveklabnik
@steveklabnik
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