[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-mail] Spad and inductive types
From: |
Gabriel Dos Reis |
Subject: |
Re: [Axiom-mail] Spad and inductive types |
Date: |
Wed, 9 May 2007 10:30:19 -0500 (CDT) |
On Wed, 9 May 2007, Ralf Hemmecke wrote:
| > Well, I did not interepret it as a slur against Haskell. However, it did
| > appear to me to be fundamentally incorrect to miss the core ideas of
| > algebraic data typea and how they lead to GADT:
| > data Expr where
| > MkInt:: Integer -> Expr
| > MkAdd:: Expr -> Expr -> Expr
| > MkMul:: Expr -> Expr -> Expr
| >
| > That is all that is needed to define more operations on values of
| > type Expr.
|
| Gaby, I think I must disagree with your last sentence. It might probably be
| correct for Haskell, because there is the pattern matching thing, but in
| general one would need also functions like
|
| apply: (%, 'MkInt') -> Integer;
| apply: (%, 'MkAdd') -> %
|
| case: (%, 'MkInt') -> Boolean;
| etc.
|
| Accessor functions seem to be somewhat hidden in Haskell, but in Aldor they
| would have to be explicit.
Yes, you are right -- I implicitly assumed accessors (in terms of
pattern matching) or case expression in case of Spad or Aldor.
You're right that I should have spelled it out explicitly.
| Anyway, that GADT example above looks already surprisingly like Aldor
| (although it probably means something else --- what exactly?).
It means that Expr is a datatype with the data constructors listed
in the where clause, and only those.
I believe the core ideas are present in Boot and Aldor, but they have
not been made as explicit and concise as it could be.
-- Gaby
- Re: [Axiom-mail] Spad and inductive types, (continued)
Re: [Axiom-mail] Spad and inductive types, Bill Page, 2007/05/09