I have studied the materials but not tried it out. the effort is directed
towards allowing to build algebraic structures with haskell in a way closer
to regular algebra (i was reading this summer the classic macLean &
Birkhoff, algebra, (3rd edition) - highly recommended!). the proposal is
very interesting and the materials covers a surprisingly large field.
the major problem encountered if one tries to achieve this is the class Num
(and Integral, Rational etc). This is not a simple theoretical problem of
interest only to mathematicians - we are interested in practical
applications of Haskell in geographic information systems and are extremely
happy with haskell/hugs, except for some details in the prelude, Num being
one. The current definition of Num comes in your way in numerous ways and i
suggest that this should be fixed.
the proposal made is essentially to divided Num in two classes: Additive and
Multiplicative, which makes sense to me and is likely to overcome some of
the problems we have encountered. I will experiment with this proposal and
see how it works for us. the test case will be geometry operations, based on
vector algebra.
the proposal goes much further and includes a lot of interesting algebra for
for most of which i do not currently see much application in our area. i
would suggest that the authors separate the proposal into two parts - the
piece which identifies the parts which must be changed in the prelude and a
library of routines, which demonstrate that on the proposed base
functionality in the prelude an algebraic package can be built. the goal
must be to put as little of this into the prelude to reduce a) the burden on
people who use haskell for other purposes b) to reduce the potential
interference with other code (i object to a wholesale use of good names in
the prelude which leaves nothing to the application, the current situation
is already bad enough...).
It seems to me that all what is needed to change in the Prelude are the
classes defining numbers (Num, Rationl, Fractional...); everything else can
go in a support library? is this correct?
i am interested in an improvement of the numeric classes and hope the
proposal by Mechveliani can contribute to this.
andrew frank
Andrew U. Frank
Geoinformation E127 phone: +43 1 588 01 12710
TU Vienna secr. +43 1 588 01 12700
Gusshausstrasse 27-29 fax +43 1 588 01 12799
A-1040 Vienna Austria cellular phone +43 676 41925 72
http://www.geoinfo.tuwien.ac.at/persons/frank.html
-----Original Message-----
From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED]]On
Behalf Of S.D.Mechveliani
Sent: Tuesday, August 15, 2000 2:27 PM
To: [EMAIL PROTECTED]
Cc: [EMAIL PROTECTED]
Subject: basAlgPropos, dependent types
Dear haskellers,
I suggest the two points to your attention.
New basAlgPropos
----------------
materials reside in
http://www.botik.ru/pub/local/Mechveliani/basAlgPropos
/haskellInCA.ps.zip
/bal-pre-0.01/
Read the paper first.
The implementation works, at least, so show the demo-s.
But it is about 30% documented,
the sources need to be brought to a better shape.
I do not know when this project will be completed.
I was not disposed to show it, but one of the users asked for the
implementation. So, OK, let it exist in an in-complete form.
Attempt with dependent types
----------------------------
This may present an alternative to the sample argument approach used
in basAlgPropos.
I experimented with Cayenne, for several days and remain in a doubt.
I understand few in Cayenne. Still, here are my newbie impressions.
(Inst) Cayenne lacks half of the Haskell instance possibilities.
(DTG) Sometimes dependent types do a good job for basAlgPropos.
(DTB) In other cases, the record type expressions become too
complex, maybe, the language should be able to specialize
some record types automatically.
Could the Cayenninsts advise?
------------------
Sergey Mechveliani
[EMAIL PROTECTED]
-------------------------------------------------------------------
(Inst)
------
Example. In Haskell, if a type T matches the instance of Eq,
then it is clear, what does it mean
x == y for x :: T.
And the match is determined according to the data constructors used
to build x. The map
x --> T --> instance match
works automatically.
In Cayenne, the programmer has to bring in from somewhere the record
eq :: Eq T and set
eq.(==) x y
The map x --> eq is never automatic: the place "from somewhere"
is never related to the surrounding context of a variable x.
This leads to more complex and less safe programs.
But could Cayenne accept the
domain membership declaration?
In addition to x :: T, to introduce the denotation x <- dom,
( ::: ?)
where dom is a collection (a record, a finite map ...) that may
contain several instance records.
Example:
let dom = struct {eq = eq_Int; enum = enum_Int; num = num_Int}
x,y <- dom
in (x==y) && (x+y == x*y)
The meaning of this example is that x,y belong to the mathematical
domain dom. dom is represented as a container of the instances
(records) of Eq, Enum, Num. The instances can be extracted by their
names.
Now, as x+y is in the scope of x <- dom declaration, it is
clear from what universe to get the instance records for (==) -- Eq,
(+) -- Num, and so on. And the compositions of the field selection
`.' can be rebuilt automatically.
(DTG)
-----
Sometimes dependent types do a good job for basAlgPropos.
For example, I defined the residue domain Int/(m) modulo m
as a record type with the field `base' containing the value
parameter m :: Int.
And the compiler rejects at the compile time the expressions like
num.(+) r1 r2, r1 :: R1 <--> Int/(m1),
r2 :: R2 <--> Int/(m2)
- unless the user program helps it to proof that the types
(residue domains) R1 and R2 are the same. That is m1 == m2.
The easiest way to help such proof is to write the same variable m
for m1, m2, or maybe, m1 = ...
m2 = m1,
- but this is not always the best. Anyway, it is good that the
compiler needs here to insure in the type equality.
(DTB)
-----
A more advanced example leads to complications.
type Attributes = Pair Bool Bool
type OrdSet a = sig {(==) :: a -> a -> Bool;
(<) :: a -> a -> Bool;
attributes :: Attributes;
finList :: List a
}
OrdSet exports equality and ordering on a set, finite listing and
a pair of attributes.
The first attribute shows whether (<) is transitive.
The second shows whether a set is finite.
finList lists all the elements of a set, and it has sense only
for a finite set.
maxOfSet :: (a :: #) |-> OrdSet a -> a
has to find the maximum of a given set.
But the compiler has to reject the program if maxOfSet is applied
to a set with wrong attributes.
For example,
maxOfSet _ OrdSet_Int is to be rejected by the compiler,
maxOfSet _ OrdSet_Bool --> True,
maxOfSet _ (OrdSet_Pair OrdSet_Bool OrdSet_Bool) --> (True,True).
The first is because the record OrdSet_Int :: OrdSet Int
contains the attributes (True,False).
The transitiveness of (<) and the infiniteness are postulated with
the word `concrete' when the record is built.
In OrdSet_Bool, (True,True) are postulated.
For Pair Bool Bool, OrdSet_Pair computes the field value
(A x B).attributes via A.attributes and B.attributes.
(A x B).(<) is defined coordinatewise-lexicographically. The user
knows that if A.(<), B.(<) are transitive, then (A x B).(<) is
transitive. And the user puts this as the computation rule for the
attributes in OrdSet_Pair A B.
Seeing this program, the compiler should derive automatically that
OrdSet_Pair OrdSet_Bool OrdSet_Bool
possesses the needed attributes.
I tried to program this. And never succeeded, until introduced
additional attribute parameter:
type Attributes = Pair Bool Bool
type OrdSet a (atts :: Attributes) =
sig {(==) :: a -> a -> Bool;
(<) :: a -> a -> Bool;
attributes :: Pair Bool Bool = atts;
finList :: List a
}
This leads to rather complex type for the direct product:
OrdSet_Pair :: (a, b :: #) -> (attrsA, attrsB :: Attributes) ->
(A :: OrdSet a attrsA) -> (B :: OrdSet b attrsB)
->
OrdSet (Pair a b) (pairAttrs attrsA attrsB)
OrdSet_Pair _ _ attrsA attrsB A B =
...
These arguments attrsA, attrsB
in the type expression look superfluous. Because their values can
be extracted from A, B. But I cannot get rid of them.
I wonder, what is the proper way to program such task.
