Passing a package constructor function as argument

[Ralf Hemmecke]

Hi Waldek,

I cannot send the whole code, but I'd like to ask whether the
construction (see RED) should in principle be possible.

It basically says that instead of a package in the argument list of a
constructor, I pass a function that returns a package, because I would
like to instantiate that package either with (C,L,QXAB) or with (C,F,AB).

The compiler throws a strange error message at me that I cannot interpret.

Any hints?

Thank you in advance.

Ralf

PS: I can certainly rewrite my code if the above passing of a package
constructor isn't (yet) working. I'm just curious how good the SPAD
compiler already is.

================================================================

QEtaExtendedAlgebraBasis(L, F, AB): Exports == Implementation where
L: Type
F: with first: % -> L
AB: QEtaAlgebraBasisCategory F
Exports ==> QEtaAlgebraBasisCategory(L) with
coerce: AB -> %
Implementation ==> ...

QEtaExtendedReduction(L, F, AB, RED): Exports == Implementation where
L: Type
F: with (first: % -> L)
AB: QEtaAlgebraBasisCategory F
RED: (C:Type, LF:Type, XAB:Type) ->
QEtaComputationReductionCategory(LF, XAB)
QXAB ==> QEtaExtendedAlgebraBasis(L, F, AB)
Exports ==> with (reduce: (F, AB))
Implementation ==> add
reduce(u: F, ab: AB): F ==
ul: L := reduce(first u, ab :: QXAB)$RED(C, L, QXAB)
zero? ul => return 0$F
return reduce(u, ab) $ RED(C, F, AB)

----------------------------------------------------------------------

initializing NRLIB QETAXRED for QEtaExtendedReduction
compiling into NRLIB QETAXRED
compiling local reduce : (F,AB) -> F
****** comp fails at level 4 with expression: ******
error in function reduce

(SEQ
(|:=| (|:| |ul| L)
((|Sel| (RED C L (|QEtaExtendedAlgebraBasis| L F AB)) |reduce|) | << |
(|first| |u|) | >> | (|::| |ab| (|QEtaExtendedAlgebraBasis| L F AB))))
(|:=| (|:| #1=#:G52032 (|Boolean|)) (|zero?| |ul|))
(|exit| 1
(IF #1#
(|return| (|Sel| F 0))
(|return| ((|Sel| (RED C F AB) |reduce|) |u| |ab|)))))
****** level 4 ******
$x:= (first u)
$m:= LF
$f:=
((((|ul| #) (|ab| # #) (|u| # #) (|reduce| # #) ...)))

>> Apparent user error:
Cannot coerce ab
of mode AB
to mode (QEtaExtendedAlgebraBasis L F AB)

[Waldek Hebisch]

On Tue, May 02, 2023 at 09:42:07AM +0200, Ralf Hemmecke wrote:
> Hi Waldek,
>
> I cannot send the whole code, but I'd like to ask whether the construction
> (see RED) should in principle be possible.
>
> It basically says that instead of a package in the argument list of a
> constructor, I pass a function that returns a package, because I would like
> to instantiate that package either with (C,L,QXAB) or with (C,F,AB).
>
> The compiler throws a strange error message at me that I cannot interpret.
>
> Any hints?

The following:

RED: (C:Type, LF:Type, XAB:Type) -> QEtaComputationReductionCategory(LF, XAB)

is probably unsupported. First, giving names of arguments is not
really supported, at best they will be ignored but potentially
they may cause trouble. Second, QEtaComputationReductionCategory(LF, XAB)
depends on argument, this is unsupported.

--
Waldek Hebisch

[Ralf Hemmecke]

Dear Waldek,

> RED: (C:Type, LF:Type, XAB:Type) -> QEtaComputationReductionCategory(LF, XAB)

> is probably unsupported. First, giving names of arguments is not
> really supported, at best they will be ignored but potentially
> they may cause trouble. Second, QEtaComputationReductionCategory(LF, XAB)
> depends on argument, this is unsupported.

Thank you for your clarification.

Being not able to give names to argument ...

We have this in our library.

entries : (lp : %) -> List NNI

https://github.com/fricas/fricas/blob/master/src/algebra/graph.spad#L1033

That is of course unnecessary and I would like to remove the "lp : " in
these cases (there are several of them). But I found it too unimportant
until now.

You probably meant something else like: the SPAD compiler does not
support dependent types?

However, this

Localize(M : Module R, R : CommutativeRing) : Module R with ...


https://github.com/fricas/fricas/blob/master/src/algebra/fraction.spad#L11

is not much different. It seems that you tell me that I can create
something like Localize, but *not* use it as a first class object, i.e.
pass it as an argument to a function. And I mean "Localize", not
"Localize(M,R)", because, the compiler doesn't allow me to specify the
type of the argument as

(Module R, R : CommutativeRing) -> Module R

Well, if that is the case, it's a pity, but I can live with it for now.

Thanks again for your answer.

Ralf

[Waldek Hebisch]

On Tue, May 02, 2023 at 12:50:07PM +0200, Ralf Hemmecke wrote:
> Dear Waldek,
>
> > RED: (C:Type, LF:Type, XAB:Type) -> QEtaComputationReductionCategory(LF, XAB)
>
> > is probably unsupported. First, giving names of arguments is not
> > really supported, at best they will be ignored but potentially
> > they may cause trouble. Second, QEtaComputationReductionCategory(LF, XAB)
> > depends on argument, this is unsupported.
>
> Thank you for your clarification.
>
> Being not able to give names to argument ...
>
> We have this in our library.
>
> entries : (lp : %) -> List NNI
>
> https://github.com/fricas/fricas/blob/master/src/algebra/graph.spad#L1033
>
> That is of course unnecessary and I would like to remove the "lp : " in
> these cases (there are several of them). But I found it too unimportant
> until now.

Well, I would like to support argument names some day, so if this
works let it stay.

> You probably meant something else like: the SPAD compiler does not support
> dependent types?

As I wrote: constructor are example of dependent types, so in this
sense dependent types work. But support for dependence on something
else than constuctor parameters is quite limited and you can not
declare ordinary functions with dependencies like constructors.

> However, this
>
> Localize(M : Module R, R : CommutativeRing) : Module R with ...
>
>
> https://github.com/fricas/fricas/blob/master/src/algebra/fraction.spad#L11
>
> is not much different.

It is a constructor, internally handled quite different than functions.

> It seems that you tell me that I can create something
> like Localize, but *not* use it as a first class object, i.e. pass it as an
> argument to a function.

Yes, you can not. You can not even give correct type to 'Localize'
(it is not a function).

> And I mean "Localize", not "Localize(M,R)", because,
> the compiler doesn't allow me to specify the type of the argument as
>
> (Module R, R : CommutativeRing) -> Module R
>
> Well, if that is the case, it's a pity, but I can live with it for now.
>
> Thanks again for your answer.
>
> Ralf
>

> --
> You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to fricas-devel...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/5cb8efd3-6bb1-aca3-0b65-e14fb4863f9a%40hemmecke.de.

--
Waldek Hebisch