Ralf Hemmecke wrote:
>
> 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.
>
<snip>
> 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).
_Before_ compiling 'e pretend T' Spad compiler has to compile 'e'.
'pretend' affects compilation of 'e', because due to 'pretend'
Spad prefers 'T' as the result type. I think that general
rule is the same for Spad and Aldor. And probably you use
'(x@%) pretend T' to avoid consequences of this rule in Aldor.
I do not know if Aldor has user definable 'elt', if it has, then
details of its handling may differ. Or maybe Aldor 'pretend'
skips some steps of compilation of 'e'.
> > 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?
If you define 'elt' you presumably want it to be used, so element of
your domin behave like functions. Nice side effect of Spad way is
that anything callable should be usable in place of a function.
I write 'should' because it currently gets miscompiled. Otherwise
you would have to explicitely coerce your callable to a function.
> > 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.
Well, I think you start from too complicated things. I would rather
give a few small examples in style of Rosetta Code.
If you want an example which uses only 'basic' things the
following may do:
-------------------
)abbrev domain MYPAIR MyPair
MyPair(T : Type) : with
my_pair : (T, T) -> %
first : % -> T
second : % -> T
== add
my_pair(x, y) ==
(((f : (T, T) -> T)) : T +-> f(x, y)) pretend %
first_aux(x : T, y : T) : T == x
first(p) == (p pretend ((T, T) -> T) -> T)(first_aux)
second_aux(x : T, y : T) : T == y
second(p) == (p pretend ((T, T) -> T) -> T)(second_aux)
-------------
>
> 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?
Look OK. But without an example I would not guess that there
is problem with current definition.
--
Waldek Hebisch
[email protected]
--
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.
