unisonweb / unison

A friendly programming language from the future
https://unison-lang.org
Other
5.76k stars 269 forks source link

it's too easy to make a mistake with getOrElse and raise/bug/etc #4070

Open ceedubs opened 1 year ago

ceedubs commented 1 year ago

Code like the following has bitten @stew, a couple of people in the public Slack and me:

-- example with "bug"
myOption |> getOrElse (bug "it shouldn't be None")

-- example with "raise"
myOption |> getOrElse (raise (Generic.failure "shouldn't be None" ()))

This doesn't do what you want it to do, because getOrElse is strict in both arguments, so you will hit the bug/raise every time. Ideally you'd get a compile error about this, but since raise and bug are universally quantified in their return type, they are also happy to pose as a lazy 'a.

You can achieve the desired behavior by using getOrElse':

myOption |> getOrElse' '(bug "it shouldn't be None")

There are probably times when you are doing something like myOption |> getOrElse "default" and don't care about the laziness, after seeing several people who know what they are doing get tripped up by it, I'm inclined to say that the strict version should be deemphasized a bit. My suggestion would be to rename the current getOrElse to something signifying the strictness (maybe getOrElse!?) and rename the current getOrElse' to getOrElse. Then you would have the following:

Optional.getOrElse : '{e} a -> Optional a ->{e} a

-- Could be a different name
Optional.getElse! : a -> Optional a -> a
pchiusano commented 1 year ago

Changing the names won't make any difference, since bug a will also have the type '{e} x forall x.

> Some 1 |> getOrElse' (bug "oog")

This typechecks and bombs with bug "oog".

I'm not sure the fix for this, but it's not something that can be solved at the library level, it's more like a typechecker fix. Going to transfer this issue to the Unison repo.

pchiusano commented 1 year ago

Potentially an easy fix is to not allow bug or todo or Exception.raise to be unguarded in a function application.

That is, if you ever write foo (bug 123), there is very little chance that's what you want, since that is equivalent to bug 123. There's no point in passing an evaluation of bug to a function, since functions evaluate their arguments before being called.

But can we do better than special casing bug and todo and Exception? (Since this also comes up with like, Abort or Throw or other abilities that allow early termination)

Here's an idea: when typechecking a function application (the synthesizeApp fn in the typechecker), check if the argument is universally quantified over its return type. If yes, then it's necessarily an "early termination" operation, and that can just be a type error with a nice error message.

The function `bug` terminates this expression early, but it will be evaluated before the
call to `getOrElse`:

  12 |    |> getOrElse (bug 123)
                        ^^^^^^^

Did you mean to put a `'` around this argument? Or perhaps use a non-strict version of `getOrElse`?

Elaborating on the implementation a bit

Here's the signature of synthesizeApp, it's synthesizeApp functionTerm functionType arg:

-- | Synthesize the type of the given term, `arg` given that a function of
-- the given type `ft` is being applied to `arg`. Update the context in
-- the process.
-- e.g. in `(f:t) x` -- finds the type of (f x) given t and x.
synthesizeApp ::
  (Var v, Ord loc) =>
  Term v loc ->
  Type v loc ->
  (Term v loc, Int) ->
  M v loc (Type v loc, Wanted v loc)

When arg is a Term.Apps' f args, lookup the type of f. If it's known (which it will be if it's a call to bug or an ability operation like raise or throw) and fully saturated, see if it returns a free type variable. If yeah, that's this case and it merits a special error.

You could add a special case for todo in this same spot, to avoid having todo trigger this.

The rest is plumbing code - create a new error constructor and then render a nice message.

SystemFw commented 1 year ago

I wouldn't include todo there, I want to be able to put it wherever I want to make things compile

aryairani commented 1 year ago

But don't say "terminates early" based on the type if it might actually be an infinite loop.

ceedubs commented 1 year ago

@pchiusano ooh I had mentally written this off as impossible to fix, but your proposal sounds really good! I like that it's a general solution as opposed to an ad-hoc attack on raise and bug.

@SystemFw might be right about special-casing todo, though I could probably be convinced either way.