First Class Representations

[Patrick Premont]

Francois-Rene Rideau <rideau@ens.fr> writes :
> Patrick, are you still here?

Yes!

>    Here are some very late thoughts about your FCREP article.
> Those are the very same objections I had originally,
> but presented in a way that have grown to full maturity since.
> Your article was essential to help me find those objections
> and consequently crystallize the ideas that are at the center of my design
> for a reflective language that allows proofs.
>    BTW, could you introduce me to Prof. Malenfant?

Sure. I'll e-mail you about that.

> >> * I think that if we consider representations as a general concept,
> >>  not only for representing end-user objects with low-level bit streams,
> >>  then we got something very generic,
> >>  that is the very basis of computational reflection:
> >>  more abstract objects being represented by more concrete objects,
> >>  with arbitrary variations and subtleties about abstractness/concreteness.
> >
> > Yes absolutely. I've specialized my description for low level cases to
> > show that it can go all the way down.
>    Yes. That's great.
> 
> > The next version should be an
> > almost complete rewrite where I forget about that triple and see
> > representations as relations (or morphisms) between two sets.
> >
>    Relations, no; morphisms, yes.
> The structure being conserved by "representation"
> can be considered as a mapping to the an abstract set of "meaning".
> Something represents an integer if I can attach to it the
> meaning of the integer being represented.
> That's the "semantic function" as described in semantic theory
> (see e.g. articles by Cousot&Cousot).
>    The way the system chooses a particular representing instance,
> that is your function from the set of abstract represented objects to the
> concrete representations, is not what caracterizes the representation,
> but a meta-object that is known as the instantiation tactic,
> which people aware of the Curry-Howard isomorphism know is isomorphic
> to proof tactics in formal proof systems.
>    A same representation can have many different corresponding tactics:
> see lots of compilers on a same architecture with same calling convention,
> each with lots of code-generation/optimization switches.
> There might be no every-where defined total *computable* mapping from
> represented space to representing space,
> but you could still say that something actually represents another thing
> because *the semantic function* is uniquely well-defined.

Although in particular applications it might be more useful to see the
relation as a mapping from abstract to concrete, and in other
situations from concrete to abstract, the direction is not important
to the characterization of what is a representation. Also if you are
to consider partial and multi-valued functions, to handle objects that
have no representing state and those that have more than one, and if
you are to consider ambiguous or imprecise representations which map
(or relate) many objects to the same states, you might as well say
that representation are relations instead of partial multi-valued
functions (for conciseness, since these things cam serve the same
purposes), no matter which way you'd want the function to go. If by
morphism you mean something that can be partial and multi-valued then
I mean representations to be practically the same thing (modulo the
objection in the next paragraph). If not, then morphisms don't handle
the cases mentionned above.

