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:
fricas
(1) -> <spad>
fricas
)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>
fricas
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 SEC.
Warnings:
[1] eval: lAdd has no value
[2] eval: rAdd has no value
[3] eval: lMul has no value
[4] eval: rMul has no value
[5] coerce: lAdd has no value
[6] coerce: rAdd has no value
[7] coerce: lMul has no value
[8] coerce: rMul has no value
Cumulative Statistics for Constructor Expr
Time: 0 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 01 NOV 2024 01:13:20 AM):
; wrote /var/aw/var/LatexWiki/EX.NRLIB/EX.fasl
; compilation finished in 0:00:00.012
------------------------------------------------------------------------
Expr is now explicitly exposed in frame initial
Expr will be automatically loaded when needed from
/var/aw/var/LatexWiki/EX.NRLIB/EXfricas
n:Expr:=3
Type: Expr
fricas
m:Expr:=4
Type: Expr
fricas
p:=n+m
Type: Expr
fricas
eval(p)
fricas
q:=p*5
Type: Expr
fricas
eval(q)
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 Aldor compiler and options
-O -Fasy -Fao -Flsp -lfricas -Mno-ALDOR_W_WillObsolete -DFriCAS -Y $FRICAS/algebra -I $FRICAS/algebra
Use the system command )set compiler args to change these
options.
"/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/9147585987609704779-25px003.as", line 1:
#include "axiom"
^
[L1 C1] #1 (Error) Could not open file `axiom'.
The )library system command was not called after compilation.fricas
nBin: BinExpr := 3
BinExpr is not a valid type.
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 01 NOV 2024 01:13:20 AM):
; wrote /var/aw/var/LatexWiki/EXCAT.NRLIB/EXCAT.fasl
; 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
Local variable Rep type redefined: (Join (IntegerNumberSystem) (LinearlyExplicitOver (Integer)) (PolynomialFactorizationExplicit) (ConvertibleTo (String)) (OpenMath) (Canonical) (canonicalsClosed) (Hashable) (CATEGORY domain (SIGNATURE random (% %)) (SIGNATURE seedRandom ((Void))))) to (Join (SetCategory) (CATEGORY domain (SIGNATURE ~= ((Boolean) (Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))) (Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))))) (SIGNATURE coerce ((OutputForm) (Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))))) (SIGNATURE autoCoerce ((Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))) (Integer))) (SIGNATURE coerce ((Integer) (Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))))) (SIGNATURE autoCoerce ((Integer) (Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))))) (SIGNATURE case ((Boolean) (Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))) (Integer))) (SIGNATURE autoCoerce ((Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))) (Record (: lAdd %) (: rAdd %)))) (SIGNATURE coerce ((Record (: lAdd %) (: rAdd %)) (Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))))) (SIGNATURE autoCoerce ((Record (: lAdd %) (: rAdd %)) (Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))))) (SIGNATURE case ((Boolean) (Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))) (Record (: lAdd %) (: rAdd %)))) (SIGNATURE autoCoerce ((Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))) (Record (: lMul %) (: rMul %)))) (SIGNATURE coerce ((Record (: lMul %) (: rMul %)) (Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))))) (SIGNATURE autoCoerce ((Record (: lMul %) (: rMul %)) (Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))))) (SIGNATURE case ((Boolean) (Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))) (Record (: lMul %) (: rMul %))))))
compiling exported coerce : Z -> %
Time: 0 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 SEC.
Cumulative Statistics for Constructor MkInt
Time: 0 seconds
finalizing NRLIB MI
Processing MkInt for Browser database:
--------constructor---------
--------(coerce (% Z))---------
; compiling file "/var/aw/var/LatexWiki/MI.NRLIB/MI.lsp" (written 01 NOV 2024 01:13:20 AM):
; wrote /var/aw/var/LatexWiki/MI.NRLIB/MI.fasl
; compilation finished in 0:00:00.008
------------------------------------------------------------------------
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
Local variable Rep type redefined: (Join (SetCategory) (CATEGORY domain (SIGNATURE construct ((Record (: left X) (: right Y)) X Y)) (SIGNATURE ~= ((Boolean) (Record (: left X) (: right Y)) (Record (: left X) (: right Y)))) (SIGNATURE coerce ((OutputForm) (Record (: left X) (: right Y)))) (SIGNATURE elt (X (Record (: left X) (: right Y)) left)) (SIGNATURE elt (Y (Record (: left X) (: right Y)) right)) (SIGNATURE setelt! (X (Record (: left X) (: right Y)) left X)) (SIGNATURE setelt! (Y (Record (: left X) (: right Y)) right Y)) (SIGNATURE copy ((Record (: left X) (: right Y)) (Record (: left X) (: right Y)))))) to (Join (IntegerNumberSystem) (LinearlyExplicitOver (Integer)) (PolynomialFactorizationExplicit) (ConvertibleTo (String)) (OpenMath) (Canonical) (canonicalsClosed) (Hashable) (CATEGORY domain (SIGNATURE random (% %)) (SIGNATURE seedRandom ((Void)))))
compiling exported + : (X,Y) -> %
MA;+;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)
;;; *** |MkAdd| REDEFINED
;;; *** |MkAdd| REDEFINED
Time: 0 SEC.
Warnings:
[1] eval: left has no value
[2] eval: right has no value
Cumulative Statistics for Constructor MkAdd
Time: 0 seconds
finalizing NRLIB MA
Processing MkAdd for Browser database:
--------constructor---------
--------(+ (% X Y))---------
; compiling file "/var/aw/var/LatexWiki/MA.NRLIB/MA.lsp" (written 01 NOV 2024 01:13:20 AM):
; wrote /var/aw/var/LatexWiki/MA.NRLIB/MA.fasl
; compilation finished in 0:00:00.008
------------------------------------------------------------------------
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.
Warnings:
[1] eval: left has no value
[2] eval: right has no value
Cumulative Statistics for Constructor MkMul
Time: 0 seconds
finalizing NRLIB MM
Processing MkMul for Browser database:
--------constructor---------
--------(* (% X Y))---------
; compiling file "/var/aw/var/LatexWiki/MM.NRLIB/MM.lsp" (written 01 NOV 2024 01:13:20 AM):
; wrote /var/aw/var/LatexWiki/MM.NRLIB/MM.fasl
; compilation finished in 0:00:00.008
------------------------------------------------------------------------
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
Local variable Rep type redefined: (Join (SetCategory) (CATEGORY domain (SIGNATURE ~= ((Boolean) (Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)) (Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)))) (SIGNATURE coerce ((OutputForm) (Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)))) (SIGNATURE autoCoerce ((Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)) (MkInt (Integer)))) (SIGNATURE coerce ((MkInt (Integer)) (Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)))) (SIGNATURE autoCoerce ((MkInt (Integer)) (Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)))) (SIGNATURE case ((Boolean) (Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)) (MkInt (Integer)))) (SIGNATURE autoCoerce ((Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)) (MkAdd % %))) (SIGNATURE coerce ((MkAdd % %) (Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)))) (SIGNATURE autoCoerce ((MkAdd % %) (Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)))) (SIGNATURE case ((Boolean) (Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)) (MkAdd % %))) (SIGNATURE autoCoerce ((Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)) (MkMul % %))) (SIGNATURE coerce ((MkMul % %) (Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)))) (SIGNATURE autoCoerce ((MkMul % %) (Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)))) (SIGNATURE case ((Boolean) (Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)) (MkMul % %))))) to (Join (SetCategory) (CATEGORY domain (SIGNATURE construct ((Record (: left X) (: right Y)) X Y)) (SIGNATURE ~= ((Boolean) (Record (: left X) (: right Y)) (Record (: left X) (: right Y)))) (SIGNATURE coerce ((OutputForm) (Record (: left X) (: right Y)))) (SIGNATURE elt (X (Record (: left X) (: right Y)) left)) (SIGNATURE elt (Y (Record (: left X) (: right Y)) right)) (SIGNATURE setelt! (X (Record (: left X) (: right Y)) left X)) (SIGNATURE setelt! (Y (Record (: left X) (: right Y)) right Y)) (SIGNATURE copy ((Record (: left X) (: right Y)) (Record (: left X) (: right Y))))))
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 SEC.
(time taken in buildFunctor: 0)
;;; *** |Expr2| REDEFINED
;;; *** |Expr2| REDEFINED
Time: 0 SEC.
Cumulative Statistics for Constructor Expr2
Time: 0 seconds
finalizing NRLIB EX2
Processing Expr2 for Browser database:
--------constructor---------
--->-->Expr2((coerce (% (Integer)))): Not documented!!!!
--->-->Expr2((+ (% % %))): Not documented!!!!
--->-->Expr2((* (% % %))): Not documented!!!!
; compiling file "/var/aw/var/LatexWiki/EX2.NRLIB/EX2.lsp" (written 01 NOV 2024 01:13:20 AM):
; wrote /var/aw/var/LatexWiki/EX2.NRLIB/EX2.fasl
; compilation finished in 0:00:00.008
------------------------------------------------------------------------
Expr2 is now explicitly exposed in frame initial
Expr2 will be automatically loaded when needed from
/var/aw/var/LatexWiki/EX2.NRLIB/EX2fricas
n2:Expr2:=3
Type: Expr2
fricas
m2:Expr2:=4
Type: Expr2
fricas
p2:=n2+m2
Type: Expr2
fricas
eval(p2)
fricas
q2:=p2*5
Type: Expr2
fricas
eval(q2)
