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.




Reply via email to