[Aldor-l] [Aldor-combinat-devel] parametric types and instantiation

[Ralf Hemmecke]

Thank you, Christian, for going through that piece of code so carefully.

In particular, I must agree with the fact that

define CatA(T: PrimitiveType): Category == with;

is not as innocent a function definition as it may look. Writing that in 
another syntax (which is not Aldor) it actually means

CatA(T: PrimitiveType): Category == with { CatA(T) }

or

... == CatA(T) with;

I must admit that in

   define CatA(T: PrimitiveType): Category == with;
   define CatB(T: PrimitiveType): Category == with;

I read that the functions CatA and CatB return the same value "with" for 
every input T, but, of course, they don't.
Aldor syntax is a bit misleading here, in particular because the current 
Aldor compiler does not require the "define" keyword.

My example was not really appropriate.

Ralf

>> I think, I cannot confirm that Dom(1) does not carry information about
>> Dom and 1.
> 
> Mapxe, my previous paragraph wasn't as clear as it should be.
> The result of Dom( A ) should not know that it is the result of applying 
> A to Dom.
> Let me explain what I mean with the help of the example you provided:
> 
>> ---BEGIN aaa.as
>> #include "aldor"
>> #include "aldorio"
>>
>> define CatA(T: PrimitiveType): Category == with;
>> define CatB(T: PrimitiveType): Category == with;
>> DomA(T: PrimitiveType): CatA(T) == add;
>> DomB(T: PrimitiveType): CatB(T) == add;
>> stdout << (DomA(Integer) has CatA(Integer)) << newline;
>> stdout << (DomA(Integer) has CatA(String)) << newline;
>> stdout << (DomA(Integer) has CatB(Integer)) << newline;
>> stdout << (DomA(Integer) has with) << newline;
>> ---END aaa.as
> 
> As your example also uses functions mapping to categories, let me start 
> with these Categories, as they further complicate things.
> 
> What is CatA( Integer )?
> CatA( Integer ) is the application of Integer to the function CatA.
> The result is a new, empty category.
> 
> What is CatA( String )?
> CatA( String ) is the application of String to the function CatA.
> The result is another, new, empty category.
> 
> These two categories are not equal. First of all, they live at different 
> places in memory. They have different exports.
> The result of CatA( Integer ) exports itself.
> The result of CatA( String ) exports itself.
> Both of CatA( Integer ) and CatA( String ) occur in type context. 
> Therefore, CatA should return the same category each type it is 
> evaluated at Integer. Therefore, CatA should return the same category 
> each type it is evaluated at String.
> 
> The self exports do not couple the categories with being the result of a 
> function evaluation.
> 
> Now on to DomA( Integer ).
> DomA( Integer ) is again a function call. Integer is applied to DomA.
> When calling this function its type creating function (CatA) is 
> evaluated at the actual parameter value of T (i.e.: Integer ). Hence, 
> the type of the result of evaluating DomA at Integer is CatA( Integer ).
> As CatA( Integer ) appears in type context, it holds the unique value as 
> described above.
> The value of the result of the application of Integer to DomA is just 
> some new, empty domain.
> 
> Note, that through the evaluation of DomA at Integer, the returned 
> parameter is/should be equivalent to
> 
> SomeName: Cat( Integer ) == add;
> 
> where Cat( Integer ) could be replaced by some constant as well. The 
> important part of decoupling is, that the result of the application of 
> Integer to DomA has no notion of being the result of the application of 
> Integer to DomA.
> Of course, Integer appears within its definition. But the semantic of 
> this Integer is now really, plainly Integer and no longer some actual 
> parameter value within some function call.
> 
>> Actually I don't know for domains, but for categories how
>> would the following be possible then?
> 
> I'll discuss the results step by step. Let me first note, that DomA( 
> Integer ) gives the same value again and again. It appears natural to me 
> that it should be in type context due to the “has” constructs, but 
> according to the AUG, “has" does not form a type context -- at least it 
> is not mentioned.
> I furthermore assume, that “the type context because of ‘has’” has been 
> forgotten in the AUG and consider DomA( Integer ) in type context.
> 
>>  >aldor -grun -laldor aaa.as
> 
>> T
> due to
>> stdout << (DomA(Integer) has CatA(Integer)) << newline;
> 
> The type of the result of DomA(Integer) contains the only evaluation of 
> CatA(Integer). Of course, this yields true. But at this point now, 
> DomA(Integer) refers to the result of the application, hence to the 
> construct SomeName above, which is decoupled from DomA and its parameter 
> Integer. Same holds for CatA( Integer ).
> 
>> F
> due to
>> stdout << (DomA(Integer) has CatA(String)) << newline;
> 
> CatA( String ) yields a different category as CatA( Integer ) does -- as 
> explained above. DomA( Integer ) only exports CatA( Integer ) and not 
> CatA( String ). Hence, false.
> 
>> F
> due to
>> stdout << (DomA(Integer) has CatB(Integer)) << newline;
> 
> CatB( Integer ) gives a third category, exporting no function, but only 
> itself. DomA( Integer ) again does not export this third category, hence 
> false.
> 
>> T
> due to
>> stdout << (DomA(Integer) has with) << newline;
> 
> Here you introduce another category. An anonymous one. Anonymous 
> categories do not export themselves as far as I can tell. Therefore, 
> “with” is a completely empty category, which is exported by every 
> domain. Therefore, true.
> 
> 
>> If CatA and DomA where really functions then the second line should give
>> true since neither the DomA nor CatA actually depend on their parameter.
> 
> Hopefully, my explanations made clear, what I meant by the decoupling.
> 
> Kind regards,
> Christian