[Ur] folder

[Adam Chlipala]

Gergely Buday wrote:
> why is it necessary to include the [folder] type in the type of higher
> order record functions when it is always inferred?
>
> Isn't it enough to see them as something happening behind the scene?
>    

The [folder] functionality is a convenience added on top of the core Ur 
language, which has no support for iteration over records.  A key 
feature of the Ur type system is that a record is indistinguishable from 
any permutation of its fields; in other words, records are inherently 
unordered.  Building in iteration would break this principle, so 
operations that need iteration must be parametrized over [folder] values 
that represent orderings.  Inference of [folder]s for concrete records 
is done in an ad-hoc way, but the core language stays elegant.