[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