[TYPES] Max on terminology: "Graduality" instead of "Gradual Guarantee"

[Gabriel Scherer]

Dear types-list,

I attended this week at FSCD an excellent talk by Max New (see
abstract and link at the end of this email) where he proposed the name
"graduality" for what we usually call the "gradual guarantee", to get
a stronger correspondence with the name "parametricity": we don't say
"parametric guarantee".

I like the suggestion, and I would suggest to adopt it!

P.S.: It is interesting that graduality experts sometimes distinguish
"static graduality" from "dynamic graduality" -- there are different
things
that could be called "dynamic parametricity", and they are being
actively researched.


   Call-by-name Gradual Type Theory
   Max S. New, Daniel R. Licata, 2018
   https://arxiv.org/abs/1802.00061

This terminology is also used in a follow-up paper

  Graduality from Embedding-projection Pairs
  Max S. New, Amal Ahmed, 2018
  https://arxiv.org/abs/1807.02786