First Class Representations

[Francois-Rene Rideau]

> 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.
Whatever convention you use to direct your representation,
there is a complete dissymetry between the abstract and concrete space,
so that when you say "concrete space A represents abstract space B",
you don't generally have "B represents A".
The semantic function must be a computable morphism
so we can use the representation,
while the instantiation tactic needn't be given at the same time,
needn't be a morphism, and needn't be computable,
without hampering us to use the 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.
But I'm NOT considering multi-valued functions. See below.

> 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.
Which cases don't I handle?
What is a morphism to you when it's multivalued?
Ain't it more cleanly done with a functional backend morphism
that would collapse your multiple values into one?
My guess is that only those specific relations for which
such backend exist do qualify as relational morphism.
If my guess is true, then, my way to express representations
is as expressive as yours, while being simpler and cleaner.
To see whether it is, we need a more precise definition
for a functional or relational morphism.

> 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.
What bijection is it?
I see an injection from predicates on the abstract space
to predicates on the concrete space, but no bijection!

> 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.
Depends on how deep you represent things:
are you just representing separate objects and functions,
or are you representing the process of computing the function?
Those are different matters;
of course, you'll want to express the more complex latter
using the simpler former...

> So the usual concept of morphism isn't what we want here.
Yes it is. Just not always a morphism
to the abstract space of single objects,
but, when we go deep into the system,
to a space of "environments" of abstract objects.

> We want the relation from type to state space, as usual,
Well, I'll say semantic function from concrete state space
to space of environments of abstract objects.

> plus a description of how to implement the functions of the type by
> programming the dynamic system.
Uh? If you want the functions to be reified in the representation space,
then do reify them in the abstract state, too,
and use the usual representation mechanism.

>>> 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).
That is, representations founded on the physical universe
(actually, we'll most often settle upon the already founded
logical universe of implemented computer systems).

>> 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),
Granted.

> but then you'd have to make it multi-valued to handle
> ambiguous or imprecise representations.
No. Because, I either
1) I'll never need to disambiguate, hence,
 the real abstract object is not that space I first chose,
 but an even more abstract space,
 with a semantic function that will remove ambiguities, or
2) I'll need to disambiguate,
 and will do it by using currently hidden/implicit information,
 which I should show/make explicit in the real representation space.

examples:
1) after compiling a C program, I can't distinguish between
 the number 1, and the enum one from << enum { zero, one }; >>.
 Who cares? The compiled object does not represent the C source
 in the space of valid C source programs,
 but the program represented by the C source in a more abstract space.
2a) in a cell of the GC'ed memory lies the raw data representing number 1.
 Does it represent a number? a character? an index in some enumerated type?
 something else? Well, even though the GC mightn't disambiguate,
 either we're in case 1, or a structure somewhere is describing the given
 cell so a *global* analysis of the memory would tell what this *local*
 analysis didn't.
2b) such a handle to some external object might mean lots of thing;
 to disambiguate, we must formally include the external object into the
 representation space so we can reason about it, even though the
 real external object might be much too large; if we are to prove
 something, the few required known properties of the external object
 should be ok.

> 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.
Relations being reversible make it not obvious what represents what,
while being a representation is something strongly not reversible to me:
when my GCed memory represents my program's state,
I don't think that my program's state represents the state of the GC.
Abstract to me means less dependent on concrete contingencies.
Functions are more suited to represent representations.

> Whatever order you chose, there is no difference in expressivity
> or capability in the resulting programming system.
>
Because I use *functions*, not *relations*, and require
the semantic function, not the instantiation tactic,
to be *computable* (or rather, computably approximable?),
for the representation to be *effective*,
there *is* a specific order.


>> 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.
The Semantic function S is a single-valued morphism
that characterizes the representation.
The instantiation tactic I is not a morphism, is single-valued,
and can dynamically vary for a same representation.
Just that it should be a (partial) inverse of the semantic function,
that is, if I(x) is defined, then S(I(x)) is defined and S(I(x))=x.
[Actually, the "real" instantiation function i,
will take a (syntactical) representation t of x as a parameter
with semantic function s: s(t)=x,
and we require that if i(t)=y then S(i(t))=s(t);
again, i is not a morphism; i represents I]
Again, the aim of all this is to have *dynamically computable* functions
as semantic function and instantiation tactic.
Arbitrary relations just can't provide dynamical computability
and/or not in any reasonable time.

> 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.
>
Let's settle our argument: surely, if our definitions are equivalent
up to mathematical transformations, there is no mathematical reason
to prefer one.
My point is that they are not equivalent up to *computable* transformations,
that semantic functions are a "right" way to describe things,
while arbitrary relations lead to uncomputable representations,
unless you constrain your relations in such a way to make
the semantic function explicit,
in which case it is but a contrived way to do the same as I.
I admit I didn't give convincing evidence
that your definition be strictly more complex,
but it seems (perhaps wrongly) obvious to me that
mine is at least as simple.
If we still disagree after this message,
then we'll have to go formal to see who's right (if any of us).

[about consequences of computations "overflowing" the representation]
>> And to Ariane V exploding...
>
> Is this just an example of a possible consequence or did this
> really happen because of such a problem ?
>
It really did happen because of such a problem: out of memory in ADA.
Billion dollars for the pocket of french taxpayers for /dev/null return.
Better dig holes and fill them.

>> 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.
>
Well, the semantic function being given,
the problem of not "overflowing" during a computation becomes that
of being sure that the instantiation function will not fail
when trying to instantiate a representation of a "further step"
of the computation. This cleanly pinpoints the problem,
and helps separate proofs into "the program does nothing but what we want"
part with the semantic function, and "the program actually completes
computation" part with the instantiation tactic.
In an dynamic/interactive system, the instantiation tactic may "escape"
when it detects that an overflow would happen,
so that the system would take appropriate measures.


