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.
