Generative labels #1169

dhil · 2023-01-31T13:59:57Z

This PR is a rebase of #1148 on top of the latest changes to master -- in particular those made to effect handlers.

This PR also generalises the previous work the following ways:

fresh declarations can be made in any binding contexts (just like fun, var, etc.)
fresh does no longer equipped with an explicit scope, wherein the fresh labels are defined, instead it now follows the standard block-structured lexical scope of Links.

This PR also fixes a regression for session exceptions introduced by one of the previous patches, which made a change to the operation syntax at the type level. However, this change was never propagated properly, as a result session exceptions continued to use the reinterpretation of the function arrow.

allow better printing

This reverts commit 49a9a61.

This reverts commit 5150615.

Co-authored-by: Daniel Hillerström <[email protected]>

…-fresh-label

This commit fixes a regression introduced by the previous commit, wherein numeric labels wouldn't get looked up correctly in `Label.{Map,Set}`. This commit also generalises `fresh` such that it can be used locally within a binding context. Furthermore, it changes the syntax such that it no longer introduces encloses a list of bindings, but instead uses the standard block-structured scope of Links.

dhil · 2023-02-01T17:22:15Z

The feature, as implemented by this patch, does not interact well with some of Links' other features, e.g. modules. However that shouldn't be a blocker. Another thing, after doing some thinking os that I would like to repurpose new for label generation, then we can avoid introducing fresh as a keyword.

dhil · 2023-02-02T10:54:57Z

It is worth remarking that this patch further widens the gap between type-inferable expressions and type-ascribable expressions. For instance,

