[Ur] the Unit kind

Gergely Buday gbuday at gmail.com
Thu Aug 18 06:58:59 EDT 2011


> [{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?

- Gergely



More information about the Ur mailing list