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