Bill Page wrote:
>
> On 30 October 2016 at 19:40, Waldek Hebisch <[email protected]> wrote:
> >
> > Before using a function Spad runtime first has to compute
> > types appearing in function signature. So before call to 'ap'
> > we have to compute 'A(S->S)' with 'A' replaced by 'AMaybe'.
> > The problem is that constructors (in particular 'AMaybe')
> > use different calling convention than normal functions.
>
> Notice that 'A(S->S)' only appears in the signature of 'ap'. As far as
> I understand it functions in signatures are never "called". In terms
> of computation all that happens is that parameters such as 'A' and
> 'S'; are substituted for values.
Actually, FriCAS assumes that it can evaluate types when
needed. Types in signatures are no exception to this. Of
course eager evaluation of types would lead to infinite
loop (recursion) already during typechecking. Most of
typechecking can just use syntatic form of definition
(with substitutions if needed). Even if needed
evaluation of types may be postponed (it works in lazy
way). But in general eventually we may need to evaluate
types in signatures. To put it differently: once you
define type later code could force its evaluation.
So type can be considered "type correct" only if it can
be safely evaluated.
Let me add that current implementation uses evaluation in
some places where just syntactic substitution in definitions
would do. OTOH current implementation skips some checks
in types which means it can skip some evaluations/substitutions
which would be neccessary otherwise.
> > More precisely, normal functions have an extra hidden
> > argument which normally is the domain implementing the
> > function. Constructors have no such extra argument.
> > You may think that extra argument can be safely ignored,
> > but unfortunately Lisp will signal mismatch if number
> > of declared arguments does not agree with number of
> > actual arguments.
>
> But Lisp evaluation is never called on 'A(S->S)'.
Types are evaluated by using Lisp 'eval'.
>
> > Inside Applicative symbol 'A' has
> > type 'Type->Type' so is considered to be an ordinary
> > function so call will add the hidden argument.
> >
>
> it is not used in a context where it must be evaluated.
>
> In fact the apparent function call is only "decoration" in any case.
> The following variant of the code gives exactly the same result:
>
> )abbrev category APPL Applicative
> Applicative(S : Type, A: Type) : Category == Type with
> pure: S -> A(S)
> ap: (A(S->S),A(S)) -> A(S)
As I wrote: Spad compiler does not check if arguments of constructors
are of correct type...
> > To be clear: we _should_ use the same calling convention
> > for functions and constructors. But the above is how
> > current runtime/compiler works and required changes are
> > rather large...
> >
>
> Perhaps the following example
>
> --
> )abbrev category APPL Applicative
> Applicative(S : Type, A: (Type->Type)) : Category == Type with
> pure: S -> A(S)
> ap: (A(S->S),A(S)) -> A(S)
> ff: () -> Integer
> add
> ff() == 0$Integer
> --
>
> manifests a problem similar to that to which you refer. This compiles
> and works exactly as I indicated before but if I try to call the dummy
> exported function 'ff' I get the following unexpected message:
>
> (1) -> ff()$AMaybe(Integer)
> Internal Error
> Unexpected error in call to system function evalSlotDomain
>
> So it seems that adding a default implementation to even an unrelated
> function can create a problem.
I did not check details of this example. But basic thing is clear:
lazy evaluation of types meant that in your earlier tests there was
no need to evaluate offending type. Calling function forced
evaluation of some types leading to crash.
--
Waldek Hebisch
--
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 [email protected].
To post to this group, send email to [email protected].
Visit this group at https://groups.google.com/group/fricas-devel.
For more options, visit https://groups.google.com/d/optout.
