login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit

On May 6, 2007 11:01 PM Gabriel Dos Reis wrote:

While writing a tutorial on programming with Spad, I realize that I don't have a good way to present inductive types in Spad. I know what they would like in my ideal Spad, but we don't have that ideal Spad yet. So, I'm asking here how you would write inductive types today in Spad.

For concreteness, 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?

Haskell code:

  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)

Here is the same thing written in New Boot:

  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"

On Sent: May 7, 2007 9:11 AM Gabriel Dos Reis wrote:

An inductive type is a kind of union whose members are inductively defined. Here I took a very simplistic datatype, that of an arithmetic 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.

MkInt, MkAdd and MkMul (in both Boot and Haskell) are data constructors. Given an integer, MkInt turn it into an Expr. Simirlarly, 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.

On May 7, 2007 4:14 AM Martin Rubey wrote:

spad
)abbrev domain EX Expr
Expr(): with
    eval: % -> Integer
    coerce: Integer -> %
    coerce: % -> OutputForm
    _+: (%,%) -> %
    _*: (%,%) -> %
  == add
    MkInt ==> Integer
    MkAdd ==> Record(lAdd:%,rAdd:%)
    MkMul ==> Record(lMul:%,rMul:%)
    Rep := Union(MkInt, MkAdd, MkMul)
eval(x:%): Integer == x case MkInt => x x case MkAdd => (eval(x.lAdd) + eval(x.rAdd))$Integer x case MkMul => (eval(x.lMul) * eval(x.rMul))$Integer
coerce(n: Integer) == n
x + y == [x,y]$MkAdd
x * y == [x,y]$MkMul
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 ")"]
spad
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/3998018739717071210-25px001.spad
      using old system compiler.
   EX abbreviates domain Expr 
------------------------------------------------------------------------
   initializing NRLIB EX for Expr 
   compiling into NRLIB EX 
   processing macro definition MkInt ==> Integer 
   processing macro definition MkAdd ==> Record(lAdd: $,rAdd: $) 
   processing macro definition MkMul ==> Record(lMul: $,rMul: $) 
   compiling exported eval : $ -> Integer
Time: 0 SEC.
compiling exported coerce : Integer -> $ EX;coerce;I$;2 is replaced by CONS0n Time: 0 SEC.
compiling exported + : ($,$) -> $ Time: 0 SEC.
compiling exported * : ($,$) -> $ Time: 0 SEC.
compiling exported coerce : $ -> OutputForm Time: 0 SEC.
(time taken in buildFunctor: 0)
;;; *** |Expr| REDEFINED
;;; *** |Expr| REDEFINED Time: 0.01 SEC.
Cumulative Statistics for Constructor Expr Time: 0.01 seconds
finalizing NRLIB EX Processing Expr for Browser database: --->-->Expr(constructor): Not documented!!!! --->-->Expr((eval ((Integer) %))): Not documented!!!! --->-->Expr((coerce (% (Integer)))): Not documented!!!! --->-->Expr((coerce ((OutputForm) %))): Not documented!!!! --->-->Expr((+ (% % %))): Not documented!!!! --->-->Expr((* (% % %))): Not documented!!!! --->-->Expr(): Missing Description ; compiling file "/var/aw/var/LatexWiki/EX.NRLIB/EX.lsp" (written 31 JUL 2013 05:27:44 PM):
; /var/aw/var/LatexWiki/EX.NRLIB/EX.fasl written ; compilation finished in 0:00:00.027 ------------------------------------------------------------------------ Expr is now explicitly exposed in frame initial Expr will be automatically loaded when needed from /var/aw/var/LatexWiki/EX.NRLIB/EX

fricas
n:Expr:=3

\label{eq1}3(1)
Type: Expr
fricas
m:Expr:=4

\label{eq2}4(2)
Type: Expr
fricas
p:=n+m

