[Ur] Question about the Sum metaprogramming example

[Adam Chlipala]

David Snider wrote:
> "Ur's support for analysis of types is based around extensible records, or
> row types. In the definition of the sum function, we see the type parameter
> fs assigned the kind {Unit}, which stands for records of types of kind
> Unit. The Unit kind has only one inhabitant, (). The kind Type is for
> "normal" types."
>
> Could you elaborate on why you used the kind Unit instead of Type?
>    

If this example used [Type] instead of [Unit], then the constructor 
parameter [fs] would need to assign a type to each record field.  This 
goes against the point of the example, as we want to _force_ every type 
to be [int]; if we gave the caller more freedom, some field might be 
assigned a different type.  This looser version would yield the same 
functionality, but it would be harder to use with type inference.  The 
[Unit] version has the advantage that [Unit] has only one inhabiting 
constructor, so type inference doesn't need to guess a value for each 
field.  It would be silly to guess a field value from a set of size 
greater than one, when we are just going to overwrite these choices with 
a [map].