On 02/14/2014 02:46 PM, Waldek Hebisch wrote: >> >> Does someone know why 'elt' in MyFun doesn't work as expected? >> > > Your 'elt' essentially is: > > elt(x: %, s: S): S == (x pretend S -> S)(s)
Yes. > This is not going to work: pretend tries to compile x to get > result mode 'S -> S'. Then, I guess, 'pretend' works different in SPAD and Aldor and my description of 'pretend' on http://axiom-wiki.newsynthesis.org/ProgrammingSPAD is not fully accurate and rather describes the situation for Aldor than for SPAD. ======== - The use of 'pretend' in 't pretend X' is very dangerous. It tells the compiler to consider 't' as an element of type 'X' even though it might be of a type 'T' with a completely different memory layout. In other words <code>"abc" pretend Integer</code> would interpret the storage of '"abc"' as an element of type 'Integer'. Careless use of 'pretend' usually leads to a program crash and should thus better be avoided. Since '%' and 'Rep' are supposed to have the same memory layout, 'pretend' is safe in:: rep x ==> (x@%) pretend Rep Nevertheless is 'pretend' a way to make the safety that SPAD brings with its type system void if it is not used with great care. In fact, 'pretend' should be used only in these rare situations where the compiler is unable to figure out the right type itself. ========= Up to now, I would have thought that in "e pretend T" the compiler throws away any type analysis of the expression e and just sets it to be T (with all the possible nasty consequences). > This uses 'compWithMappingMode' which > provides a dummy argument and tries to compile 'x' applied > to the dummy, in other words we try to compile something like: > > x(%A) > > That triggers 'elt' magic. Something goes wrong and we get > a nonsense. But if things worked correctly we would get > a closure containing recursive call to 'elt'. You've just explained that the compiler is actually doing something else. Do you have an idea why this is currently done the way it is? > AFAICS the following works as intended: > > coerce(x: %): S -> S == x pretend None pretend Rep > elt(x: %, s: S): S == (x pretend None pretend Rep)(s) > > Main point here is that None does not have 'elt' so 'pretend' > from 'None' works without any magic. Cool. Thank you for the fix. > BTW: For this domain you probably should define 'rep' as: > > rep(x) ==> x pretend None pretend Rep > > because _any_ use of your version of 'rep' will lead to > call to 'elt'. Thank you for this suggestion. However, this is bad. It somehow defeats the purpose of that webpage. I cannot put tricks on the very first introduction. Interestingly, (minc pretend (I->I))(1) worked in the interpreter, even with a defined elt(x: %, s: S): S == (rep x) s so things must work differently in the interpreter. Would it make sense to *always* use rep x ==> (x@%) pretend None pretend Rep ? Would that break anything if we are not dealing with something like S->S? In fact, I currently fail to see why the case S -> S is obviously treated in a special way. In which situation is that actually useful? Although I don't think that rep/per must be built into the language, I don't really like the idea of defining them in every file. And now with the special case for the Mapping constructor, it somewhat calls for a mechanism for rep/per. Ralf -- 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 http://groups.google.com/group/fricas-devel. For more options, visit https://groups.google.com/groups/opt_out.