[Using co-/contra- variance to prove that inheritance != 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.
>
Well, covariance is a way to prove the difference
(type of generic functions w/ member methods is
covariant w/ inheritance in parameters,
contravariant w/ subtyping in parameters).
People trying to have them be the same are going nowhere
(all the mainstream "OO" guys).
Anyhow, this is getting out of our main point.
For a language that does both inheritance and subtyping
without getting get mixed up, see OCAML.
I think that providing multiple representations
in a reflectively typed language
of can solve the problem of having both clean subtyping
and efficient ad-hoc methods.

[about semantic functions being contravariant to instantiation tactics]
> 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".
>
Yes. Computations take (the values of) simple objects and combine them
into (the values of) more complex objects.
Refining representations goes the other way round.

>> Refining representations is going from higher-level objects
>> to lower-level representations;
>
> Yes. Although your defining the inverse mapping at the same time.
>
Not "at the same time".
The instantiation tactics can be dynamically
defined and modified afterwards.
The important point is that we needn't be statically founded
on ground object anymore, as with traditional computation,
and we can develop programs in both directions,
with our interacting with the system at all times,
instead of the system giving us feedback only from
our current development only when in its current state,
it is completely statically founded.

>> 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.
>
The computation *is* semantic evaluation.
It is covariant w/ evaluation of semantic functions.
You strip information about the concrete computation path,
to keep only the result, a more abstract information.

>> 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).
There exists non-screwy traditional programming
(well, I'm not so sure after all;
does any actual well-typed language recover cleanly from memory overflow?).
Let us build non-screwy reflective programming.

>>>> * 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,
>
Perhaps saying "covariant with the way structures build up" would be
more appropriate. Traditional programming will have you combine information
into more complex structures, not let you refine structures being used.
You must build your new features from the old ones,
and cannot build the old from the new ones
(at least not dynamically in non-reflective languages,
and not while preserving meaning in current screwy reflective languages).

> I'm pretty sure you're seing too much in the choice
> of what a representation is.
No. My problems are not related to the extrinsic syntax choosen,
but to intrinsic properties of representations.

> 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.
Surely not. However, see computability of representations above.

> 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.
No, because whenever you change the order of arguments in your syntax,
this also changes the order in which evaluation of expressions takes place,
so covariance/contravariance of design stays the same.


>> 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.
>
Well, you should make a difference between
an abstract function, and
a meta-function that gets a representation as argument;
they are not on the same representation level,
the second being especially more concrete
when used as a representation of the former.


> 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 ?
>
This might be a good plan to develop the HLL
(independently from the LLL effort to begin with).
Unhappily I have very little space time currently,
so if I'm to do that alone, it will be long,
unless I can manage to convince my professors to have me
work on it for my studies.

> I just happen to be doing my Master's thesis about the first step
> (the logic and theory, well some aspects of it).
>
Great. You're lucky you can do your official work and personal interest
at the same time. I couldn't manage to have this luck (yet).

> What kind of logic/theory should we use in TUNES ?
>
I'm all for a reflective variant of Coq,
where the Curry-Howard isomorphism between types and predicates
would be used to identify proof tactics as a particular case
of instantiation tactics;
reflection would allow the system to dynamically absorb
all that must be statically built into Coq.

> My feeling is that most logics/theories I know are pretty bad.
>
Ahem. In France, students in Computer Science (theory) "informatique"
as opposed to students in Computer Technology (practice)
"informatique appliquee" learn a lot of semantics,
which is a Good Thing(tm) to me,
even though I often dislike the way it's done.

> 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 see nothing wrong with type disjointness.
What I see wrong is lack of expressiveness in types.

What is a type? It is present information that constrains the future.
Untyped languages like C have no locally typed objects, only a global state.
Trivially typed languages like LISP (often traditionally but wrongly
called dynamically typed) do have locally typed objects, but only one type
for them.
Statically typed languages do have more than one type,
but all typing information must be statically known at compile time.
Real dynamically typed languages (that might be called reflectively typed,
to distinguish them from the above-mentionned trivially typed languages)
do have a non-trivial type structure, so that implicit information can be
given on objects that constrain them for all their future life;
but this type information can be obtained from non-statically-known
computations (e.g. complicated computations from external input,
including possibly user interaction);
this means that representations of types can be computed as objects
and absorbed by the system, so that the system is reflective.
Very few known languages are such (the only one I know is Napier88,
and its source-string-based reflectivity is dirty to me).

> 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.
>
Whatever you do, you can't escape troublen
if a system can talk about "itself" with enough expressiveness.
Of course, a system can very well talk about *another* "lesser" system.
The solution is to build a hierarchy of systems
each talking about some lesser ones.
Again, some do it with a static hierarchy of systems (see Coq),
so you are limited again.
A truely reflective system would do it w/ a dynamic hierarchy,
where you can always find a common meta-system for
whatever dynamically computed "set" of systems you have.

Ok. Enough for now.
I should really try to sum up my ideas and
write an "official" article [unless you're convinced and you do]
about reflectivity.
Thanks for allowing me to develop my ideas.
Please continue to make all appropriate objections.

== Fare' -- rideau@ens.fr -- Franc,ois-Rene' Rideau -- DDa(.ng-Vu~ Ba^n ==
Join the TUNES project for a computing system based on computing freedom !
                TUNES is a Useful, Not Expedient System
URL: "http://www.eleves.ens.fr:8080/home/rideau/Tunes/"