Proposal(ux): make sorts maximally limited by default

[srghma]

In https://digama0.github.io/mm0/thesis.pdf You write "Sorts have modifiers that limit what roles they can play". This is not really true. provable relaxes the default sort IIUC.

Therefore

Actual:

the provable sort is maximally permissive:

1. can use in axioms and theorems
2. can be used as a dummy variable
3. can be used as a name
4. can be created by terms or defs constructors

sort without modifiers is on second level of permissivness:

1. cannot use in axioms and theorems
2. can be used as a dummy variable
3. can be used as a name
4. can be created by terms or defs constructors

all other modifiers limit usage more:

• free changes 2. can be used as a dummy variable to from can to cannot
• strict changes 3. can be used as a name to from can to cannot
• pure changes 4. can be created by terms or defs constructors to from can to cannot

This results in poor UX. E.g. in here #146 (comment) I had to add modifiers to limit code more (thus gain more knowledge about code)

Expected:

lets make sort without modifiers maximally limited:

1. cannot use in axioms and theorems
2. cannot be used as a dummy variable
3. cannot be used as a name
4. cannot be created by terms or defs constructors

and then have modifiers

• provable changes 1. cannot use in axioms and theorems to from cannot to can

• unfree changes 2. cannot be used as a dummy variable to from cannot to can

  • or inhabited (Highly recommended): This is the standard type-theoretic term for a sort/type that is guaranteed to have at least one term.
  • or nonempty: Simple, direct, and universally understood in mathematics.
  • or allow_in_dummy

• unstrict changes 3. cannot be used as a name/in binders/in {...} to from cannot to can

  • or bindable (Highly recommended): Very clear from a UX perspective. It tells the programmer: "You can bind this sort in {}."
  • or nominal: From nominal logic; denotes that the sort represents abstract names/variables.
  • or variable: Direct and intuitive.

• impure changes 4. cannot be created by terms or defs constructors to from cannot to can

  • or constructible (Highly recommended): Explicitly states that you can use term or def constructors to build elements of this sort.
  • or structured: Contrasts beautifully with "pure/unstructured" variable sorts.
  • or algebraic: Since term constructors define an algebra over the sort.