not all strings are valid, and that's beautiful
1
25
Conversation
thinking about dependently typed strings
2
14
putting words to my vague thoughts: we have lots of different types of strings but they're very ad hoc, e.g. "utf8 string", "ascii string", "bytestring", "valid identifier", "valid json string". these are all one-offs. is there a "string type family" that unifies all of these?
2
3
Show replies
Yeah, this fits well with the view of types as predicates on representations, and a representation as a record of the path of choices made to produce a value, or needed to consume it. The hard part is of course what logic you allow. Regexes have been done; CIC seems tractable?
2