type rewrapping and data hiding; multi-typing?

[gusl]

I was just looking back at my proposal for formalizing basic Statistics, and chrisamaphone's twelfing.

There, I treated "Random Variable" (RV) as a basic type, which you never go inside. I think this was the right choice for the purposes of that formalization: seeing RV as (Real -> Real) isn't helpful, and loses important information.
I want to think of RV as a type that contains a (Real -> Real) (i.e. its pdf): a RV has a pdf (rather than "is"), though I can sorta imagine such choices being somewhat arbitrary in some situations. (Speaking of metonymy...)

But there are cases where you'd want to allow this. You may have a value x and you want to talk about the probability of various RVs being exactly x. This would require accessing the pdf object. No problem here...

The alternative is for RV to be an alias for (Real -> Real). This would be a transparent / glass-box way to model that, and amounts to saying that an RV is its pdf.

---

Now, since math is all about metaphors (through which one tries to transfer results), this means that mathematical objects sometimes have multiple meanings (i.e. they simultaneously instantiate multiple structures). In information geometry, for example, distributions are points in a space.

So I want to say that:

p : point.
p : distr.

are both true.

But this won't jibe with normal type systems (AFAIK): since point and distr aren't subtypes of each other, these two statements contradict each other. So we should add information about the context, i.e. the metaphor through which you see the object, as a point or as a distribution.

Something like:

p [prob_theory] : distr.
p [info_geo] : point.

I'm trying to keep identity sacred here, but there might be good reasons to sacrifice it, and instead treat the mapping between metaphors as a bijective function.

Comments

[simrob.livejournal.com]

Refinement types? In that setting, point and distr could both, perhaps, be refinements of the location type, which is what you're really working with here.

[gustavolacerda.livejournal.com]

I still think reasoning inside the metaphor is important. Can you have labeled refinements? i.e. 2 refinement relations in this case, one for each metaphor.

Points also exist in prob_theory. But

p [prob_theory] : point

is a false statement.

The whole point (pardon the pun) is that the type point and its associated methods really model the mathematical concept of "point". It's still the same type when applied across contexts. And sometimes, via mathematical metaphor, you have "points" that "contain" "points".

e.g. we can consider intervals in real line (call this context1) as points in 2D space (call this context2).

So when I say there exist "points" that "contain" "points", I mean:

there exists an object a of type point(context1)
there exists an object b of type point(context2) ... which makes it an interval(context1)
such that b contains a (context1)


(perhaps I should define a bijective function metaphor_from2to1 : type -> type, so that metaphor_from2to1 point returns interval or set).

[gustavolacerda.livejournal.com]

So I think the two contexts here (i.e. two pairs of < type-of , subtype-of > relations) could be implemented by having two type systems in parallel.

Is that ever done?