[Ur] the Unit kind

[Adam Chlipala]

Gergely Buday wrote:
> I'm wondering about the role of the Unit kind. Is that there to have the
>
> kind x Unit = kind
>
> equality, so to have a neutral element in the structure of kinds?
>    

No, that equality does not hold in Ur.  There are no kind equalities 
beyond simple syntactic equality.

The purpose of [Unit] at the kind level is the same as the purpose of 
[unit] at the type level: sometimes you just don't want to include any 
information!  For instance:

> And, while it is clear that {Type} is a type-level record, it is not
> clear what purpose does
>
> {Unit} and {{Unit}}
>
> have.
>    

[{Unit}] is the kind of sets of field names.  That is, a record (e.g., 
finite map) whose co-domain is a singleton set is isomorphic to a finite 
set.  The [Unit] kind is a simpler feature to add than a separate 
treatment of finite sets, and yet it makes finite sets derivable from 
records.

"Finite set of names" is a very useful abstraction to have.  For 
instance, to write a function polymorphic in all record types that map 
all fields to [string], one writes something like:
     val f : names ::: {Unit} -> $(mapU string names) -> ...