links> fun () { fresh `Foo; do `Foo }
fun : () {`Foo:() => a|_}-> a

The programmer can never manually ascribe the effect-type to the above function, because the label \Foo` is not in scope at the point where the type signature would be written down, e.g.

links> fun () { fresh `Foo; do `Foo } : () {`Foo: () => a |_}-> a;
***: Fatal error : The local label `Foo is not bound

A similar problem also exists in SML with local datatype definitions, e.g.

- fn () => let datatype t = Unit in Unit end;;
val it = fn : unit -> ?.t

slindley · 2023-02-05T16:09:31Z

The new function creates a new access point. We cannot also use it for creating a fresh effect.

dhil · 2023-02-05T17:01:56Z

The new function creates a new access point. We cannot also use it for creating a fresh effect.

Of course we can. The question is whether we should.

slindley · 2023-02-06T11:02:43Z

The new function creates a new access point. We cannot also use it for creating a fresh effect.

Of course we can. The question is whether we should.

Well... it's true that we could in theory (with a bit of care to disambiguate syntax) choose to overload new as a keyword for one thing and a built-in function for another, and indeed we do just that for receive (a keyword for a blocking receive from the current mailbox versus a function for receiving a message through a session endpoint).

Here's the relevant parser code for supporting receive as a function:

/* HACK: allows us to support both mailbox receive syntax
and receive for session types. */
| RECEIVE                                                      { with_pos $loc (Var "receive") }

This is indeed a hack... and arguably bad language design. But I could imagine a more systematic way of allowing certain suitably contextually-distinguished keywords (e.g. those that must appear before an open brace character such as spawn) to be reused as function names.

frank-emrich

In general, I'm having troubles trying to understand how exactly the feature is supposed to work, even after reading the original PR and trying to understand what may have changed in this version. I would appreciate an up-to-date description.

In particular, I'm interested in understanding how the removal of local labels from types and datatype definitions is supposed to work (erase_local_labels_from_tycon and erase_local_labels_from_type in Typesugar).

Also, do we have an idea if this negatively interacts with Remy-style rows once we actually implement them?

frank-emrich · 2023-02-06T13:53:12Z

core/compilePatterns.ml

              (function
                | Types.Present t ->
                  extract t
                | _ -> assert false)
+              (* | Types.Present t -> *)


should this be here?

frank-emrich · 2023-02-06T14:02:34Z

core/ir.ml

@@ -18,9 +18,9 @@ type tyvar = Quantifier.t
 type tyarg = Types.type_arg
  [@@deriving show]

-type name_set = Utility.stringset
+type name_set = Label.Set.t


Are all of these really labels? For example, name_map is used by the XmlNode constructor, and I'm not sure if we consider the names in their to be "labels".

frank-emrich · 2023-02-06T14:07:46Z

core/label.ml

+    type t =
+        | Local of local
+        | Global of global
+        | Number of int


After some offline discussion with @dhil it seems like Number is just a special case of Global, with a more efficient internal representation. I think we should therefore rename Number to Global_number and make the latter and Global behave equivalently outside of this module. Further, of_int should be make_global_of_int instead.

I think the naming can be better here too:

type t = | Bound of ... | Textual of ... | Number of ...

frank-emrich · 2023-02-10T14:53:04Z

core/typeSugar.ml

+let bind_labels      context ls     = {context with label_env  = Label.Env.bind_labels ls context.label_env}
+(* let unbind_labels    context ls     = {context with label_env  = Label.Env.unbind_labels ls context.label_env} *)
+
+(* let extend = Types.extend_typing_environment *)


debugging code?

I am not sure. But it can be deleted.

frank-emrich · 2023-02-10T14:54:10Z

core/typeSugar.ml

+      } ;
+      Some (`Mutual (qs, tygroup))
+
+(* let erase_local_labels labels decls ctx = *)


leftover code

frank-emrich · 2023-02-10T15:00:06Z

core/typeSugar.ml

+    | _ -> dt
+  in
+  try Some (e dt)
+  with CannotErase -> None


using exceptions for control flow?

frank-emrich · 2023-02-10T16:09:31Z

core/typeSugar.ml

@@ -4898,12 +5127,27 @@ and type_binding : context -> binding -> binding * context * Usage.t =
          let () = unify pos ~handle:Gripers.bind_exp
            (pos_and_typ e, no_pos Types.unit_type) in
          Exp (erase e), empty_context, usages e
+      | FreshLabel ls ->


I don't understand what's happening here. It seems that at this point, some local labels ls are brought into scope, but then we try to remove occurences of these labels from types in context, which is the typing context before ls are brought into scope?

Is similar logic necessary for when labels are brought into scope using the fresh keyword in, say, a function definition? I assume the code here is only run for standalone fresh declarations, right?

I think there is a bug here actually. The labels are bought into to scope, but I think they should be removed when the block is exited. For this to work correctly, I think we need to track the "level" (i.e. block nesting depth) that the labels were introduced at.

Orbion-J and others added 30 commits May 13, 2022 14:55

effectalias init

b1969a3

desalias inline

49a9a61

alias = effectname and typename | init

36a488f

merge into 1 construct ok; still 2 contexts

dbb6b5b

merge type and effect aliases contexts

84ffd9b

effectname body desugared into effectname

5150615

allow better printing

Merge branch 'merge-typenames-effectnames'

ee1651e

Revert "desalias inline"

a2d8bdc

This reverts commit 49a9a61.

Revert "effectname body desugared into effectname"

419aca4

This reverts commit 5150615.

"effectname" in links-mode.el

6e8c0df

cleaning before pr

1355a93

re-cleaning

50edb64

effectname -> typename _::Kind

ce200de

Update bin/repl.ml

c0c3e5b

Co-authored-by: Daniel Hillerström <[email protected]>

Update bin/repl.ml

eace411

Co-authored-by: Daniel Hillerström <[email protected]>

Update bin/repl.ml

93b2cf1

Co-authored-by: Daniel Hillerström <[email protected]>

Update bin/repl.ml

1736097

Co-authored-by: Daniel Hillerström <[email protected]>

Update bin/repl.ml

bb0fb30

Co-authored-by: Daniel Hillerström <[email protected]>

Update core/desugarDatatypes.mli

6206a6b

Co-authored-by: Daniel Hillerström <[email protected]>

Update bin/repl.ml

9a499fc

Co-authored-by: Daniel Hillerström <[email protected]>

Update core/defaultAliases.ml

c45fbbc

Co-authored-by: Daniel Hillerström <[email protected]>

Update core/desugarDatatypes.ml

832a424

Co-authored-by: Daniel Hillerström <[email protected]>

Update core/desugarDatatypes.ml

0bd30cd

Co-authored-by: Daniel Hillerström <[email protected]>

Update core/desugarDatatypes.ml

35e50e8

Co-authored-by: Daniel Hillerström <[email protected]>

rename alias_env -> tycon_env as originally

14df529

Merge branch 'master' of github.com:Orbion-J/links

31dffbb

idem

3489b8a

fixes & add primary kind in aliases

b35a3da

new error kind mismatch

69f2920

fresh label : init

f88808d

Orbion-J and others added 17 commits June 24, 2022 17:32

alias stuff + context management

82641fc

wip

b9e25e6

Merge branch 'master' into fresh-label

571ffa2

Merge branch 'links-lang:master' into fresh-label

c76a41e

fold_left_map in ListUtils (not in Ocaml < 4.11)

38f7f3e

Merge branch 'fresh-label' of github.com:Orbion-J/links into fresh-label

58919f5

fix in test

6a5e7da

fixes rule-check ocamlformat

310ebb4

fixes rule-check ocamlformat bis

152b59a

fix tests unit labels

de09626

fix Labels in tests

667a886

fix Labels tests

61ad662

fix labels tests

589a7db

fix labels tests

3ea8ddf

fix labels tests

ab3ab86

change pollution test

5e5dae6

Merge branch 'fresh-label' of github.com:Orbion-J/links into Orbion-J…

d31a6fe

…-fresh-label

dhil mentioned this pull request Jan 31, 2023

Fresh label #1148

Closed

dhil added 5 commits January 31, 2023 19:11

Refactor

066af32

Fix unique label resolution

717eba0

Fix session exceptions regression

ec92181

Slight hack to make unique labels work properly with elaborated modules.

192c437

dhil requested a review from frank-emrich January 31, 2023 22:25

frank-emrich requested changes Feb 10, 2023

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Generative labels #1169

Generative labels #1169

dhil commented Jan 31, 2023 •

edited

Loading

dhil commented Feb 1, 2023

dhil commented Feb 2, 2023 •

edited

Loading

slindley commented Feb 5, 2023

dhil commented Feb 5, 2023

slindley commented Feb 6, 2023

frank-emrich left a comment

frank-emrich Feb 6, 2023

frank-emrich Feb 6, 2023

frank-emrich Feb 6, 2023

dhil Feb 21, 2023

frank-emrich Feb 10, 2023

dhil Feb 21, 2023

frank-emrich Feb 10, 2023

frank-emrich Feb 10, 2023

dhil Feb 21, 2023

frank-emrich Feb 10, 2023

dhil Feb 21, 2023

Generative labels #1169

Are you sure you want to change the base?

Generative labels #1169

Conversation

dhil commented Jan 31, 2023 • edited Loading

dhil commented Feb 1, 2023

dhil commented Feb 2, 2023 • edited Loading

slindley commented Feb 5, 2023

dhil commented Feb 5, 2023

slindley commented Feb 6, 2023

frank-emrich left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

dhil commented Jan 31, 2023 •

edited

Loading

dhil commented Feb 2, 2023 •

edited

Loading