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.
_______________________________________________ Ur mailing list [email protected] http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
