type rewrapping and data hiding; multi-typing?
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.
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.