[Ur] the Unit kind

[Adam Chlipala]

Gergely Buday wrote:
>> [{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) ->  ...
>>      
> Then why is there the kind Name, so why not {Name} is used for having
> a set of field names?
>    

A record of kind [{K}] is a finite map from names to constructors of 
kind [K], so names are already built in.  A record of kind [{Name}] 
would be a finite map from names to names, which I haven't found any use 
for so far.  You can imagine it being useful for some sort of "record 
renaming," but I don't think the Ur type system would be up to the 
challenge of reasoning about such things.