Re: [Axiom-mail] Spad and inductive types

[Gabriel Dos Reis]

"Bill Page" <address@hidden> writes:

| 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)

This is probably one of the places where I was not happy with what I
came up with:  The representations of the multiplication and addition
need to have different field labels.  I was unhappy with that because
that just does not *look* right.  I have more obsrvations that I'll
send later.

|     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 ...

Yes.

| I don't understand that. Perhaps you can see a way around it?

Rep needs to be defined to something, not just a macro.

-- Gaby