Re: [boost] [serialization] Dealing with any tainted types.

Subject: Re: [boost] [serialization] Dealing with any tainted types.
From: David Sankel (camior_at_[hidden])
Date: 2011-01-17 13:47:08

On Fri, Jan 14, 2011 at 6:17 PM, Robert Ramey <ramey_at_[hidden]> wrote:

> David Sankel wrote:
> > Thanks for your detailed response Robert...
> >> <snip>
> >> To really do this right, I see the following as necessary
> >>
> >> a) Clarify and simplify the current archive concept.  I've thought
> >> about this alot and know what I want to do - but I'm not excited
> >> enough to
> >> do it.
> >>
> >
> > I've been giving some thought to this. Not as much clarifying and
> > simplifying, but more distilling the essence of the domain. I have a
> > feeling that if we nail the essence down, all the compositionality
> > will be there without having to tack it on as an afterthought.
> >
> > Here's what I have so far:
> >
> > concept Archive:
> >  struct _ where
> >  { typedef _ RState
> >  ; typedef _ WState
> >
> >  ; template< typename T >
> >    struct lookup
> >    { typedef _ type  // This _ is either mpl::void_ or
> >                      // std::pair< function< void (RState&, const T&)
> >                      > //          , function< T (WState&) >
> >                      //          >
> >    ; type operator()() const;
> >    }
> >  };
> >
> >
> > Something fits the archive concept if they fill in the blanks above.
> > RState and WState are state information required for reading and
> > writing. The lookup type function, passed type T, will either return
> > mpl::void_ or a pair. If it returns void_ we know that T is not
> > considered a primitively serializable type. If it returns the pair,
> > we know it is a serializable type witnessed by the pair of write and
> > read functions returned by operator().
> >
> > One key condition is that the primitive types for an Archive, if they
> > are templates, must be *fully saturated*. Meaning that:
> >
> > template<>
> > lookup< std::vector<bool> >
> >
> >
> > is fine, but
> >
> > template<typename T>
> > lookup< std::vector<T> >
> >
> >
> > is not. This condition prevents recursive lookup calls with
> > non-primitives. This, I think, is going to be the key to
> > compositionality later. More to come...
> >
> > Does all of this make sense so far?
>
> In all honesty, I didn't understand even one sentence of the above.
>

Ah, darn. I have the terrible curse of thinking in a very precise and
powerful language (denotational semantics with Agda as the semantic domain
in this case), but find it terribly difficult to translate it to prose.

For the record, here is what I'm trying to translate:

μ [[concept Archive]] = data Archive : Set where
                         archive : (RState,WState : Set)
                                 → (l : List ( T : Set
                                             , (RState,T) → IO RState
                                             , WState → IO (WState,T)
                                             ))
                                 → UniqueFsts l
                                 → Archive

I'm going to think more about how to explain this and try again. Thanks for
hanging in there.

David

-- 
David Sankel
Sankel Software
www.sankelsoftware.com