High Order Function with Type Parameter

I by now understand your (and others') point is that attaining the nominal (not first-class) intersection trait NatPos : Nat + Pos by implementing Natural for Pos is local violation of invariants at the declaration imp Pos for Natural.

My point can remain that with a first-class intersection Natural /\ Positive, there is no motivation to unknowingly implement a Natural for a Pos as I did in my first "proof" of unsafety wherein I obfuscated to myself that a u32 only enforces Natural data type semantics on itself (which is by now obvious as you pointed out by the fact that an incorrectly implemented NatPos can refer to constructed instance containing the value 0).

Given my idea for first-class intersections and unions, afaics it requires de-structuring (or dynamically dispatching) a disjunction to a type interface at runtime and the types have to be tagged.

If given it is true my assertion that the immutability combined with encapsulation of construction make all types have disjoint invariants w.r.t. to the state of the instance of the type, a Natural /\ Positive is sound because there will be no way to write a 0 value to a Positive and no way to have a Pos trait on Natural /\ Positive because not only would Pos would not be implemented for a Natural but there is no motivation to mistakenly do so.

In short, with first-class intersections, there is no need to formulate that 4 trait granularity that was necessary to correctly implement a NatPos. The programmer doesn't have to get that clever, because the composability would be in the type system first-class and reusable. Don't Repeat Yourself (DRY) is an important design goal.

Natural /\ Positive = Positive

The intersection of a set and a subset is simply the subset. So you may as well have Box<Positive> as that is the intersection of Natural and Positive.

Note: My last implementation in Rust only had two traits Nat and Pos, not four.


How is that relevant to my post you replied to?

What is a Box in this context? I do not understand.

The markup removed the angle brackets, it should have been Box<Positive>

Moreover the immutability isn't necessary. The problem at-hand arose from forming a shared interface for the trait NatPos because we don't have first-class intersections with tagged instances. Afair, the research paper was assuming that the types were untagged and thus we could write to an instance as a Nat and read from it as Pos. Tagging forces de-structuring that disallows doing that.

My real motivation has been first-class intersections and unions as I think they will be necessary for composability, but I will want to discuss that in a different thread.

Do you mean unions? Rust Has tagged unions which are created using enum. I am not sure a tagged intersection is meaningful. The intersection of two types is that which is common to both. If all types are disjoint, then the intersections are all going to be the empty-set.

Can we delve into that in the other thread instead?

I am thinking enum is not first-class disjunction but perhaps I am mistaken. And that doesn't provide first-class intersections in any case.

I want to compare design paradigms such as what you were doing with OOHaskell. There is a lot I need to learn.

Natural /\ Positive is not the empty set. Where we have arrived is they are not disjoint and the problem at-hand is not requiring the programmer to conceive of 4 traits to be able to write NatPos instead of Natural /\ Positive. The utility is Don't Repeat Yourself (DRY) and greater degrees-of-freedom.

Ostensibly (possibly but I could be mistaken) you dismiss the utility of Don't Repeat Yourself (aka no boilerplate), greater degrees-of-freedom of composability, and not motivating obfuscated errors such as imp Pos for SomeData where SomeData was really u32 which is really Natural.

There are composability and DRY benefits to making constructs first-class, e.g. first-class functions where a function is a type and can also be a value any where types and values are allowed.

Not at all, I am a great proponent of DRY, and I highly value composability, and I don't see any evidence that would lead you to conclude that. What made you think that? Because I don't like intersection types? I have tried many programming languages and styles, most if not all claim to help DRY and composability, however the most success I have had is applying the techniques in Elements of Programming. The idea is you only ever need to define an algorithm once (normally using iterators) and this can be applied to any collection of any value. The whole realisation is that code should not be structured around objects and classes, but algorithms and concepts (where a concept is equivalent to a type-class or trait). Maybe it's because I have done a lot of functional programming, but I find this approach much more powerful, yet resulting in simpler code. To me Rust is the best bits of Haskell and C++ in one language. There are some things I would do differently if it were one of my own languages, but it is the kind of thing I have been independently working towards.

Traits offer the best DRY and composability of any language feature, better than classes, better than any form of inheritance. Their fundamental limitation is that there can only be one trait implementation per type, but having programmed with parameterised modules, I still think traits are a better solution.


Implementations can't carry invariants, because everything an implementation function can do a free function outside of that implementation can do too. Invariants go on types and traits.

You might just as well write

pub trait Pos {
    /// always returns a positive value
    fn read(&self) -> u32;
    fn write(&mut self, u32);
pub trait Reset {
    fn reset(&mut self);

pub mod junk {
    use {Pos, Reset};
    pub struct SomeData { x : u32 }
    impl SomeData {
        pub fn one() -> Self { SomeData { x: 1 } }

    impl Pos for SomeData {
            fn read(&self) -> u32 { return self.x; }
            fn write(&mut self, x:u32) {
                assert!(x > 0); self.x = x;

        impl Reset for SomeData {
             fn reset(&mut self) { self.x = 0; }

fn unsound<T>(t: T) where T: Pos + Reset
    let mut t = t;
    assert!(t.read() > 0);

fn main() {
    let to = junk::SomeData::one();

Obviously, the implementation for Reset is not compatible with the implementation for Pos, as it allows you to break the trait invariant. If you want to locally reason about correctness, you can, for example, add an invariant to SomeData that requires its data to be positive - and then Reset would clearly violate that invariant.

The Pos + Reset or PosReset or PosNat or whatever intersection type is a total red herring. Subtrait-to-supertrait coercions are only not possible due to technical reasons involving the layout of vtables, and we are working on changing that - but you can always do the coercion in a trait method.

I really don't get your point here, yes Junk is bad, you have written a bad ADT because it does not enforce its own invariants. You can do this in any language so I don't see your point.

If I write an ADT that correctly implements the invariant checks as a module, and compile it, and give you only the binary interface, you cannot break it. This is what an ADT is :slight_smile:

I must have pressed the wrong response button - I meant to distill @shelby3's examples.

Ah, okay, yes I agree that is the kind of thing that we have been discussing. I would rather approach the discussion by showing a well designed ADT, but it is true in any language I know that if you have privileged access inside the encapsulation you can break the invariants.

The idea of combining the encapsulation with the datatype is a bad one in my opinion because you can no longer create abstract data types, and abstraction is one of the key properties of a high level programming language.

Because your correct solution for NatPos : Nat+Pos in a language without first-class intersections and unions required you to use 4 traits of boilerplate; whereas, as I had already explained upthread that in my proposal with the first-class intersections I can write instead Nat /\ Pos and only 2 traits are needed to attain the same correct semantics and safety. I expounded on other reasons (my replies will be forthcoming at the linked thread).

Well I provided a version with only two traits later on as well.

As I already explained upthread, it has incorrect semantics and is unsafe as you showed that NatPos in that example can be initialized with a value of 0.

I don't see that? Please explain why the semantics are not correct, and why you think the semantics you are proposing are better. How do you prevent NatPos being initialised with a value of Natural.0 ?

Huh ??? You composed that example to show that it was unsafe.

By using your 4 trait example with the encapsulation it has. Or by using my proposal for first-class intersections and unions, then only 2 traits are needed. This is what I have been explaining upthread already many times.

No, I composed that example to show the behaviour was unavoidable If you have a way to avoid it I would like to see it, because neither encapsulation or immutability will fix it. First class intersections will not fix it.