Generic overload resolution

Kitten has ad-hoc static polymorphism in the form of traits. You can declare a trait with a polymorphic type signature, then define instances with specialisations of that signature:

// Semigroup operation
trait + <T> (T, T -> T)

instance + (Int32, Int32 -> Int32) {
  _::kitten::add_int32
}

instance + (Int64, Int64 -> Int64) {
  …
}
…

This is checked with the standard “generic instance” subtyping relation, in which <T> (T, T -> T)Int32, Int32 -> Int32. But the current compiler assumes that specialisations are fully saturated: if it infers that a particular call to + has type Int32, Int32 -> Int32, then it emits a direct call to the (mangled) name of the instance. I’d like to remove that assumption and allow instances to be generic, that is, partially specialised:

// List concatenation
instance + <T> (List<T>, List<T> -> List<T>) {
  _::kitten::cat
}

// #1: Map union
instance + <K, V> (Map<K, V>, Map<K, V> -> Map<K, V>) {
  …
}

// #2: A more efficient implementation when the keys are strings
instance + <V> (Map<Text, V>, Map<Text, V> -> Map<Text, V>) {
  …
}

But this raises a problem: I want to select the most specific instance that matches a given inferred type. How exactly do you determine that?

That is, for Map<Text, Int32>, #1 and #2 are both valid, but #2 should be preferred because it’s more specific. There are also circumstances in which neither of two types is more specific: if we added an instance #3 for <K> (Map<K, Int32>, Map<K, Int32> -> Map<K, Int32>), then #2 and #3 would be equally good matches, so the programmer would have to resolve the ambiguity with a type signature.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Most specific instance

The method is as follows: first, you need a measure:

cmp: T1 * T2 -> Greater, Equal, Less, Incomparable

Now suppose you have a set of Input of candidates,
Make a set of Output candidates, initially empty.
Move one function from the input to output set.

How it works: the output set maintains an invariant that for every pair of functions in it, they're either equal or incomparable. In other words, the set never contains two functions, one of which is more specialised than the other.

For each input candidate:

  1. If we have a candidate Greater than any one element, we ignore it: the output set already has a more specialised function in it.
  2. If we have a candidate Less than any one element, we have to remove that element from
    the output and add the candidate to the set. But we have to throw out ALL the elements which are Greater than it from the output set.

  3. If the candidate is Equal to any element, we just add it.
  4. If the candidate is Incomparable with ALL elements in the output set,
    we have to add it.

  5. There are no other possibilities because of the invariant.

The result: if empty, you have an empty input.
If the set has one function in it, it is the most specialised.
if the set has two functions in it, either they're incomparable
or they're equal. For three or more this is true pairwise,
in any case there is no most specialised function.

Tuples

I like that you favor tuples over currying in Kitten.

Meet semilattice

Doesn't this a require a meet semilattice, as in Fortress's multimethod overloading? The rules are summarized thusly:

Given a class table T , a set D of generic function declarations for T , and a function name f, the set Df is valid (or is a valid overloading) if it satisfies the following three rules:

  1. No Duplicates Rule For every d1, d2 ∈ Df , if d1 ⊆ d2 and d2 ⊆ d1 then d1 = d2.
  2. Meet Rule For every d1, d2 ∈ Df , there exists a declaration d0 ∈ Df (possibly d1 or d2) such that, d0 ⊆ d1 and d0 ⊆ d2 and d0 is applicable to any type T ∈ T to which both d1 and d2 are applicable.
  3. Return Type Rule For every d1, d2 ∈ Df with d1 ⊆ d2, and every type T ≠ Bottom such that d1 ∈ Df (T), if an instance f S2 :T2 of d2 is applicable to T, then there is an instance f S1 :T1 of d1 that is applicable to T with T1

Fortress similarly uses tuples for arguments, so this should map naturally to Kitten's semantics.

Multiple dispatch is harder

The Fortress rules are stronger than what's needed for overload resolution, I think, because Fortress needs to statically decide that dispatch cover all cases that might arise dynamically. Whereas overloading just needs to pick a most specific match for the case in question.

I don't think much changes

Perhaps, but starting from this general basis, I don't think much changes actually. Kitten's "subtyping" relation would just be simpler than Fortress's, consisting only of "types are more specific than type schemas, and tuple T1 ⊆ T2 if every pairwise element of T1 ⊆ T2". I think everything else falls out naturally.

Fortress does take the approach that ambiguous definitions require a disambiguating definition that's more specific than both, but I don't see why you couldn't do as the original post suggested and simply require a type annotation to pick the one you want. I personally prefer the disambiguating approach, but to each their own.

Coverage

