Algorithms from Core.hs

[MonoidMusician]

I have started converting most of the algorithms from Core.hs, but they need to be finished and verified.

• shift and subst are important to get tested to ensure correctness, but I think I copied and converted them over fully.
• normalizeWith needs to be completed in full, and tested, as it is one of the most important parts of Dhall. isNormalizedWith can be just derived from it for now, but should be updated with a real algorithm. Maybe they can be merged, returning Tuple Boolean (Lazy (Expr s a))
• Related: I don’t understand boundedType and whether it applies to a strict implementation and if I actually need laziness somewhere. Actually implement boundedTypeG.

[MonoidMusician]

dhall-lang/dhall-haskell#612 (comment)
http://www.haskellforall.com/2017/09/type-driven-strictness.html

[MonoidMusician]

• Need to move normalization into its own file.
• Break apart normalization into various passes.
• Break apart typechecking into its cases, give names to common elements.
  • Then work on generalizing check and ensure to adapt to a unification algorithm.