Refactor typechecker

[WardBrian]

This is following on the discussion here #966.

The typechecker has several historical oddities and design decisions that don't make sense with the way the project has gone. To be clear, I'm not anti-monad or anything, I just think the typechecker can and should be simple to read an understand. By using the OCaml exception handling internally, it's possible to make each function very clear while still returning a Result at the high-level interface to the rest of the compiler.

This mainly has implications for the developers and open PRs like #675 #742 . I'm very happy to help update those PRs as needed.

Summary:

1. Validation is gone. Each check_ function either returns the typed segment of the AST it is responsible for, or throws an error which is caught by check_program. Functions that start with verify_ either throw an error or return unit. This (indirectly) closes Semantic check should only use applicative interface #265
2. The typechecker is ~400 lines shorter now
3. The typechecker was renamed to Typechecker.ml. This was mainly because I kept Semantic_check.ml around during development so I needed a new name, I'm not attached to it.
4. The order of checks is preserved in this change. All the same errors are caught in the same order, 1-1.
5. Some error messages are improved: in particular, declared-but-undefined functions are now pointed to exactly.
6. The typechecker uses a functional, immutable symbol table.
   • This closes Investigate removing context_flags (and Symbol_table) from global state #28
   • I think this is the number one argument in favor of this rewrite, issues with Validation aside. It makes things like function overloading much easier to reason about and removes the rather hacky way of doing scope etc used before.
   • This also moves toward unifying the symbol table of stan math functions and the user defined variables and functions. Stan_math_signatures is not gone, but it is far less used and we can work on simplifying this further later.
7. This PR also undoes the movement of Error and a few other front-end specific files that got moved in Refactor warnings and add filename-in-msg #780

Why?:

1. This version of the type checker is much clearer to read and understand. There's no extra construct getting in the way, so changing error conditions or adding a new check is much simpler. You avoid things like liftA2 (a, b) |> (fun ua ub -> ... that add no functionality besides satisfying the monad
2. The environment as a functional map makes scoping logic much cleaner and an explicit part of the function signature. If a function does not return a Env.t as part of it's signature, you know it cannot edit the types. This avoids the need for (* WARNING: SIDE EFFECTING *) comments.
3. The environment being (at least partially) unified with the Stan math signatures will make refactoring the later much easier, as well as allowing a lot of nice extensions like overloading of UDFs

Submission Checklist

• Run unit tests
• Documentation
  • OR, no user-facing changes were made

Release notes

Refactored Stan typechecker.

Copyright and Licensing

By submitting this pull request, the copyright holder is agreeing to
license the submitted work under the BSD 3-clause license (https://opensource.org/licenses/BSD-3-Clause)

[SteveBronder]

Quick first review, still need to dive deeper into the code

[nhuurre]

Arguably model_name should be a field in Ast.program and also included in Env.t.

[WardBrian]

I think we do need it to be a mutable reference somewhere, unless we want to pass it as an argument to all the major frontend functions. It being in the environment makes a little more sense than in the typechecker, but I think it would still be in the Environment module, not each tenv mapping

[nhuurre]

Looks good to me. Have you talked to @rybern about PR #675 ?

[WardBrian]

I haven’t yet. The changes that he makes to the typechecker are pretty minimal though, and adapting them should be straightforward (I’d be happy to do it in his branch if he would welcome it)

[WardBrian]

I've removed the failing test (it will be addressed separately #1011) so this should be good to go with approval @SteveBronder @nhuurre

[SteveBronder]

Only one thing to fix in the tests for python, but I think besides that most of my parts are comments. So code looks good!

[WardBrian]

How does this look in the current state @nhuurre @SteveBronder?

[nhuurre]

Approved.

[WardBrian]

Just merging master in hopes that this is the next PR merged. Needs approval from @SteveBronder still before GitHub will allow it

[SteveBronder]

lgtm!