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?

  data Expr = MkInt Int
| 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)
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:

)abbrev domain EX Expr
Expr(): with
eval: % -> Integer
coerce: Integer -> %
coerce: % -> OutputForm
_+: (%,%) -> %
_*: (%,%) -> %
MkInt ==> Integer
MkMul ==> Record(lMul:%,rMul:%)
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 "(",          _
message "+",          _
message ")"]
x case MkMul => hconcat [message "(",          _
(x.lMul)::OutputForm, _
message "*",          _
(x.rMul)::OutputForm, _
message ")"]
   Compiling FriCAS source code from file
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 (1)
Type: Expr
fricas
m:Expr:=4 (2)
Type: Expr
fricas
p:=n+m (3)
Type: Expr
fricas
eval(p) (4)
Type: PositiveInteger?
fricas
q:=p*5 (5)
Type: Expr
fricas
eval(q) (6)
Type: PositiveInteger?

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,
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;
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 (7)
Type: PositiveInteger?
fricas
mBin: BinExpr := 4 (8)
Type: PositiveInteger?
fricas
pBin := nBin + mBin (9)
Type: PositiveInteger?
fricas
eval(pBin) (10)
Type: PositiveInteger?
fricas
qBin := pBin*(5::BinExpr)
Cannot convert from type PositiveInteger to NIL for value
5
eval(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.

)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
)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
Rep := Integer
coerce(i:Z):% == convert(i)@%
eval(x:%):Integer == x pretend Integer
coerce(x:%):OutputForm == outputForm eval x
++ Description:
_+: (X,Y) -> %
++ \spad{+} returns an expression representing the sum
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
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 -> %
_+:(%,%) -> %
_*:(%,%) -> %
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(%,%)
   Compiling FriCAS source code from file
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
------------------------------------------------------------------------
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)
Time: 0 SEC.
Time: 0.01 seconds
finalizing NRLIB MA
--------constructor---------
--------(eval ((Integer) %))---------
--------(coerce ((OutputForm) %))---------
--------constructor---------
--------(coerce (% Z))---------
--------constructor---------
--------(+ (% X Y))---------
; 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
/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 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 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 (12)
Type: Expr2
fricas
m2:Expr2:=4 (13)
Type: Expr2
fricas
p2:=n2+m2 (14)
Type: Expr2
fricas
eval(p2) (15)
Type: PositiveInteger?
fricas
q2:=p2*5 (16)
Type: Expr2
fricas
eval(q2) (17)
Type: PositiveInteger?

 Subject:   Be Bold !! ( 15 subscribers )