Numbers as type parameters

[Kurt Pagani]

Problem: when using a type A(p:Polynomial Integer) in another type B, then Fricas complains if p is a number (Expression makes no difference). Is there any method to tell the compiler that the number (if) is a "Polynomial Integer"? I tried out as much as crossed my mind. Any clues highly appreciated?

Below is a minimal code sample:

[1] b:=b::B

   (1)  b
                                                                      Type: B
[2] f b
 
   >> System error:
   The value
  0
is not of type
  CONS

[3] g b

   (3)  OK
                                                            

 Type: A(r)
[4] h b
 
   >> System error:
   The value
  |pretend|
is not of type
  FIXNUM

----

)abbrev domain ADOM A
A(p:Polynomial Integer) : Exports == Implementation where
  --p : Polynomial Integer
  BOP ==> BasicOperator
  Exports == SetCategory with
    coerce : Symbol -> %  
  Implementation == BOP add
    Rep := BOP  
    coerce(s:Symbol):% == operator s

)abbrev domain BDOM B
B : Exports == Implementation where
  BOP  ==> BasicOperator
  PINT ==> Polynomial Integer
  Exports == SetCategory with
    coerce : Symbol -> %
    f : % -> A(0)
    g : % -> A(r)
    h : % -> A(2 pretend PINT)
  Implementation == BOP add
    Rep := BOP  
    coerce(s:Symbol):% == operator s
    NULL:A(0):="NULL"::Symbol::A(0)
    TWO:A(2 pretend PINT):="TWO"::Symbol::A(2 pretend PINT)
    r:Polynomial Integer
    OK:A(r):="OK"::Symbol::A(r)
    f x == NULL
    g x == OK
    h x == TWO

---

Background:   

http://fricas-wiki.math.uni.wroc.pl/DependentTypeTest1

[Waldek Hebisch]

On Thu, Sep 01, 2022 at 09:11:33AM -0700, Kurt Pagani wrote:
> Problem: when using a type A(p:Polynomial Integer) in another type B, then
> Fricas complains if p is a number (Expression makes no difference). Is
> there any method to tell the compiler that the number (if) is a "Polynomial
> Integer"? I tried out as much as crossed my mind. Any clues highly
> appreciated?

<snip>

> )abbrev domain BDOM B
> B : Exports == Implementation where
> BOP ==> BasicOperator
> PINT ==> Polynomial Integer
> Exports == SetCategory with
> coerce : Symbol -> %
> f : % -> A(0)
> g : % -> A(r)
> h : % -> A(2 pretend PINT)

ATM I see no chance to make this working. Let me recall what I wrote
im March 2021:

: However, as long as use is strictly at
: Spad level, types are not used in conditions and
: parameters are first assigned to variables and
: only variables are passed to constructors, then arbitrary
: non-type parameters probably should work (I know of no obstacle
: to such use).

You violated one of rules above, namely you are passing nontrivial
constants directly to constructor.

BTW: '2 pretend PINT' is really bad code. It works only when
'2@PINT' works and otherwise silently produces wrong result.

--
Waldek Hebisch

[Kurt Pagani]

On 01.09.2022 19:11, Waldek Hebisch wrote:
> On Thu, Sep 01, 2022 at 09:11:33AM -0700, Kurt Pagani wrote:
>> Problem: when using a type A(p:Polynomial Integer) in another type B, then

...

>
> ATM I see no chance to make this working. Let me recall what I wrote
> im March 2021:
>
> : However, as long as use is strictly at
> : Spad level, types are not used in conditions and
> : parameters are first assigned to variables and
> : only variables are passed to constructors, then arbitrary
> : non-type parameters probably should work (I know of no obstacle
> : to such use).

I had this vaguely in the back of my head, but did not find the page.
Now I can remember that only variables may be passed ... that's why the function
"g" is working.

>
> You violated one of rules above, namely you are passing nontrivial
> constants directly to constructor.