Not sure why one would do that. The reason is you can guarantee coverage by simply making the most general case do "Error, dispatch failed". This is a common trick in C++, to make an abstract class concrete by defining an otherwise pure virtual to just throw an exception.

It's not coverage that's the issue. The hard thing is failing to find a most specialised instance. I do not see how separately compiled and linked derived classes can allow this to happen: there's no way to check (until link time). Since an OO language that doesn't support loading DLL's dynamically at run time is a waste of time***, it follows you just cannot maintain any assurances unless you examine each run time DLL load for consistency with the environment its loaded into, at the time it is loaded, which is run time. So you get a run time error, unavoidably, although it is earlier than the error you'd get on an actual dispatch. However there's no way to know if the error generating dispatch actually happens, so the early diagnostic may not be a good idea.

*** the reason I say this is that run time loading is the primary benefit of dynamic dispatch, that is, support for plugins. If you didn't want this, there's no reason to bother with an OO language, just use an statically typed language (FPL or not).

Orthogonal

I think OO and static/dynamic typing are orthogonal concepts. I don't think OO and dynamic loading should be conflated. Dynamic loading only requires a typed interface with optionally some kind of subsumption, which could be a module, with parametrically polymorphic subsumption

Orthogonal

I don't think they're orthogonal: if OO were a valid general paradigm, yes. But it isn't. It's significant advantage is dynamic dispatch. That's also why it isn't a general paradigm (because linear dispatch doesn't work in general). So if you're using OO, the reason has to be because of the dynamics.

FPL's tend to have only constant dispatch, eg for variant types (finite cases only). With say C++ virtual function dispatch this increases to linear dispatch, meaning covariant down an unbounded depth derived class chain.

Since conventional programs are bounded, there is never any need for such linear dispatch in them. So the ONLY use for OO is if the collection of derived classes is unbounded, which can be done on modern systems with dynamic loading.

It's true that other machinery can also work with dynamic loading (type classes, Ocaml modules, etc). The point is OO is broken, so the only excuse for using it is to leverage the dispatch machinery to support dynamic loading.

Objects

I think there is nothing wrong with simple objects. Starting from coroutines/cofunctions, we realise that an object is a recursive cofunction with a single yield, that accepts a message and returns a result. As this is a very common case we can introduce special syntax for it, where we have a set of private object data (the values passed recursively by the cofunction to itself) and a set of methods (the messages and their responses). This all seems perfectly fine and well founded to me, and offers state encapsulation, so we can have objects like an io-stream with read and write methods for various datatypes.

We have three ways to handle state (and IO):

- the change in state results in a change in the identity of the value (even if you cannot access the actual state inside) this leads to having to thread the state through the program, either by passing the "world" to every function that does IO or by using a monad (Haskell)

- state is global, and implicitly accessed by special functions (ML)

- a change in state does not result in a change in the identity of the value. This avoids the need for threading, and avoids global state, as the state is contained in the value. (Objects)

If we want to not have to thread the state, but we also do not want global state, then we have an object.

Agree

I agree, there's nothing wrong with objects. It's Object *Orientation* that's the problem.

I actually think that you need general co-routines to control invert objects with multiple methods. Your idea involves a single communication channel with a sum type which is still somewhat passive. Definitely worth doing to see how it pans out.

However I am thinking now, there is a very strong space/time duality. Functions access spatial data, aka products. FPL's can't correctly handle sum types any more than partial functions or streams, coroutines can because they're temporal (but dually can't handle products). Of course both systems can build models of these things.

Switching systems from F to CoF is action. A system with both models (space/time continuum) is action oriented.

I really don't fully understand this yet, however the temporal calculus clearly deals with continuations.

Serialisation

To avoid problems with effect order from methods, the object should have a single communication channel that serialises the requests.

By having a single thread of control these channels do not ever have to queue messages, so the cofunction approach transfers control to the object when you make a request and transfers it back when the response is yielded. The cofunction in the object is simply a loop that passes itself the state at the end of the previous method call so it is available to the next message call. In this way state is threaded inside the cofunction in a "functional" way, there are no mutable variables.

We end up with a finite state machine like model where state transitions are pure functions that have as their inputs the current object state and the method arguments, and output the new state and the method result.

Effect order

I have no idea how you arrive at the conclusion that effect order requires a single channel. A Felix coroutine can have any number of channels. Any effects between I/O operations by that coroutine are determined by the coroutine's control logic.

For example if you do read A, read B, write C, write D and loop back, then any effects between the I/O operations occur at particular points in the control flow between particular I/O operations.

