Re: Spad and inductive types

Quoting Ralf Hemmecke <[email protected]>:

> On 05/09/2007 10:02 AM, Bill Page wrote:
>  > ... 
>  > MkInt is *not* a function which when given an Integer
>  > returns something of type Expr. It is type *constructor*,
>  > that is, when given 'Int' MkInt returns a subtype of Expr. 
>
> Before you criticize... I don't claim that I am right. What
> comes is just my current understanding. 
>

Sorry, I do not mean to criticize. I am also only writing about my
current (provisional) understanding. 

> Let me quote from
> http://en.wikipedia.org/wiki/Algebraic_data_type
>
>    Here, Empty, Leaf and Node are the constructors. Somewhat
>    similar  to a function, a constructor is applied to arguments of
>    an appropriate type, then yielding an instance of the data type
>    to which the constructor belongs. 
>

I would emphasize *Somewhat similar to a function*. Yes the
Haskell definition does define the application of data constructors
to "arguments of an appropriate type". 

> ... 
>  > In Spad and Aldor a type constructor is a function that
>  > returns a Type. 
>
> I agree on the latter, but as you said, it is a "type constructor". 
> In the wikipedia article "constructor" sounds to me more like a
> constructor in object oriented languages like Java. One creates
> an instance of the type. 

Both categories and domains are types in Aldor. A constructor
can return a domain as an instance of a category. Any way you
write it

   data Expr = MkInt Integer | ... 

defines Expr as a type with members 'MkInt 1', 'MkInt 2', ... etc. 

> So as in
> http://lists.nongnu.org/archive/html/axiom-mail/2007-05/msg00001.html
> one says
>
> eval (MkInt i) = i
>
> i.e. the argument is an integer and not the type Integer. 

The argument of eval above is 'MkInt i'. It is not an integer. 
It is a member of the type 'MkInt Integer', which is a subtype
of Expr. 

> And since
>
> eval::Expr -> Int
>
> the input to eval should be an actual element of type Expr, not
> the type Expr itself. 

I agree. 

> ... 
> Ah, is begin to understand. Have you seen my note on the use of the
> macros
>
> Mkint ==> MkInt;
> Mkadd ==> MkAdd;
> Mkmul ==> MkMul;
>
> ? MkInt is the constructor (in the oo sense) and Mkint is just a tag. 
>

Yes. 

> The tag Mkint corresponds to the MkInt in the above Haskell code. 
> And a tag (together with the (aldor) functions MkInt, etc. is enough to
> simulate the Haskell code. In the Haskell code Mkint and MkInt is
> denoted by the same identifier. 

I agree. 

>
> I still don't say that one cannot simulate Haskell's MkInt by a
> Aldor domain constructor. You have shown that it works on
> http://wiki.axiom-developer.org/SandBoxAldorInductiveTypes . 
> But it seems to be unnecessary overhead to me. 
>

Maybe that is true. I have not looked at the actual generated
Lisp code. I very much doubt that it is anything as economical
as the Lisp output of Shoe (New Boot) that Gaby showed in the
email that started this thread. But I would expect that: Spad is
not Boot. 

>  > ... 
>  > in Haskell, by a kind of convenient abuse of notation
>  > (or polymorphism if you wish) 'MkInt' also denotes a
>  > function
>  >
>  >   MkInt: Int -> MkInt Int
>  >
>  > that creates an object of type 'MkInt Int' from an object
>  > in 'Int'. I think this is a potential source of confusion. 

Probably I should have avoided the wording above that might
(incorrectly) be interpreted as a slur against Haskell. That is
certainly not my intent and perhaps it would have help to avoid
Gaby's reaction to my email. Really I am only talking about
how I think this concept should be written in Spad and Aldor. 

>
> I agree that it's a source of confusion. But I must admit that
> I would have written
>
>    MkInt: Int -> Expr
>
> instead. Otherwise there would be a type mismatch in
>
>    eval (MkInt i) = i
>
> since MkInt(Int) is not equal to Expr. Don't you agree?

'MkInt i' is a member of the type 'MkInt Integer' which is
a subtype of Expr. The expression

     eval (MkInt i) = i

only defines eval over this subtype of Expr. The complete
definition of 'eval' also requires two other definitions for
'MkAdd Expr Expr' and 'MkMul Expr Expr', respectively. 

> ... 
> >. Then
>  >
>  >   rep: % -> Rep
>  >
>  > automatically classifies members of Expr (implements the
>  > pattern matching) and
>  >
>  >   per: Rep -> %
>  >
>  > injects these subtypes into Expr. 
>
> Unfortunately, in Aldor rep and per are macros and actually only do
> some "pretend". 

You are right however they also involve @. The reason is that they
must be "type-safe". Assuming however that they are type-safe,
then they can be written as functions as I show above. (In fact this
is used in several places in the Axiom library.)

> What you need is an actual functions "union" to map an element
> of type MkInt(Integer) into Rep. 
>

Yes, "union" is needed in the implementation, but my point is that

   rep: % -> Rep

maps elements of Expr directly into the Union. 'case' can then be
used to classify them as 'MkInt ...', 'MkAdd ...' or 'MkMul ...'. 

> ... 

Regards,
Bill Page.