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
Brendan Zabarauskas
@brendanzab
Ah gotcha, sorry for nitpicking! hehe :) Can definitely be a tricky thing to explain. I remember being confused over type-safe format strings, wondering if I'd end up parsing them twice during runtime because of how I was representing them in the types.
2
1