And on the issue of morphism from A to B versus function from A to B
or relation on AxB, the difference is the presence of a bijection
between function and predicates on A to functions and predicates on
B. We do want that bijection in a representation that relates two
types, but it is not appropriate when a representation relates a type
to a state space of a dynamic system. That's because to apply a
function to two objects in the type, you don't what to apply a
function to two states, you want to tailor the dynamic system (program
it) so that one state which represents both objects (with different
representations otherwise they wouldn't be concurrently satisfiable)
eventually evolves into a state where the result of the function is
represented. So the usual concept of morphism isn't what we want
here. We want the relation from type to state space, as usual, plus a
description of how to implement the functions of the type by
programming the dynamic system.

> > Calling
> > them abstract and concrete looks like a good idea.
> I stick to it. Plus it shows how abstract and concrete are
> concepts relative to a considered representation.
> 
> > Although I'd pitch
> > in some comment that what makes a representation useful for computation
> > in our physical universe is that its concrete set is a set of states
> > of some system (or can be mapped to such a set through additional
> > representations).
> 
> 
> >> * I'd call both sets Universes rather than Type and Set of States.
> >>  You'd have the "Univers de depart" and "Univers d'arrivee" of your mapping.
> >>  For many reasons, and particularly because I don't agree with the
> >>  direction of your mapping, I propose that another terminology be used:
> >
> > What do you mean by direction ? You mean you'd like it to go in the opposite
> > direction ? I think I'll use relations anyway. Are you saying you'd
> > prefer the concrete universe to be the first argument of the relation ?
> > I tend to prefer the other way.
> >
> Yeah, I do prefer defining the representation
> by the existence of the Semantic Function.

You could define a representation as a semantic function (but not as
its existance), but then you'd have to make it multi-valued to handle
ambiguous or imprecise representations. We could just say that in
general representations are relations R between abstract and concrete
(or type and state space) (and put whichever argument you prefer
first). Then the semantic function would be R or R^-1, depending
on the chosen order, and would be single-valued when dealing with
precise representation. 

Whatever order you chose, there is no difference in expressivity
or capability in the resulting programming system.

> That's what comply to the formal theory of Semantics,
> and gives us a clean framework to prove things:
> an object is actually a representation of given Semantic Function
> iff the function is a morphism,
> i.e. conserves all the properties we prove on the abstract object.
> That's *exactly* what is meaningful to write proofs.
>    On the contrary your opposite mapping,
> that I identify with the instantiation tactic,
> just CANNOT be a morphism in the general case
> (e.g. the mapping from a set of considered objects to the way the
> objects are represented in dynamically allocated realtime GCed memory),
> and shouldn't even when it can
> (imagine that your compiler would never optimize
> because compiling wouldn't be a morphism then!).

I don't get your objection. I think it has to do with your morphisms
being single-valued. But I'd like to restate that no matter which
way (direction) you define representations, you get the same expressivity.
If sematic functions are more useful in some circustances, we can use
them, no matter how we defined representations.

[cut]

> >> * on real computers, the set of states is finite,
> >>  whereas on languages used, the set of objects is infinite;
> >
> > Yes. And that leads to the infamous "out of memory" problem.
> >
> And to Ariane V exploding...

Is this just an example of a possible consequence or did this
really happen because of such a problem ?

> Our framework *MUST* take that into account,
> or the problem will stab you in your back at the worst moment.
> Again, if we consider the semantic function,
> it will always be defined to find what a program/state means,
> while the instantiation tactic need not always succeed.

That doesn't deal with the problem. It just doesn't come up
when you apply the semantic function to a concrete represented
object. Whether representations go from abstract to concrete
or the other way around that problem is still there and unaffected.

> Surely, when we try to execute an operation that
> overflows from the representation,
> this should be formalized, and usually detected,
> and an escape mechanism used to recover the system in some way.
> Of course, we are better off when we can *prove* that the
> overflow won't happen, or at least not in the 10% of code
> that gets executed 90% of time...

Of course I agree with the importance of handling the "out of memory"
problem by proving it out of existance. (And of course, it won't be easy.)

[cut, ok for local versus global morphisms]

> >> * Hence, the design process of refining representations
> >>  is an operation that, contrarily to
> >>  composition of simpler known objects into new more complex ones,
> >>  is *contravariant*, not covariant, with computation.
> >
> > Oops, covariant, contravariant, what do these mean ? Does one ever know
> > enough mathematics ? :) Are these worth learning ?
> >
> Yes these are worth learning if you're doing any type theory.
> When you have two Universes each made of sets and morphisms between sets,
> then a covariant functor from one universe to the other is
> a metamorphisms that maps sets to sets, morphisms to morphisms,
> and conserves the relations between sets and morphisms.
> A contravariant functor instead changes the direction of the morphisms.
>    For instance, consider the arrow operator -> such that A->B
> is the type of functions from type A to type B
> from the Universe of types with type inclusions as morphisms to Itself.
> If B' is a subtype of B,
> then any function in A->B' is also trivially in A->B,
> so that A->B' is a subtype of A->B;
> however, we conversely obtain that if A' is a subtype of A,
> then a function from A to B is trivially a function from A' to B,
> so that A'->B is a *supertype* of A->B.
> Hence the arrow operator is covariant in B and contravariant in A!

Ok, I remember having seen that use of covariant and contravariant
in one of my courses.

> This is inheritance in OO languages is NOT some kind of subtyping,
> because the arrow is covariant with inheritance, not with subtyping.
> Hence, all the "OO" methodologies that will try to achieve subtyping
> through inheritance are fundamentally flawed!

Here you lost me completely. I know that inheritance isn't subtyping
but I don't see the connection to co- or contra- variance.

>    If SIC: C->I is a semantic function
> from concrete universe C to intermediate universe I,
> and SAI: I->A from I to abstract universe A,
> with corresponding tactics TIA: A+>I and TCI: I+>C (partial functions)
> then SAC = SAI o SIC : c-> SAI(SIC(c)) is the semantic function from
> C to A while the corresponding tactic is TCI o TIA.
> Hence, tactics are contravariant with semantic functions.
> The way we refine representations is contravariant to the way
> we compute the meaning of a calculus.

Well, all I see here is that inverse function are composed in the
opposite order. The only connection to contravariance that's left
in my mind is the vague concept of "the opposite direction".

> Refining representations is going from higher-level objects
> to lower-level representations;

Yes. Although your defining the inverse mapping at the same time.

> Computing a value is going from lower-level objects to Her-L ones.

Disagreement or misunderstanding here. To me computation is restricted
to one level, which can be high or low, but in no sense do computation
"go" from on level to another.

> Traditional programming only allows the later.
> Reflective programming also allows the former.
> Screwy Traditional programming will introduce lots of unsafety
> doing the later (e.g. overflows in integers, pointers, and memory allocation
> go wild and undetected in C or ADA until the rocket explodes).
> Screwy Reflective programming will introduce lots of unsafety
> doing the later (e.g. semantics is not guaranteed to be conserved
> by reflective operations in Scheme, LISP (CLOS), Smalltalk).
> 
> >> * Up to now, for reasons of easier computability,
> >>  people have priviledged covariant design,
> >>  and tried to artificially apply it to representation,
> >>  whereas we can only grossly approximate the inverse
> >>  of the contravariant function with covariant constructs.
> >
> > Of course I don't understand this...
> >
> Yeah. See above Traditional programming:
> you build HerL obj from LerL ones, which is covariant w/ evaluation.
> People developing "OO" methodologies et al
> have tried to keep their design covariant w/ evaluation and it sucks.
> If you define a representation by the instantiation tactic,
> you also only obtain an approximation of an inverse of the semantic function.

Although I really don't see how you could consider programming styles as
covariant or contravariant, I'm pretty sure you're seing too much in the choice
of what a representation is. If there is such a thing as covariant design, it
isn't forced on you because you represent representation by mappings from
abstract to concrete. In fact the most general way of representing
representations (as relations) completely evades the debate since it's
not a function from abstract to concrete and not a function from concrete
to abstract, just a relation where the order of arguements is a purely
syntactic issue.

[cut]

> >> * Representation as concrete->abstract morphism makes many things easier.
> >>  But that's only a better starting point,
> >>  and doesn't solve trivially solve any of the problems you pose
> >>  after page 5.
> >
> > Yes, exactly.
>    But it *DOES* solve many other problems you have *before* page 5:
> way to formally verify co-satisfiability, to manage overflows, etc.

I disagree for the previously stated reasons.

>    Now, we *can* solve the problems of page 5
> independently of our starting from my point of view or not:
> if you want that a function work
> on variable representations of the argument,
> then consider that the abstract function works on the abstract argument,
> and that a *representation of the function* does a representation of work
> on the representation of the argument.

Yes.

> Hence, to different representations of the argument
> will correspond different representations of the function.

Or the same, as I was suggesting, if the represented function can
handle the different representations dynamically.

> Surely, building these representations
> can be done statically or dynamically by meta-functions,
> that can or not be specialized with the given function, etc.

> My speech was reported indefinitely as I'm in Nice while the
> people for the speech are in Paris :( :( :(

Oh.

On a different note: I used to think we should define the HLL first
and choose a logic later but these days I tend to think the best way
to build TUNES would be to adopt a logic and theory of dynamic systems
(as this is what a computer and its environement are) and start to
express low-level data structures and programs in that theory and use
it to prove the programs correct (manually or with a computer tool
(which we build quickly or which we obtain from the shelf (although
none may match our logic, I'd like to discuss that))). Then we would
work our way up in a proven way until we manage to include all the
functionality we want, including (and preferably starting with) the
proved proving tools which we can then use to check the proofs of
everything done so far to increase our confidence.

This would give us a complete system. Its internals won't all be
expressed in the presumably better programming constructs which were
introduced near the end. So we might want to bring these parts up to
date for reflective reasons (although considerable reflexivity will
already be acheived before that step).

What do you think ?

I just happen to be doing my Master's thesis about the first step
(the logic and theory, well some aspects of it). 

What kind of logic/theory should we use in TUNES ?

My feeling is that most logics/theories I know are pretty bad.  I
think that typed theories are a pain because they make assumtions like
"all types are disjoint" and/or "all function map one type to another"
(and of course there is no type that includes everything). I'd love
feedback on that. My guess is that they have types because the
assumptions in types provide a computationally efficient way of
proving things (about the safety of programs, in ML for example).
There is a cost in ease of use however (you have to hack around
limitation) and I'd think that the above mentionned proofs could be
done by stating the assumptions whenever want to assume them and using
other techniques when we don't.

I looked at set theory as a potential solution to this problem but
I don't like the axioms I've seen. If I can think of the universe
as a set when I define the logic, I would expect the set of every
set to exist. This may not seem very important but I think it is.
If I want to represent predicates by sets, I need the set of every
set to represent the predicate that always answers "true". And I
surely want that predicate to exist. I know this has puzzled
mathematicians for a long time since Russell's paradox but I'm
not really satisfied with the current solution and I've been
audaciously trying to work out a better set of axioms. I'd love
to ear of nice sets of axioms if you know of any.

If other logics/theories look promissing I'd love to hear about
them.

Patrick