Re: [Axiom-mail] Spad and inductive types
Dear Gaby, Gabriel Dos Reis [EMAIL PROTECTED] writes: For concretness, here is a very classic example of inductive type along with a function working on expression of such type, written in both Haskell and New Boot. How would you best write that in Spad? I'm very sorry, but I do not understand the code below. Could you describe what it is supposed to do? I guess: Expr is the name of the type (= domain?) you want to create, and it exports a single operation called eval, which returns an integer. But what is MkInt, MkAdd and MkMul? Perhaps you want to say that an element in Expr can be of three forms, namely MkInt, MkAdd or MkMul? Martin --8- Begin Haskell code --8- data Expr = MkInt Int | MkAdd Expr Expr | MkMul Expr Expr eval::Expr - Int eval (MkInt i) = i eval (MkAdd x y) = (eval x) + (eval y) eval (MkMul x y) = (eval x) * (eval y) --8- End Haskell code --8--- Here is the same thing written in New Boot --8- Begin Boot code --8- structure Expr == MkInt(Integer) MkAdd(Expr, Expr) MkMul(Expr, Expr) eval e == case e of MkInt(i) = i MkAdd(x, y) = eval(x) + eval(y) MkMul(x, y) = eval(x) * eval(y) otherwise = error should not happen --8- End Boot code --8--- For the curious, the above New Boot code is translated as shown below. How would you write that in Spad. Please, keep the discussion on axiom-mail. Thanks! -- Gaby ; structure Expr == ;MkInt(Integer) ;MkAdd(Expr, Expr) ;MkMul(Expr, Expr) (DEFUN |MkInt| #0=(|bfVar#1|) (CONS '|MkInt| (LIST . #0#))) (DEFUN |MkAdd| #0=(|bfVar#2| |bfVar#3|) (CONS '|MkAdd| (LIST . #0#))) (DEFUN |MkMul| #0=(|bfVar#4| |bfVar#5|) (CONS '|MkMul| (LIST . #0#))) ; eval e == ; case e of ; MkInt(i) = i ; MkAdd(x, y) = eval(x) + eval(y) ; MkMul(x, y) = eval(x) * eval(y) ; otherwise = error should not happen (DEFUN |eval| (|e|) (PROG (|bfVar#7| |bfVar#6|) (RETURN (PROGN (SETQ |bfVar#6| |e|) (SETQ |bfVar#7| (CDR |bfVar#6|)) (CASE (CAR |bfVar#6|) (|MkInt| (LET ((|i| (CAR |bfVar#7|))) |i|)) (|MkAdd| (LET ((|x| (CAR |bfVar#7|)) (|y| (CADR |bfVar#7|))) (+ (|eval| |x|) (|eval| |y| (|MkMul| (LET ((|x| (CAR |bfVar#7|)) (|y| (CADR |bfVar#7|))) (* (|eval| |x|) (|eval| |y| (T (|error| '|should not happen|))) ___ Axiom-mail mailing list Axiom-mail@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-mail ___ Axiom-mail mailing list Axiom-mail@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-mail
RE: [Axiom-mail] Spad and inductive types
On May 7, 2007 2:28 AM Martin Rubey writes: Gabriel Dos Reis writes: For concretness, here is a very classic example of inductive type along with a function working on expression of such type, written in both Haskell and New Boot. How would you best write that in Spad? I'm very sorry, but I do not understand the code below. Could you describe what it is supposed to do? I guess: Expr is the name of the type (= domain?) you want to create, and it exports a single operation called eval, which returns an integer. But what is MkInt, MkAdd and MkMul? Perhaps you want to say that an element in Expr can be of three forms, namely MkInt, MkAdd or MkMul? ... --8- Begin Haskell code --8- data Expr = MkInt Int | MkAdd Expr Expr | MkMul Expr Expr eval::Expr - Int eval (MkInt i) = i eval (MkAdd x y) = (eval x) + (eval y) eval (MkMul x y) = (eval x) * (eval y) --8- End Haskell code --8--- Yes, I think what Gaby wants might be written something like this in SPAD: )abbrev domain EX Expr Expr:with eval: % - Integer coerce: Integer - % _+: (%,%) - % _-: (%,%) - % == add MkInt == Integer MkAdd == Record(lAdd:%,rAdd:%) MkMul == Record(lMul:%,rMul:%) Rep == Union(MkInt,MkAdd,MkMul) eval(x:%) == i := x pretend Rep i case MkInt = i i case MkAdd = eval(i.lAdd) + eval(i.rAdd) i case MkMul = eval(i.lMul) * eval(i.rMul) -- coerce(n) == autoCoerce(n)$Rep pretend % -- x + y == autoCoerce([x,y]$MkAdd)$Rep pretend % -- x * y == autoCoerce([x,y]$MkMul)$Rep pretend % This compiles eval, but I have a problem. Obviously one would like to create members of this domain. But I can not seem to persuade SPAD to compile my defintions of coerce, + and *. SPAD tells me: Cannot pretend ... I don't understand that. Perhaps you can see a way around it? Regards, Bill Page. ___ Axiom-mail mailing list Axiom-mail@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] Spad and inductive types
Here you go. But I doubt somehow that Gaby had this in mind, since this is quite usual stuff in Axiom (grep Rep.*Union) Martin )abbrev domain EX Expr Expr(): with eval: % - Integer coerce: Integer - % coerce: % - OutputForm _+: (%,%) - % _*: (%,%) - % == add MkInt == Integer MkAdd == Record(lAdd:%,rAdd:%) MkMul == Record(lMul:%,rMul:%) -- Rep shouldn't be a macro, I think Rep := Union(MkInt, MkAdd, MkMul) eval(x:%): Integer == -- in SPAD, conversion from Rep to Union(MkInt, ...) is implicit x case MkInt = x -- without package calling + the compiler picks + from %... x case MkAdd = (eval(x.lAdd) + eval(x.rAdd))$Integer x case MkMul = (eval(x.lMul) * eval(x.rMul))$Integer coerce(n: Integer) == n::Rep x + y == [x,y]$MkAdd :: Rep x * y == [x,y]$MkMul :: Rep coerce(x: %): OutputForm == x case MkInt = outputForm x x case MkAdd = hconcat [message (, _ (x.lAdd)::OutputForm, _ message +, _ (x.rAdd)::OutputForm, _ message )] x case MkMul = hconcat [message (, _ (x.lMul)::OutputForm, _ message *, _ (x.rMul)::OutputForm, _ message )] ___ Axiom-mail mailing list Axiom-mail@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-mail
RE: [Axiom-mail] Spad and inductive types
Martin, On May 7, 2007 4:14 AM you wrote: Here you go. But I doubt somehow that Gaby had this in mind, since this is quite usual stuff in Axiom (grep Rep.*Union) ... Fantastic! Thankyou. See it again here: http://wiki.axiom-developer.org/SandBoxInductiveType I believe that is exactly what Gaby wanted. Yes, grep shows some examples but not of the specific type of induction that Gaby had in mind. It seems that one key differences between what I wrote and your version was: ... Rep := Union(MkInt, MkAdd, MkMul) ... The grep command actually shows one case where == is used, but I have noticed before that Spad seems to treat this differently than what I always expect but you seem to write it naturally. :-) Now I can retire to sleep in peace. Cheers, Bill Page ___ Axiom-mail mailing list Axiom-mail@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] Spad and inductive types
Martin Rubey [EMAIL PROTECTED] writes: | Dear Gaby, | | Gabriel Dos Reis [EMAIL PROTECTED] writes: | |For concretness, here is a very classic example of inductive type | along with a function working on expression of such type, written in | both Haskell and New Boot. How would you best write that in Spad? | | I'm very sorry, but I do not understand the code below. Sorry. An inductive type is a kind of union whose members are inductively defined (like the kind of combinatorial thing you're doing with Ralf). Here I took a very simplistic datatype, that of an arithemtic expression over integers: An arithmetic expression over integer is: * an integer, or * addition of two expressions over integer, or * multiplication of two expressions over integer. | Could you describe | what it is supposed to do? I guess: Expr is the name of the type (= domain?) | you want to create, and it exports a single operation called eval, which | returns an integer. But what is MkInt, MkAdd and MkMul? Perhaps you want to | say that an element in Expr can be of three forms, namely MkInt, MkAdd or | MkMul? MkInt, MkAdd and MkMull (in both Boot and Haskell) are data cnstructors. Given an integer, MkInt turn it into an Expr. Simirlarlt, MkAdd and MkMul combines two expressions into an Expr. So, they have types: MkInt :: Int - Expr MkAdd :: Expr - Expr - Expr MkMul :: Expr - Expr - Expr Furthermore, they can also serves as tags to indicate how expressions of Expr are constructed. That is useful in pattern matching. In pattern matching, the data constructor serves as tag, and the operands are variables that are bound to the operands. -- Gaby ___ Axiom-mail mailing list Axiom-mail@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] Spad and inductive types
http://wiki.axiom-developer.org/SandBoxInductiveType I've added an Aldor version. Ralf ___ Axiom-mail mailing list Axiom-mail@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-mail
RE: [Axiom-mail] Spad and inductive types
On May 7, 2007 10:41 AM Gaby wrote: Martin Rubey writes: | Here you go. But I doubt somehow that Gaby had this in | mind, since this is quite usual stuff in Axiom (grep Rep.*Union) Thanks, Martin. I did not say I did not know how to write it. I said I don't have a good way :-). Everything I've tried to come up (including proposed solutions here) with looked a hack to me. I think it would have been very useful if you had included what you came up with in your original email. :-( Anyway, I think your question is very useful as it stands as an example of the difference between Spad and Boot. Part of the reasons is -- MkAdd == Record(lAdd:%,rAdd:%) -- MkMul == Record(lMul:%,rMul:%) if union are used whose fields are directly records, then the fields of the record must themselves have different name. In the Boot or Haskell case, only the data constructor name need to be different. That is not an essential feature of how this must be written in Spad. For example see my recent additional example at: http://wiki.axiom-developer.org/SandBoxInductiveType But I think you are right to point out a limitation of the design of the 'Union' domain constructor in Spad (and in Aldor). I think there is no good reason that 'Union' is implemented in Spad using polymorphism of coerce to create elements. For example the following provides no method to create objects with a specific tag, x or y (by default only objects tagged x are created). (1) - )sh Union(x:Integer,y:Integer) Union(x: Integer,y: Integer) is a domain constructor. --- Operations ?=? : (%,%) - Boolean ?case? : (%,x) - Boolean ?case? : (%,y) - Booleancoerce : % - OutputForm construct : Integer - % construct : Integer - % ?.? : (%,x) - Integer ?.? : (%,y) - Integer In spite of this it appears that the internal representation of 'Union' does implement a proper disjunction as required by the expected semantics. I would prefer that Union have methods something like this: construct : (Integer,x) - % construct : (Integer,y) - % but this would also require some changes in the Axiom interpreter to work smoothly. I fully understand Spad is not Haskell, neither Boot, but I'm looking for a solution where only the toplevel data constructors needs to be different. I think my example 'Expr2' at http://wiki.axiom-developer.org/SandBoxInductiveType satisfies your requirement, although on initial look it probably seems more complicated than what you might like. Some of this complication is merely interface for the Axiom interpreter. The essential definition of the inductive type is merely given by: Rep := Union(MkInt(Integer), MkAdd(%,%), MkMul(%,%)) The definitions of MkAdd and MkMul as named types (domains) is sufficient to avoid the problem that this form of 'Union' is not disjunctive. I have more to say later. We're listening. :-) Regards, Bill Page. ___ Axiom-mail mailing list Axiom-mail@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-mail
