News for hackers. Stuff that matters.
Re:Names are not type safety by remexre on Monday November 02, 2020 @12:05PM (#24970331)
What dependent types would protect you against would be the parser itself returning data. I think it'd be quite difficult to do this for the case of an email or URL, but for cases like "length values must be non-negative," a parser/validator with a type like

    parseLength :: JSON -> Either Error (Sigma (l : Length). lengthToDouble l >= 0.0)
is reasonable, and I'm sure somewhere in the literature there's an indexed monad or something for building parsers/validators out of these, that keeps track of the properties while combining parsers like these.

There are no comments on this comment yet.