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