\label{eq3}(3 + 4)(3)
Type: Expr
fricas
eval(p)

\label{eq4}7(4)
fricas
q:=p*5

\label{eq5}({(3 + 4)}<em> 5)(5)
Type: Expr
fricas
eval(q)

\label{eq6}35(6)

Ralf Hemmecke wrote:

Here is a similar thing in Aldor. Actually it should be called BinaryExpressionTree?. Note that according to the Aldor User Guide (Type Union) one cannot use the type as the second argument of a "case" expression. So the above representation would rather look like:

    Rep == Union(
        MkInt: Integer,
        MkAdd: Record(lAdd:%, rAdd:%),
        MkMul: Record(lMul:%, rMul:%)
    );

in an Aldor equivalent. I only see a problem if there were additionally an entry like:

        MkInt2: Integer

whose type is identical to some other type of the union, because then the function "union(i)" where i is an integer would not know whether it belongs to MkInt? or MkInt2?.

aldor
#include "axiom"
macro Z == Integer; BinExpr: with { eval: % -> Integer; coerce: Integer -> %; +: (%,%) -> %; *: (%,%) -> %; coerce: % -> OutputForm; } == add { Rep == Union( z: Z, tuple: Record(print: String, op: (Z, Z) -> Z, left: %, right: %); ); import from Rep; coerce(i: Integer): % == per union i; (x: %) + (y: %): % == per union ["+", +, x, y]; (x: %) * (y: %): % == per union ["*", *, x, y]; eval(x: %): Integer == { rep x case z => rep(x).z; (s, f, a, b) := explode(rep(x).tuple); f(eval a, eval b); } coerce(x: %): OutputForm == { import from List OutputForm; rep x case z => coerce(rep(x).z); (s, f, a, b) := explode(rep(x).tuple); hconcat [ message "(", a :: OutputForm, message s, b :: OutputForm, message ")" ]; } }
aldor
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/9147585987609704779-25px003.as
      using AXIOM-XL compiler and options 
-O -Fasy -Fao -Flsp -laxiom -Mno-ALDOR_W_WillObsolete -DAxiom -Y $AXIOM/algebra -I $AXIOM/algebra
      Use the system command )set compiler args to change these 
      options.
#1 (Warning) Could not use archive file `libaxiom.al'.
#2 (Warning) Could not use archive file `libaxiom.al'.
"/usr/local/aldor/linux/1.1.0/include/axiom.as", line 4: 
import from AxiomLib;
............^
[L4 C13] #3 (Error) No meaning for identifier `AxiomLib'.
"/usr/local/aldor/linux/1.1.0/include/axiom.as", line 15: import { true: %, false: % } from Boolean; ..................................^ [L15 C35] #4 (Error) No meaning for identifier `Boolean'.
"/usr/local/aldor/linux/1.1.0/include/axiom.as", line 17: string: Literal -> %; ........................^.......^ [L17 C25] #5 (Error) No meaning for identifier `Literal'. [L17 C33] #6 (Error) There are no suitable meanings for the operator `->'.
"/usr/local/aldor/linux/1.1.0/include/axiom.as", line 18: } from String; .......^ [L18 C8] #8 (Error) No meaning for identifier `String'.
"/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/9147585987609704779-25px003.as", line 7: +: (%,%) -> %; .................^ [L7 C18] #12 (Error) There are no suitable meanings for the operator `->'.
"/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/9147585987609704779-25px003.as", line 9: coerce: % -> OutputForm; ..................^..^ [L9 C19] #10 (Error) There are no suitable meanings for the operator `->'. [L9 C22] #9 (Error) No meaning for identifier `OutputForm'. [L9 C22] #13 (Fatal Error) Too many errors (use `-M emax=n' or `-M no-emax' to change the limit).
The )library system command was not called after compilation.

fricas
nBin: BinExpr := 3

\label{eq7}3(7)
fricas
mBin: BinExpr := 4

