[kreetx]

We might be coming from different backgrounds and hence not immediately understand each other, but, at least in Haskell if the types are precise in the sense that you can't construct invalid values, then using such types will make your programs more correct.

For example, if you want a program from a number to HTML, then if the HTML type is a syntax tree type of all valid HTML rather than wrapper around string, then filtering LLM output by that type will make it more correct than a string wrapper kind of type (as with the latter, any program generated by the LLM which returns a string and wraps it into HTML will do).

The actual use cases might not go as extreme as the above, but the idea is that the "tighter" your type is, the better it is on pruning LLM outputs from invalid programs.

[oivey]

Suppose you write a program that computes the sum of two input numbers. Suppose the two inputs are 1 and “a”. If it returns “1a” or 12 or whatever, the program is incorrect. Its correctness does not hinge on type safety. A untyped program could detect that one of the inputs is unexpected and correctly raise an error. Typing may make it easier to detect this error (or not). Fundamentally, adding type information does not make the above program “more” correct. It’s either correct, or it’s not.

You can write a sorting algorithm in assembly, and it can be correct. Rewriting in Haskell won’t make it “more” correct.

There’s an undercurrent of people espousing strictly types languages (not accusing you) who believe that somehow programs written in them are better. They’re not. They either serve their purpose, or they don’t. Strict typing is a tool. Sometimes it’s enabling. Sometimes (example: horrible polymorphism in most strictly typed languages like C++/Java/copy cats) it’s a hinderance. Strictly typed languages aren’t strictly better than non-strictly typed ones.