Sat Dec 31 15:38:45 EST 2011

I'm sick of misunderstood morphisms..

Actually what needs to be expressed is a relation between 3 kinds of
things, using L for structuring, r for representation a for arrays and
t for the base type.  Substitude L with (,) in a straightforward way
to find an exhaustive list of all the representations.

With only L there are 3 * 2 = 6 combinations.  I'm noting

   L (r (a t))    as    L r a

This is all there is:

   L r a
   r L a
   a L r   (**)
   L a r   (*)
   r a L
   a r L   (*)

Which of these are meaningful?

I don't think (a (r .)) is meaningful (*).  This would be an array of
representations of something.  There is no need for a meta-language
array.  For the same reason (a (L (r .))) doesn't make sense either

Removing those cases leaves exactly what we expected:

   L r a    structure of representations of arrays
   r L a    representation of structure of arrays
   r a L    representation of array of structure

The operation I'm interested in is providing an equivalence between
the last two.  The first one is just a metalanguage structure and is
not so interesting, but it is there if the second one is there.

These 3 forms are related by these 2 transformations:

   r L a <-> L r a    pack/unpack: metalanguage embedding of data structures
   r L a <-> r a L    transposing of structuring and arrays
The trick now is to either express those directly.  The first one is
independent of a, and we can forget about it.  It's expressed by the
Struct constraint.

The second one is problematic because the representation r a L needs
to be implemented in some way.  So maybe it should be only virtual,
i.e. a relation between types used for inference only.

Currently in the implementation some link is broken between these 3.

So, if the problem is really just finding a representation of r a L
then maybe something can be done about it.  Anything "virtual" can
usually be implemented by a structure.

On the other hand, it might be enough to keep the current direct
implementation and encode the morphism in type class constraints.

The relation r L a <-> L r a or really r L <-> L r is expressed in
general as (with irrelevant constraints removed):

  Struct r (L t) (L (r t))


  Struct r s sr

Thinking about this a bit more and finding an understandable naming
scheme I get to this:

  {-  The following used this naming scheme for types

   r   representation (of anyting)
   a   array (of anything)
   s   structure (of base types)
   sa  structure of arrays (of base types)
   as  array of structurs (of base types)
   sra structure of representations of arrays (of base types)
   sr  structure of representations (of base types)
  class (TML m r,
         StructRepr r,
         Struct r sa sra,   -- structure of (a t_i)
         Struct r s sr)     -- structure of t_i
        => SArray m r s sa sr sra where
    _gets ::  r sa -> r Tint -> m (r s)
    _sets ::  r sa -> r Tint -> r s -> m (r ())

  -- Base case delegates to Array instance.
  instance (TMLword t,
            StructRepr r,
            Array m r a t)
           => SArray m r (L t) (L (a t)) (L (r t)) (L (r (a t))) where 

    _gets r_sa i = do
      (L a) <- return $ unatom r_sa
      v     <- _get a i
      return $ atom $ L v

    _sets r_sa i v = do
      (L a) <- return $ unatom r_sa
      (L v) <- return $ unatom v
      _set a i v

  -- Inductive case.
  instance (SArray m r s1 sa1 sr1 sra1,
            SArray m r s2 sa2 sr2 sra2)
           => SArray m r (s1,s2) (sa1,sa2) (sr1,sr2) (sra1, sra2) where

    _gets r_sa i = do
      (a1, a2) <- return $ uncons r_sa
      v1       <- _gets a1 i
      v2       <- _gets a2 i
      return $ cons (v1, v2)

    _sets r_sa i v = do
      (a1, a2) <- return $ uncons r_sa
      (v1, v2) <- return $ uncons v
      _sets a1 i v1
      _sets a2 i v2