In Felix at least, there is indeterminacy *between* communicating coroutines. For example if routine 1 reads A, does effect E, then reads B, and routine 2 writes A, then does effect F, then writes B, then we do not know which of E and F occurs first. With coroutines, it could be E then F, or F then E, but it will be one of these alternatives. If We do E1,E2 instead of E, and F1, F2 instead of F, then we have E1,E2,F1,F2 or F1,F2,E1,E2 but we cannot have E1,F1,E2,F2 etc.

I suspect you're missing the point of cofunctional code looking for functional machinery. The whole point here is that functional programming is only half the story and the functional "paradigm" is completely broken until one marries it with cofunctions.

Indeed, functional programming is very weak. It cannot handle partial functions, streams, or sum types. And your model is using a sum type for messages. Coroutines handle partial functions, streams and sums correctly but can't handle products.

FP is basically a purely spatial concept. Just replace the badly named "constructor" word with "locator" and you have a notion of objects in space which just exist: immutable and persistent. They are not created and not destroyed. This is the set theoretic model of reality. For FP you have to throw in indirection. This model is global.

The dual of this spatial world is temporal. This is a local model. It is populated by events, not objects.

The spatial world can *model* sum types (tag, value) pair but this is not a sum, only a model of a sum. Similarly, in the temporal world you can model a product as an event sequence, but this is not a product, only a model of a product.

You see the spatial world is "purely declarative". It is a description of space. There is no motion, no action, and no way to do anything. The spatial world is there to find and remember stuff. The temporal world has no memory. It is all instant actions.

So the point is, you don't want to have cofunctions doing stuff in a functional way because the whole point is that the functional way is an idiot savant: it knows everything but can never make a decision. The whole point of the dual space is that it is imperative. It is driven.

So what we need is BOTH functional and cofunctional, and you can't get that until you recognise that you have to abandon the notions of functional programming in their spatial form, and replace them with temporal notions. More precisely you need both, and the question becomes how to integrate them.

I can show you how. In Felix a pipeline can be constructed with a source at one end, a chain of transducers, and a sink at the other. The transducers are cofunctional. The source is a bridge from space to time. It is a coroutine passed a list as a parameter, which then writes the list down its output channel.

I call that a LIFT. We're lifting from space to time. From an inductive data type to a coinductive one. From a list to a stream.

Now at the end, the sink is constructed by passing a pointer to a mutable variable. It reads results and it builds a list of them in that variable. We are converting from time to space. From coinductive stream to an inductive list. I call this a DROP. We're dropping back from time to space.

But there's a PROBLEM! The stream has no end. When there is no more data coming down the pipeline the sink just hangs forever. There is no way for the function which just launched the pipeline to ever get a result.

The solution is that the whole pipeline is run AS A FUNCTION. The function starts the coroutine system and waits until it is no longer active and returns. At that point the completed results of the list processing are stored in the variable we passed to the sink.

So this is the simplest form of nontrivial bridge. We go from functional to cofunctional and then back. The other direction is trivial: coroutines can call functions in the traditional way.

The serialisation of message passing on a single channel using a sum type is, in general WRONG. More precisely it is a special case of an inert object passively responding to messages. The reason it is wrong is that it provides no support for PROTOCOLS.

A protocol is a requirement actions occur in some order (not necessarily determinate). For example you have to open a file before doing I/O and you can't do I/O after closing it. Obviously the only way to manage that with your machinery is dynamically. What we want is STATIC CHECKING.

The way to do that with a coroutine would be a channel to open the file, one to do I/O operations, and one to close. This system GUARANTEES you follow the protocol! If you try to do I/O before opening, your request is ignored and you're deadlocked!

Obviously we don't want to be deadlocked. So we need to encode the protocol the coroutine enforces in what you might call its "effect type" that the order in which is reads and writes channels. If the client using it interfaces with the wrong event type we should get a compile time error. I don't yet know how to do this. However it HAS been done for a more complex system, namely Hoares CSP.

More than one thread

The reason effect order must be serialised is that otherwise there can be two threads of control in the object at the same time, and then assumptions about the state fail, because the transactions on the state cannot be serialised.

Edit: note that this is not about the object having access to other channels, you can pass many cofunctions into an object method, but because there is only one thread the calls "out" from the object are always sequential. The issue is if there are two command channels into an object then it is possible for two different threads to call two different methods at the same time.

Fortress

AFAIK Fortress implement standard overloading rules except it does the overload resolution at run time. Unlike Felix and GHC, but like C++, Fortress supports both polymorphic subsumtion AND subtyping. It has to because typical type construction is nominal, as it's an OO language of the traditional kind.

The run time dispatch by the same rules used in static languages is VERY clever, IMHO.