\label{eq8}4(8)
fricas
pBin := nBin + mBin

\label{eq9}7(9)
fricas
eval(pBin)

\label{eq10}7(10)
fricas
qBin := pBin*(5::BinExpr)
Cannot convert from type PositiveInteger to NIL for value 5
eval(qBin)

\label{eq11}qBin(11)
Type: Expression(Integer)

On May 8 12:40 AM Bill Page writes:

Here is one way of writing this by defining the appropriate types for the expressions and sub-expressions.

spad
)abbrev category EXCAT ExprCat
++ Description:
++ Category of Integer-valued Arthemetic Expresions
ExprCat:Category == with
    eval: % -> Integer
    ++ \spad{eval} evaluates the expression as an Integer
    coerce: % -> OutputForm
    ++ \spad{coerce} displays the expression
)abbrev domain MI MkInt ++ Description: ++ Constructor for atomic Integers MkInt(Z:IntegerNumberSystem): ExprCat with coerce:Z -> % ++ \spad{coerce} converts a Z-valued object to an atomic Integer == add Rep := Integer coerce(i:Z):% == convert(i)@% eval(x:%):Integer == x pretend Integer coerce(x:%):OutputForm == outputForm eval x
)abbrev domain MA MkAdd ++ Description: ++ Constructor for additions MkAdd(X:ExprCat,Y:ExprCat): ExprCat with _+: (X,Y) -> % ++ \spad{+} returns an expression representing the sum == add Rep:=Record(left:X,right:Y) x + y == [x,y]$Rep eval(x:%):Integer == (eval((x@Rep).left) + eval((x@Rep).right))$Integer coerce(x:%):OutputForm == hconcat [ message "(", _ ((x@Rep).left)::OutputForm, _ message "+", _ ((x@Rep).right)::OutputForm, _ message ")"]
)abbrev domain MM MkMul ++ Description: ++ Constructor for multiplications MkMul(X:ExprCat,Y:ExprCat): ExprCat with _*: (X,Y) -> % ++ \spad{*} returns an expression representing the product == add Rep:=Record(left:X,right:Y) x * y == [x,y]$Rep eval(x:%):Integer == (eval((x@Rep).left) * eval((x@Rep).right))$Integer coerce(x:%):OutputForm == hconcat [message "(", _ ((x@Rep).left)::OutputForm, _ message "*", _ ((x@Rep).right)::OutputForm, _ message ")"]
)abbrev domain EX2 Expr2 ++ Description: ++ Constructor of Arithmetic Expressions over the Integers Expr2: ExprCat with coerce: Integer -> % _+:(%,%) -> % _*:(%,%) -> % == add Rep := Union(MkInt(Integer), MkAdd(%,%), MkMul(%,%)) eval(x:%): Integer == x case MkInt(Integer) => eval(x)$MkInt(Integer) x case MkAdd(%,%) => eval(x)$MkAdd(%,%) x case MkMul(%,%) => eval(x)$MkMul(%,%) coerce(n: Integer):% == n::MkInt(Integer) x + y == (x@Rep + y@Rep)$MkAdd(%,%) x * y == (x@Rep * y@Rep)$MkMul(%,%) coerce(x:%): OutputForm == x case MkInt(Integer) => coerce(x)$MkInt(Integer) x case MkAdd(%,%) => coerce(x)$MkAdd(%,%) x case MkMul(%,%) => coerce(x)$MkMul(%,%)
spad
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/2270268880364130397-25px005.spad
      using old system compiler.
   EXCAT abbreviates category ExprCat 
------------------------------------------------------------------------
   initializing NRLIB EXCAT for ExprCat 
   compiling into NRLIB EXCAT 
