Mentions légales du service

Skip to content
Snippets Groups Projects

Add annotations to System F

Merged SCHERER Gabriel requested to merge gscherer/inferno:F-annot into master

Before this MR, the ML program (t : some a . ty) would elaborate into elab((t : some a. ty)) := elab(t). This can hide issues with the inference engine; for example our inference engine could have just completely ignored annotations, and you would never notice the difference on well-typed programs. (We mostly test using well-typed programs, especially in the random generator.)

@omartino and myself are starting to work on rigid variables, and there the question of elaborating annotations becomes even more interesting: we want an elaboration for (fun x -> x : for a. a -> a) that enforces polymorphism in the elaborated System F term -- (Fun a. fun (x:a) -> x : forall a. a -> a) [tau] for tau the instantiation witness.

In preparation for these questions, the current MR introduces annotations in System F, and elaborates ML annotations into System F annotations. We now have elab(t : some a. ty) := (elab(t): elab(ty)[tau/a]), where tau is the witness of a. (One could add type-level lets and elaborate into (elab(t) : let a = tau in elab(ty)) to respect sharing, but I did not bother.)

Merge request reports

Merge request pipeline #259253 passed

Merge request pipeline passed for a1d83bd9

Approved by

Merged by SCHERER GabrielSCHERER Gabriel 3 years ago (Jun 22, 2021 8:13am UTC)

Merge details

  • Changes merged into master with 8d89520d.
  • Did not delete the source branch.

Pipeline #262640 passed

Pipeline passed for 8d89520d on master

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
Please register or sign in to reply
Loading