[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-mail] Spad and inductive types
From: |
Ralf Hemmecke |
Subject: |
Re: [Axiom-mail] Spad and inductive types |
Date: |
Wed, 09 May 2007 11:27:03 +0200 |
User-agent: |
Thunderbird 2.0.0.0 (X11/20070326) |
On 05/09/2007 10:02 AM, Bill Page wrote:
> No, I think there is a serious misunderstanding here. What
> Gaby is talking about are "algebraic data types". See for
> example:
>
> http://en.wikipedia.org/wiki/Algebraic_data_type
>
> In Gaby's example Haskell code:
>
> data Expr = MkInt Int
> | MkAdd Expr Expr
> | MkMul Expr Expr
>
> 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.
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.
> The
> difference might seem a little subtle at first but we
> can clearly distinguish such things in languages like
> Spad and Aldor.
> 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. 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. And since
eval::Expr -> Int
the input to eval should be an actual element of type Expr, not the type
Expr itself.
> For example 'Complex' is such a
> constructor, so 'Complex Integer' is the domain of
> Gaussian Integers.
> Similarly in Haskel 'MkInt' is a type constructor and
> 'MkInt Int' is an algebraic type, in exactly the same way
> that 'Complex Integer' is a domain in Axiom. One should
> not be tempted to write: 'Complex 1'. Similarly 'MkInt 1'
> would not make sense.
Ah, is begin to understand. Have you seen my note on the use of the maros
Mkint ==> MkInt;
Mkadd ==> MkAdd;
Mkmul ==> MkMul;
? MkInt is the constructor (in the oo sense) and Mkint is just a tag.
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 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.
And I cannot say whether MkInt is a type constructor in Haskell, since I
don't know the language very well. An argument against it would be that
there is no code of the form
data MkInt a = ...
But I better should be quiet, I simply don't know enough of Haskell.
>> Well. What do you do with a data structure that has no
>> accessor functions?
>
> One is supposed to define functions over an algebraic data
> type by recursion. So what in Gaby wrote:
>
> eval::Expr -> Int
> eval (MkInt i) = i
> eval (MkAdd x y) = (eval x) + (eval y)
> eval (MkMul x y) = (eval x) * (eval y)
>
>
> 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.
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?
>> What do you gain by introducing the domains MkAdd and
>> MkMul?
>
> Well, it allows me to write
>
> Expr: ExprCat
> == add
> Rep == Union(Mkint:MkInt(Integer),
> Mkadd:MkAdd(%,%),
> Mkmul:MkMul(%,%))
>
> where Rep is a union of types in ExprCat. 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". What you need is an actual functions "union" to map an
element of type MkInt(Integer) into Rep.
>> That is a step to avoid a lot of (if not all) mutual
>> recursion in the construction of the Axiom library.
> I still think that is wishful thinking. :-(
It is probably not so wishful if you have looked a bit at the
bootstrapping of LibAldor and LibAlgebra. For example, Integer is not a
Ring in LibAldor, because Ring is only introduced in LibAlgebra. Still
one can do lots of things already with LibAldor. I must say, I don't see
a big bootstrapping problem at all in LibAldor.
Ralf
Re: [Axiom-mail] Spad and inductive types, Bill Page, 2007/05/09