Comment by beders

> Still no static types for "Strings that end with a dot" or "Strings that match [a-z]+"

Sure there are. :) Technically speaking, anyway. Here’s a type for “strings that end with a dot”:

  -- | A string that ends in the character '.',
  -- represented as a string without its trailing dot.
  newtype StringEndingInDot = StringEndingInDot String

  fromString :: String -> Maybe StringEndingInDot
  fromString str = case reverse str of
    '.':cs -> Just $ StringEndingInDot (reverse cs)
    _      -> Nothing

  toString :: StringEndingInDot -> String
  toString (StringEndingInDot str) = str ++ "."

And here’s a type for “strings that match [a-z]+”:

  data Letter = A | B | C | D | ... | X | Y | Z
  type StringAZ = NonEmpty Letter

Now, admittedly, I would never use either of these types in real code, which is probably your actual point. :) But that’s a situation where there is a pragmatic “escape hatch” of sorts, since you can create an abstract datatype to represent these sorts of things in the type system without having to genuinely prove them:

  module StringEndingInDot(StringEndingInDot, fromString, toString) where
    newtype StringEndingInDot = StringEndingInDot { toString :: String }

    fromString :: String -> Maybe StringEndingInDot
    fromString str = case reverse str of
      '.':_ -> Just $ StringEndingInDot str
      _     -> Nothing

You may rightly complain that’s a lot of boilerplate just to represent this one property, and it doesn’t compose. That’s where the “Ghosts of Departed Proofs” paper (https://kataskeue.com/gdp.pdf) cited in the conclusion can come in. It provides a technique like the above that’s a little more advanced, but brings back composition.

> It's pretty cute. Still no static types for "Strings that end with a dot" or "Strings that match [a-z]+" or "Strings that are proper nouns". ;)

That’s not true, you can wrap these in types that can only be constructed from valid data, and from that point on you can be sure everything is correct.

Idris:

  data EndsWith : Type where
    EndsWithPeriod : (s: String) -> { auto prf : ("." `Strings.isSuffixOf` s = True) } -> EndsWith

  s : EndsWith
  s = EndsWithPeriod "."

  -- Value of type False = True cannot be found
  -- s2 : EndsWith
  -- s2 = EndsWithPeriod ""

The noun one might be possible -- I'm honestly less familiar with what a proper noun is offhand. (E: prefix=>suffix)

> "Use a data structure that makes illegal states unrepresentable." is not effort spent well.

Am I to presume you do all your programming in assembly (or opcodes?), since you never need to distiguish integers from strings in your source code?

> Gödels incompleteness theorems

is never relevant in the real world.

In the general case, all real computers are broken.

Ignoring all the convoluted type examples here, the simplest case is that you create the type that matches the parsed value. For example, you can create an EmailAddress class that can only contain valid email addresses. Instead of String, you use EmailAddress whenever you need to ensure the valid parsed value.

Proper nouns are finite, albeit quite numerous, so these _could_ be enumerated as a sum type.