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'.
> But it seems that interpreter has rather poor support for this usage. E.g.
>
> (3) -> AMaybe(INT) has Applicative(INT,AMaybe)
>
> Although AMaybe is the name of a constructor, a full type must be
> specified in the context you have used it. Issue )show AMaybe for
> more information.
--
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 fricas-devel+unsubscr...@googlegroups.com.
To post to this group, send email to fricas-devel@googlegroups.com.
Visit this group at https://groups.google.com/group/fricas-devel.
For more options, visit https://groups.google.com/d/optout.
