Rather than solve the general problem of evaluation of type
constructors qua functions, I think the particular problem in this
thread can be better addressed by a relatively simple extension of the
mechanism labelled '%' that allows self reference to "this domain".
A few years ago I had a discussion with Gaby about this in relation to
a possible extension to OpenAxiom. He referred to this as a special
case of the general notion of "co-induction" on types. What I wanted
was a way to refer to just the constructor name, e.g. in this case
just 'AMaybe' rather than the "full type" 'AMaybe(S)'. If I write the
symbol '%' in a constructor it denotes this full type rather than the
former. If we had available another special symbol, say for example
'%%', which only referred to the constructor name then we would have
for 'AMaybe" that
%%(S) = %
If I had a symbol like '%%' then I could write the following simpler code:
)abbrev category APPL Applicative
Applicative(S : Type) : Category == Type with
pure: S -> %
ap: (%%(S->S),%) -> %
and use it more naturally in the definition of 'AMaybe' like this:
)abbrev domain AMAYBE AMaybe
AMaybe(S : Type) : Public == Private where
Public == Join(RetractableTo S, Functor S, Applicative(S)) with
just : S -> %
++ \spad{just x} injects the value `x' into %.
fromJust : % -> S
nothing? : % -> Boolean
nothing : () -> %
++ \spad{nothing} represents failure or absence of value.
if S has CoercibleTo OutputForm then CoercibleTo OutputForm
Private == add
...
Presumably the implementation of such a special symbol would also
eliminate the need for some sort of bootstrap process to compile the
code.
On 31 October 2016 at 12:53, Waldek Hebisch <[email protected]> wrote:
> ...
>> > 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.
--
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.
