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