[Ur] Question about the Sum metaprogramming example

[David Snider]

OK, Thanks. There are some other things I don't understand:

"With sum defined, it is easy to make some sample calls. The form of the
code for main does not make it apparent, but the compiler must "reverse
engineer" the appropriate {Unit} from the {Type} available from the context
at each call to sum. The compiler also infers a folder for each call,
guessing at the desired permutations by examining the orders in which field
names are written in the code."

I understand type inference, but how does it infer the actual values of the
parameters? How do I know which parameters need to be passed and which will
be inferred?

For example, the sum function takes 3 paramters, but you only seem to be
passing one in..

On Tue, 08 Dec 2009 14:17:47 -0500, Adam Chlipala <adamc at impredicative.com>
wrote:
> 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].
> 
> _______________________________________________
> Ur mailing list
> Ur at impredicative.com
> http://www.impredicative.com/cgi-bin/mailman/listinfo/ur