High Order Function with Type Parameter

[keean]

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.

[arielb1]

@shelby3

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;
    t.reset();
    assert!(t.read() > 0);
}

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

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.

[keean]

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

[arielb1]

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

[keean]

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.

[shelby3]

@keean

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

[keean]

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

[shelby3]

@keean

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.

[keean]

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 ?

[shelby3]

@keean

I don't see that?

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

@keean

How do you prevent NatPos being initialised with a value of Natural.0 ?

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.

[keean]

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.

[shelby3]

@keean

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.

Your 4 trait example avoided it. My proposal avoids it. Please review the thread. This is getting noisy.

[keean]

Please provide code, or some hard evidence. I don't see anything that would avoid it, and it seems to me like you have misunderstood the issue.

[shelby3]

@keean

Please provide code, or some hard evidence. I don't see anything that would avoid it, and it seems to me like you have misunderstood the issue.

You provided the 4 trait example which doesn't have any unsafety. Did you forget your own code???

[keean]

I mean an example of how you avoid this with intersection types (I mean't I don't see anything about intersection types that would avoid it, sorry for omitting the context). If you are proposing intersection types solve the issue, I would like to see how. Ceylon has first class intersection types, you could try that?

What is the intersection of a Natural and a Positive ?

[shelby3]

@keean

I mean an example of how you avoid this with intersection types. If you are proposing intersection types solve the issue, I would like to see how. Ceylon has first class intersection types, you could try that?

What is the intersection of a Natural and a Positive ?

I already explained this:

@shelby3

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.

@keean

The answer is Natural /\ Positive = Positive

@shelby3

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.

Afaics, Ceylon won't work for my designs because it doesn't support typeclasses and instead offers the anti-pattern of subclassing. I anticipate this will become more clear as I will try to explain how I think the design patterns for first-class genericity must be handled with a global dictionary hashtable.

[keean]

The answer is Natural /\ Positive = Positive

If you want tagged elements, use an enum?

[shelby3]

@keean

If you want tagged elements, use an enum?

Afaics, insufficient because it is not first-class. We will get into why in the other linked thread.

Please review what I have already written upthread. I believe I have already explained why my proposal is as safe as the 4 trait boilerplate and it only requires 2 traits. I will be showing in the other thread why I think composability can not be obtained without first-class intersections and unions.

[keean]

With an intersection you can only apply operations to the intersection that you can apply to both types in the intersection. You cannot recover the individual types. An intersection is effectively a conjunction, and its is the same as '+' on traits.

I am not sure I agree the 4 traits is boilerplate, as you are implementing the same number of functions, just instead of pairing them in traits, each one has its own. We want to implement things in the most generic context to promote reuse, so separating the traits is more generic as we can re-use the traits in more contexts. So there will be less repetition in the collection library an in user code as a whole.

We have discussed so many issues, its difficult to find the precise bit you are referring to. Could you write a concise stand alone explanation without conflating any other discussion points or issues.

[shelby3]

@keean

An intersection is effectively a conjunction, and its is the same as '+' on traits.

...

@shelby3

Afaics, insufficient because it is not first-class. We will get into why in the other linked thread.

Please review what I have already written upthread. I believe I have already explained why my proposal is as safe as the 4 trait boilerplate and it only requires 2 traits. I will be showing in the other thread why I think composability can not be obtained without first-class intersections and unions.

Afaics, we are talking past each other. You appear to be ignoring the points I have already explained.

@keean

I am not sure I agree the 4 traits is boilerplate, as you are implementing the same number of functions, just instead of pairing them in traits, each one has its own. We want to implement things in the most generic context to promote reuse, so separating the traits is more generic as we can re-use the traits in more contexts. So there will be less repetition in the collection library an in user code as a whole.

We have discussed so many issues, its difficult to find the precise bit you are referring to. Could you write a concise stand alone explanation without conflating any other discussion points or issues.

I can understand why you may think that until there has been a holistic elucidation. Perhaps it is best we explore some more the discussion in the other threads first, so I have all the issues nailed down that I want to blog about. Is that an acceptable path forward in our discussion?

Doing it piecemeal here is going to cause confusion. It is not that I don't want to answer you directly, but I also don't want to write a 3 page comment here. And when I try to reply by referencing prior comments, it appears that the point ends up confused.

The thread has gone on many twists and turns and my understanding changed as we proceeded. So it may be unclear where our respective understandings are now. I think it is best to blog about the complete solution I am contemplating once I am sure I have worked through all the details, which is what I am discussing in the other related threads.