Yes, indeed :(

>
> BTW: '2 pretend PINT' is really bad code. It works only when
> '2@PINT' works and otherwise silently produces wrong result.

I only wanted to build an A(0) type and was surprised by the
"The value 0 is not of type CONS", so I tried other things (numbers),
which I don't need, actually.

Perhaps I'll find a work-around (quite confident).

Thank you for the quick answer!
Kurt


>

[Waldek Hebisch]

On Thu, Sep 01, 2022 at 07:32:00PM +0200, Kurt Pagani wrote:
> On 01.09.2022 19:11, Waldek Hebisch wrote:
> > On Thu, Sep 01, 2022 at 09:11:33AM -0700, Kurt Pagani wrote:
> >> Problem: when using a type A(p:Polynomial Integer) in another type B, then
> ...
> >
> > ATM I see no chance to make this working. Let me recall what I wrote
> > im March 2021:
> >
> > : However, as long as use is strictly at
> > : Spad level, types are not used in conditions and
> > : parameters are first assigned to variables and
> > : only variables are passed to constructors, then arbitrary
> > : non-type parameters probably should work (I know of no obstacle
> > : to such use).
>
> I had this vaguely in the back of my head, but did not find the page.
> Now I can remember that only variables may be passed ... that's why the function
> "g" is working.

I would say "no error is detected", it does not mean int works...

> > You violated one of rules above, namely you are passing nontrivial
> > constants directly to constructor.
>
> Yes, indeed :(
>
> >
> > BTW: '2 pretend PINT' is really bad code. It works only when
> > '2@PINT' works and otherwise silently produces wrong result.
>
> I only wanted to build an A(0) type and was surprised by the
> "The value 0 is not of type CONS", so I tried other things (numbers),
> which I don't need, actually.

If you look at BDOM.NRLIB/index.KAF you will see:

(CATEGORY |domain| (SIGNATURE |coerce| ($ (|Symbol|)))
(SIGNATURE |f| ((A 0) $)) (SIGNATURE |g| ((A |r|) $))
(SIGNATURE |h| ((A (|pretend| 2 (|Polynomial| (|Integer|))))

And this shous explain source of the problem: constants in signatures
are represented by Lisp expressions directly taken from source.
Later. the expressions are passed (maybe quoted) to Lisp eval.

So 0 produces Lisp integer 0. But as you can see:

(3) -> PRETTYPRINT(0::Polynomial(Integer))$Lisp
(0 . 0)

0 in Polynomial(Integer) is represented by a pair, with first
element indicating Union branch, in this case base ring R (that
is Integer), the second element is value in R, this time
Lisp integer 0.

This is not easy to fix, because at each place in code we need
to know intended meaning. Namely, one meaning is syntactic,
the other is actual value in the domain. ATM we have no way
to represent general domain values in signatures. Stephen
Watt sayed that during type checking Aldor compares parse
tree of actual argument with parse tree of formal argument.
More or less the same holds for Spad compiler. But at runtime
we need values from the parameter domain. So, compiler
and intepreted should insert code computing values.
Unfortunetly this is missing and requires finding all places
where we need to do this. Additionally, interpreter represents
things differently than Spad compiler, so we need extra
work in interpreter.

--
Waldek Hebisch

[Kurt Pagani]

Thanks for this elaborate explanation - a real eye-opener and hint for a (pseudo) work-around :)

When we change Impl B to (using _0,_2,...):

  Implementation == BOP add
    Rep := BOP  
    coerce(s:Symbol):% == operator s

    _0:PINT
    _2:PINT
    r:Polynomial Integer
    NULL:A(_0):="NULL"::Symbol::A(_0)
    TWO:A(_2):="TWO"::Symbol::A(_2)

    OK:A(r):="OK"::Symbol::A(r)
    f x == NULL
    g x == OK
    h x == TWO

then it works, suggesting that I should use a type Symbolic(X) which is able to handle primitive integer arithmetics, but avoids constants/numbers? Let's see. 

   B is now explicitly exposed in frame initial
   B will be automatically loaded when needed from
      /Users/kfp/Desktop/work/spad/BDOM.NRLIB/BDOM

[5] b:=b::B

   (5)  b
                                                                      Type: B
[6] f b

   (6)  NULL
                                                                   Type: A(0)
[7]  g b

   (7)  OK
                                                                   Type: A(r)
[8]  h b

   (8)  TWO
                                                                   Type: A(2)
[9]