unisonweb / unison

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

pure function arrow ->· to make abilities more learnable #738

Open atacratic opened 5 years ago

atacratic commented 5 years ago

In a nutshell: change the sugar for inferred pure functions from -> to ->·, and make that sugar bidirectional so you can input it as well (and also the keyboard-friendly variant ->.).

Motivation

At the moment people need to learn/remember the following, to use abilities.

When you give Unison a plain -> or ' (with no {…}) you're asking it to infer some abilities. When Unison gives you a plain -> or ', it means a pure function.

This inconsistency is surprising and hard to learn/retain, so the effect will be that people will mostly not be sure what guarantees a -> is giving them / not giving them about purity.

Current design background

When faced with something like

increment x = x + 1

Unison infers a type forall e. Nat ->{e} Nat. By parametricity this type actually guarantees that the function is pure, so it's in a sense equivalent to Nat ->{} Nat - although nonetheless that's actually a different type.

Unison doesn't actually print forall e. Nat ->{e} Nat: it contracts it to Nat -> Nat, because we don't want all that {e} noise for such a common case. Any ability type variable appearing in the outermost forall, which is otherwise mentioned only once in the type, is contracted in this way. (Type.hs, removePureEffects).

This contraction only works one way (Unison outputting code) - if you input -> then it instead means 'please do ability inference for me`.

Plan

Switch to contracting forall e. Nat ->{e} Nat to Nat ->· Nat on output. Also support the reverse direction, so the user can type Nat ->· Nat (or the keyboard-friendly version Nat ->. Nat) and have that mean the same as forall e. Nat ->{e} Nat.

That way -> always just means 'infer the abilities for me please', and ->· always means what it expands to. The ->· surfaces the purity guarantee to the user, so they'll realize and understand its value, in a minimally obtrusive way. They will also then see that -> is leaving ability info unspecified, and so learn that it does not come with a purity guarantee - hopefully preventing the nasty surprises discussed in #717.

The extra character in ->· is a 'middle dot', U+00B7, part of the 'Latin 1 punctuation and symbols' unicode character set.

Notes on the expansion/contraction:

This overall plan got agreed in slack here subject to satisfactory answers to the open questions above.

Related: Today, if I input

f : Nat ->{} Nat
f x = x + 1

then Unison tells me it has type f : Nat -> Nat rather than f : Nat ->{} Nat. I can't quite see whether it's Type.removePureEffects that's doing this, or what, but it breaks the story "-> means 'infer', purity is always made visible, and types with different meanings are not randomly swapped with one another", so I think we should stop this happening as part of work on this issue.

runarorama commented 5 years ago

I kind of like this.

atacratic commented 5 years ago

Two thoughts:

  1. Thinking about the interaction between the two types of sugar: I wonder if we'd extend this to '·Nat expanding to forall e. () ->{e} Nat. Starting to look a bit like perl, but on the other hand it seems like an arbitrary syntactic irregularity not to include this.

  2. I think we'd also need a line on when the user should write Nat ->{} Nat, when they should write Nat ->· Nat, and if it even makes a difference.

zenhack commented 5 years ago

Quoting Chris Gibbs (2019-08-18 11:03:46)

Thinking about the interaction between the two types of sugar: I wonder if we'd extend this to '·Nat expanding to forall e. () ->{e} Nat. Starting to look a bit like perl, but on the other hand it seems like an arbitrary syntactic irregularity not to include this.

One Snafu with this: if we go the route that a period can be used to type it on most keyboards, then this would translate to .Nat, which currently just refers to an identifier at the root of the namespace.

TomasMikula commented 5 years ago
  • The forall binder needs to be on the outside. So (forall e. a ->{e} b) -> [a] -> [b] is not affected. ?? Is this right? It's not quite clear to me why. Doing it this way has the odd property that the rendering of a subtree of a type AST depends on the wider AST it's embedded in. Also the example seems to mean 'a function that takes a pure function', so why not render it like that?

If the convention is that unbound variables are bound on the very outside, then (a ->· b) -> [a] -> [b] would mean forall e. (a ->{e} b) -> [a] -> [b], which is different than (forall e. a ->{e} b) -> [a] -> [b].