Bill Page wrote:
>
> On 28 October 2016 at 22:32, Waldek Hebisch <[email protected]> wrote:
> > Bill Page wrote:
> >>
> >> The following code compiles (requires bootStrapMode) and seems to work:
> >>
> >> --
> >> )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)
> >>
> >> )boot $bootStrapMode := true
> >> )abbrev domain AMAYBE AMaybe
> >> AMaybe(S : Type) : Public == Private where
> >> Public == Join(RetractableTo S, Functor S, Applicative(S,AMaybe)) with
> > ^^^^^^
> >
> > Hmm, this is not type correct, at least from point of view of current
> > Spad compiler. In other words 'AMaybe' is different than function
> > from Type to Type. Currently there are missing checks in the
> > compiler so this code may pass. But frankly, to type check it
> > would require subtantial addition. And actually, currently
> > representation of contructors and representation of functions
> > differ -- that is AMaybe is _not_ compatible with function
> > of type 'Type -> Type'.
> >
>
> This code does pass the current compiler and does work as expected if
> constructors are treated as "functions" from some category to another
> category. What harm does it do? Why is it important that the
> representation of constructors (from category to category) and
> functions (from domain to domain) is different. When would this
> matter?
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.
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. Inside Applicative symbol 'A' has
type 'Type->Type' so is considered to be an ordinary
function so call will add the hidden argument.
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...
--
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.
