Re: [boost] Terminology:Type Unification? (was Re: RFC Generic data structure traversal / manipulation library

From: Larry Evans (cppljevans_at_[hidden])
Date: 2008-01-16 07:44:11

On 01/16/2008 01:39 AM, dan marsden wrote:
> Larry Evans wrote:
>> Page:
>>
>> http://spirit.sourceforge.net/dl_docs/traversal/html/traversal/quick_start_guide.html
>>
>> contains a section titled:
>>
>> Type Unification
>>
>> however, it appears like what it describes is more like the stl's
>> accumulate or mpl's fold.  Could you explain the reason for the
>> title and why a title using accumulate or fold wouldn't be
>> more intuitive to readers?
> 
> The terminology is taken from the paper by Ren and Erwig, in the references
> section. I've borrowed a lot of the naming conventions and terminology from
> this paper. 

Thanks.  Where could I find an online copy of this paper?

> In the original there are 2 traversal types, type preserving
> which return a result of the same type as their input argument, and type
> unifying, which take all input types to the same (fixed) output type. 

Ah!  OK, now the name makes more sense to me.  The reason I was
originally surprised by the name is that I've seen 'unification'
used for something that, IIRC, is somewhat different.  It's
used in prolog, IIRC, to figure which horn clause to next use.
It does that by finding 'substitutions' for the variables in
the head of a given clause that make the head match some given
element of the rhs of another clause.

...Looking.  Found reference for the term in compilers:

  > 
http://www.cs.brown.edu/~sk/Publications/Books/ProgLangs/2007-04-26/plai-2007-04-26.pdf

where, on page 280 it says something about substitution associating an
identifier with a term to solve a set of constraints.

> In my
> library, I've currently replaced the type preserving traversals with
> inplace traversals, as C++ suits modification in place better than large
> amounts of copying.
> 
> The 2 numbered points at the start of the Type Unification section attempt
> to explain this, but obviously this could be clearer. I'll have a look at
> rewording things.
> 
> The operation is certainly not a fold, so I think it would be misleading
> to associate the example with fold like terminology.

Agreed.  A fold operates with a binary op on a sequence of values where
the result type of op is same type as operands.  The reason I was
thinking fold might be applicable is that the example just chose
the leaves in the tree of a certain type and added them.  Well, add
is certainly a valid fold op; so, the difference was some filtering
(to the given type) and then flattening the tree to conform to the
structure needed by fold.  However, now I can see how a different
name than fold is needed.

-regards,
Larry