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? -- 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.