;;; *** |ExprCat| REDEFINED Time: 0 SEC.
finalizing NRLIB EXCAT Processing ExprCat for Browser database: --------constructor--------- --------(eval ((Integer) %))--------- --------(coerce ((OutputForm) %))--------- ; compiling file "/var/aw/var/LatexWiki/EXCAT.NRLIB/EXCAT.lsp" (written 31 JUL 2013 05:27:44 PM):
; /var/aw/var/LatexWiki/EXCAT.NRLIB/EXCAT.fasl written ; compilation finished in 0:00:00.004 ------------------------------------------------------------------------ ExprCat is now explicitly exposed in frame initial ExprCat will be automatically loaded when needed from /var/aw/var/LatexWiki/EXCAT.NRLIB/EXCAT
MI abbreviates domain MkInt ------------------------------------------------------------------------ initializing NRLIB MI for MkInt compiling into NRLIB MI compiling exported coerce : Z -> $ Time: 0.02 SEC.
compiling exported eval : $ -> Integer MI;eval;$I;2 is replaced by x Time: 0 SEC.
compiling exported coerce : $ -> OutputForm Time: 0 SEC.
(time taken in buildFunctor: 0)
;;; *** |MkInt| REDEFINED
;;; *** |MkInt| REDEFINED Time: 0.01 SEC.
Cumulative Statistics for Constructor MkInt Time: 0.03 seconds
finalizing NRLIB MI Processing MkInt for Browser database: --------constructor--------- --------(eval ((Integer) %))--------- --------(coerce ((OutputForm) %))--------- --------constructor--------- --------(coerce (% Z))--------- --->-->MkInt(): Spurious comments: Constructor for atomic Integers ; compiling file "/var/aw/var/LatexWiki/MI.NRLIB/MI.lsp" (written 31 JUL 2013 05:27:44 PM):
; /var/aw/var/LatexWiki/MI.NRLIB/MI.fasl written ; compilation finished in 0:00:00.013 ------------------------------------------------------------------------ MkInt is now explicitly exposed in frame initial MkInt will be automatically loaded when needed from /var/aw/var/LatexWiki/MI.NRLIB/MI
MA abbreviates domain MkAdd ------------------------------------------------------------------------ initializing NRLIB MA for MkAdd compiling into NRLIB MA compiling exported + : (X,Y) -> $ MA;+;XY$;1 is replaced by CONS Time: 0 SEC.
compiling exported eval : $ -> Integer Time: 0.01 SEC.
compiling exported coerce : $ -> OutputForm Time: 0 SEC.
(time taken in buildFunctor: 0)
;;; *** |MkAdd| REDEFINED
;;; *** |MkAdd| REDEFINED Time: 0 SEC.
Cumulative Statistics for Constructor MkAdd Time: 0.01 seconds
finalizing NRLIB MA Processing MkAdd for Browser database: --------constructor--------- --------(eval ((Integer) %))--------- --------(coerce ((OutputForm) %))--------- --------constructor--------- --------(coerce (% Z))--------- --------constructor--------- --------(+ (% X Y))--------- --->-->MkAdd(): Spurious comments: Constructor for atomic Integers --->-->MkAdd(): Spurious comments: Constructor for additions ; compiling file "/var/aw/var/LatexWiki/MA.NRLIB/MA.lsp" (written 31 JUL 2013 05:27:44 PM):
; /var/aw/var/LatexWiki/MA.NRLIB/MA.fasl written ; compilation finished in 0:00:00.016 ------------------------------------------------------------------------ MkAdd is now explicitly exposed in frame initial MkAdd will be automatically loaded when needed from /var/aw/var/LatexWiki/MA.NRLIB/MA
MM abbreviates domain MkMul ------------------------------------------------------------------------ initializing NRLIB MM for MkMul compiling into NRLIB MM compiling exported * : (X,Y) -> $ MM;*;XY$;1 is replaced by CONS Time: 0 SEC.
compiling exported eval : $ -> Integer Time: 0 SEC.
compiling exported coerce : $ -> OutputForm Time: 0 SEC.
(time taken in buildFunctor: 0)
;;; *** |MkMul| REDEFINED
;;; *** |MkMul| REDEFINED Time: 0 SEC.
Cumulative Statistics for Constructor MkMul Time: 0 seconds
finalizing NRLIB MM Processing MkMul for Browser database: --------constructor--------- --------(eval ((Integer) %))--------- --------(coerce ((OutputForm) %))--------- --------constructor--------- --------(coerce (% Z))--------- --------constructor--------- --------(+ (% X Y))--------- --------constructor--------- --------(* (% X Y))--------- --->-->MkMul(): Spurious comments: Constructor for atomic Integers --->-->MkMul(): Spurious comments: Constructor for additions --->-->MkMul(): Spurious comments: Constructor for multiplications ; compiling file "/var/aw/var/LatexWiki/MM.NRLIB/MM.lsp" (written 31 JUL 2013 05:27:44 PM):
; /var/aw/var/LatexWiki/MM.NRLIB/MM.fasl written ; compilation finished in 0:00:00.017 ------------------------------------------------------------------------ MkMul is now explicitly exposed in frame initial MkMul will be automatically loaded when needed from /var/aw/var/LatexWiki/MM.NRLIB/MM
EX2 abbreviates domain Expr2 ------------------------------------------------------------------------ initializing NRLIB EX2 for Expr2 compiling into NRLIB EX2 compiling exported eval : $ -> Integer Time: 0 SEC.
compiling exported coerce : Integer -> $ Time: 0 SEC.
compiling exported + : ($,$) -> $ Time: 0 SEC.
compiling exported * : ($,$) -> $ Time: 0 SEC.
compiling exported coerce : $ -> OutputForm Time: 0.01 SEC.
(time taken in buildFunctor: 0)
;;; *** |Expr2| REDEFINED
;;; *** |Expr2| REDEFINED Time: 0 SEC.
Cumulative Statistics for Constructor Expr2 Time: 0.01 seconds
finalizing NRLIB EX2 Processing Expr2 for Browser database: --------constructor--------- --------(eval ((Integer) %))--------- --------(coerce ((OutputForm) %))--------- --------constructor--------- --------(coerce (% Z))--------- --------constructor--------- --------(+ (% X Y))--------- --------constructor--------- --------(* (% X Y))--------- --------constructor--------- --->-->Expr2((coerce (% (Integer)))): Not documented!!!! --->-->Expr2((+ (% % %))): Not documented!!!! --->-->Expr2((* (% % %))): Not documented!!!! --->-->Expr2(): Spurious comments: Constructor for atomic Integers --->-->Expr2(): Spurious comments: Constructor for additions --->-->Expr2(): Spurious comments: Constructor for multiplications --->-->Expr2(): Spurious comments: Constructor of Arithmetic Expressions over the Integers ; compiling file "/var/aw/var/LatexWiki/EX2.NRLIB/EX2.lsp" (written 31 JUL 2013 05:27:44 PM):
; /var/aw/var/LatexWiki/EX2.NRLIB/EX2.fasl written ; compilation finished in 0:00:00.017 ------------------------------------------------------------------------ Expr2 is now explicitly exposed in frame initial Expr2 will be automatically loaded when needed from /var/aw/var/LatexWiki/EX2.NRLIB/EX2

fricas
n2:Expr2:=3

\label{eq12}3(12)
Type: Expr2
fricas
m2:Expr2:=4

\label{eq13}4(13)
Type: Expr2
fricas
p2:=n2+m2

\label{eq14}(3 + 4)(14)
Type: Expr2
fricas
eval(p2)

\label{eq15}7(15)
fricas
q2:=p2*5

\label{eq16}({(3 + 4)}<em> 5)(16)
Type: Expr2
fricas
eval(q2)

\label{eq17}35(17)




  Subject:   Be Bold !!
  ( 13 subscribers )  
Please rate this page: