Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improved error handling #126

Merged
merged 37 commits into from
Nov 16, 2021
Merged

Improved error handling #126

merged 37 commits into from
Nov 16, 2021

Conversation

kjekac
Copy link
Collaborator

@kjekac kjekac commented Oct 2, 2021

This replaces the old ErrM with Data.Validation, which allows us to accumulate errors in cases where it is not strictly necessary for an error-prone computation to actually have access to the result of a previous error-prone computation. This allows us to output all errors during typechecking, instead of only the first one.

To take advantage of this however, the relevant code cannot make use of the Monad interface (because Data.Validation lacks a Monad instance) but must restrict itself to Applicative. Because of this, Type.hs has been largely refactored. The language extension ApplicativeDo allows us to use a restricted form of do-notation in some cases where it makes syntactic sense, but in the absolute majority of cases, the style is now much more "obviously functional". Imo the separation of concerns that this style enforces is significantly better – the validity checks have largely been factored out from the actual AST construction.

For an example of this in action, see the interplay between typecheck and lookupVars (old version, new version). Previously, the data validation was very embedded in the data construction – lookupVars performed all sorts of checks. Now, since one error-prone computation can no longer rely on the result of another, we are forced to make lookupVars pure in order to be able to pass its result to splitBehaviour. This makes its implementation much cleaner, while forcing the data validation to be carried out separately by the helper functions noDuplicateContracts and noDuplicateVars, both of which are also more clean/clear/focused than the previous implementation. Very good separation of concerns, imo.

However, in some cases we do need the result of a previous computation, either because it is actually required, or because Happy expects a function with the same signature as >>=. In these cases, there are two options:

  1. Use bindValidation from Data.Validation. We tell Happy to use this function, since it has the exact same type signature as >>=. The only reason that there is no Monad instance for Validation is that setting (>>=) = bindValidation would break the laws which govern how Applicative should relate to Monad.
  2. Use Either, and cast back and forth to Validation. In Data.Validation there are several functions/lenses which help with the casting. This is recommended whenever proper monadic do-notation is required, since Either actually has a Monad instance. This approach is used in CLI.hs – see the use of toEither on L199 and then also of ^. revalidate on L202. The latter can cast f (Validation e a) <-> f (Either e a), which is why we use it after the for. (Note: ^. revalidate could technically have been used in both places since it can do the same two-way cast with or without the functor f.)

Importantly though: Using these options does not necessarily mean that the computation will always break on the first error. Any sub-computation which has been composed in the applicative way will still accumulate its errors. So for example the typechecking will output many errors but we will never be able to start with any code generation until the typechecking succeeds completely, which makes sense. So we will generally want to restrict ourselves to the applicative style within one module, and then chain these together using the Either monad. To the extent that this is possible of course, but I was surprised how easy the typechecking was to adapt once I had figured out the singleton stuff (see point 2 below).

Some other changes:

  1. Main.hs has been split into CLI.hs and main/Main.hs. By removing Main from the primary codebase we allow test/Test.hs to depend on the compile function, instead of having to reimplement it.
  2. There now exists a singleton type SType a. It has exactly three constructors: SInteger :: SType Integer, SBoolean :: SType Bool and SByteStr :: SType ByteString. That is, it allows us to infer a type from a value and vice versa, something which the old MType doesn't allow. The new module Syntax/Types.hs contains this type, together with MType (which is still needed) and some infrastructure to go between these two, Haskell's own types, and EVM.ABI.AbiType. Introducing SType is not strictly necessary but makes the implementation of the new typechecking style easier/cleaner, and reduces code repetition in several other places.

This PR does not yet adapt any modules except Type, Parse and K to using Data.Validation, since the changes required in the other backends are more involved, at least if we want to make them applicative. Hence, #108 won't be closed by this PR. But it's a start!

@kjekac kjekac marked this pull request as ready for review October 2, 2021 23:52
@kjekac kjekac requested a review from d-xo October 2, 2021 23:52
@kjekac kjekac force-pushed the errorlogger branch 2 times, most recently from ef3f545 to 0b4c157 Compare October 3, 2021 02:03
Copy link
Collaborator

@d-xo d-xo left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Generally this seems very nice, and I don't really have many comments / changes, more questions surrounding some of the more intricate parts of the new implementation. The Loc, Update, TExp rework seems like it removes a lot of boilerplate / duplication in an elegant way, and the new Error type seems sensible. I haven't given the reworked typechecker a full read, but at a first look I agree that the new structure imposed on us by the usage of Validation is cleaner.

I think the big downside here that the guts of the Error type and the new Loc / Update types are more complex and use a lot more clever haskell, and I personally find it pretty hard to fully grok the details of what's going on there. This will presumably introduce some overhead for new contributers, especially those who are not very familiar with haskell.

src/CLI.hs Outdated Show resolved Hide resolved
src/Coq.hs Outdated Show resolved Hide resolved
src/Error.hs Outdated Show resolved Hide resolved
src/Syntax/TimeAgnostic.hs Show resolved Hide resolved
src/Syntax/Types.hs Show resolved Hide resolved
src/Syntax/Types.hs Outdated Show resolved Hide resolved
src/Syntax/Types.hs Outdated Show resolved Hide resolved
src/Syntax/TimeAgnostic.hs Outdated Show resolved Hide resolved
src/Parse.y Show resolved Hide resolved
src/Syntax/Untyped.hs Outdated Show resolved Hide resolved
@kjekac
Copy link
Collaborator Author

kjekac commented Nov 1, 2021

I have no idea why the builds are failing. Look at the diff of commit eb0c990, it literally changes nothing that could break. :/ I'll try to figure it out tomorrow unless you do first.

@d-xo
Copy link
Collaborator

d-xo commented Nov 9, 2021

@kjekac regarding ci, it seems to be failing while cachix-action is running. I would probably start by upgrading the install-nix-action and cachix-action to their latest releases respectively and see if that fixes the problem. You can do this by editing the comits in the build.yml

@kjekac kjekac merged commit 5d566a8 into master Nov 16, 2021
@kjekac kjekac deleted the errorlogger branch November 16, 2021 14:42
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants