[Aldor-l] [Aldor-combinat-devel] Set

[Christian Aistleitner]

Hello,

>>>  From my feeling, an “any instance of” should be perfectly possible  
>>> with the
>>> current Aldor language. Currently, you can model
>>>
>>>    ( l: any instance of ListType T )
>>>
>>> by
>>>
>>>    ( LT: ListType T, l: LT )
>>>
>>> . “any instance of” would just allow you to eliminate the first  
>>> parameter.
>>> It would make code more compact and more readable without losing its
>>> expressivness.  (Of course we would also need an operator allowing to  
>>> obtain
>>> the current value of “any instance of ListType T”.)
>>
>> Yes, I agree. I very often run into situations like that, and since  
>> Axiom
>> doesn't support dependend types, it is even more difficult to come up  
>> with
>> something proper...
>
> It seems, that you like to write
>
> MyPkg(LT: ListType): with {foo: LT -> Integer} == add {
>      foo(l: LT): Integer == ...
> }
>
> Is that so bad?

It would not work, would it? ListType is a function from Type to a  
Category. You'd need something like
MyPkg(LT: ( T: Type ) -> ( ListType T )):
with {
...
}
. But anyway, let's assume ListType does not have a parameter.


I do not know Martin's intention, but your example is not applicable in  
settings I want to use it in.

Consider
   coefficient: (%, List V, List Z) -> %;
 from PolynomialRing.

Modelling via
   PolynomialRing( LT: ListType ): Category == with {
     coefficient: (%, LT V, LT Z) -> %;
   }
binds connects V's LT and Z's LT, which is undesired. Furthermore, it  
suffers the same problem as
   PolynomialRing( LTA: ListType, LTB: ListType ): Category == with {
     coefficient: (%, LTA V, LTB Z) -> %;
   }
, which is: PolynomialRing( A, B ) is a different category than  
PolynomialRing( C, D ). You cannot add them or do any other usefull thing,  
although they only differ in their ListType.

Therefore, the ListTypes have to go into the signature of coefficient and  
not the containing Category:
   PolynomialRing: Category == with {
     coefficient: (%, LTA: ListType, LTA V, LTB: ListType, LTB Z) -> %;
   }
. This does not improve readability—and things get worse, when dropping  
the assumption of ListType not taking parameters.

However, let's drop the assumption and consider the signature with a „any  
instance of” keyword
   PolynomialRing: Category == with {
     coefficient: (%, any instance of ListType V, any instance of ListType  
Z) -> %;
   }
. This piece of code looks nice and cosy to me and it already respects  
ListType's parameter.

--
Kind regards,
Christian