Bayle Shanks's website: proj-oot-ootVariantImplementations

Stuff like quicksort, bubblesort, insertion sort are called 'variant implementations' in Oot because they yield the same results, albeit through different algorithms, and with different complexity characteristics.

In Oot, we also consider things like foldl, foldr, foldl', foldr' to be variant implementations, even though using traditional semantics, these functions have different results (because, when fed certain infinite inputs, some of them terminate in finite time and some do not). What we mean when we say that two functions are 'variant implementations' of the same function (todo what should be the vocab term for what they are variant implementations of? function? surely there is already vocabulary for this stuff in the field of programming languages, perhaps we should find out what it is and reuse it)? What we mean is almost that, when restricted to the domain of finite inputs, and given arbitrarily large resources (time, memory, etc), variant implementations yield the same results.

To make this formal, we need to recognize that (a) we are dealing with higher-order functions which may generate infinite outputs from finite inputs, and (b) variant implementations might have slightly different signatures, for example, you might have one sort implementation that allows you to pass in optional 'hints', and an optional 'debug' flag, and optionally the location of a file in which to write a debug trace, and which optionally returns profiling information in addition to the result, and another implementation with none of these.

X and Y are 'variant implementations of some function F with signatures s' iff (a) s is a subset of both the signature of X, and of the signature of Y, (b) let X_in be any inputs for X which are all finite data or total functions and which cannot be iteratively combined to generate infinite data or partial functions; let Y_in be any inputs for Y with the same property, such that X_in and Y_in are identical when restricted to the inputs mentioned in s; then X(X_in) = Y(Y_in).

vocab: instead of saying 'variant implementations of some function F with signatures s' we could say 'variant implementations of some INTERFACE F with signatures s'. We could distinguish between an 'interface', which prescribes semantics in the above sense, and mere 'signatures'. Note however that this is inconsistent with the usual notion of 'interface' w/r/t ad-hoc polymorphism, e.g. you could have a 'reader' interface on almost anything which has SOME semantics (e.g. you can read from this thing), but not enough to completely define its result when given finite/total input, as with variant implementations.

mb 'variant implementations of some ABSTRACT FUNCTION F with signatures s'. note that the ABSTRACT FUNCTION F may be partial even on total inputs. note that the space of abstract functions is related to the space of partial functions by the quotient operation over the homomorphism which identifies functions which differ only on non-finite or non-total or generatively non-finite/non-total inputs, and differ only by whether or not they return bottom. Note that abstract functions confuse 'codata' with 'data'.

in Oot:

(a) you cannot specify as part of a signature that you require a particular implementation; all signatures can make demands only 'up to variant implementation', that is, Oot signatures specify the abstract functions, and all variant implementations of those abstract functions fit (b) the programmer can completely control the choice of variant implementation via annotations at callsites (c) as part of typechecking, the Oot compiler determines whether or not infinite data might be provided, and if so, chooses a variant implementation that can handle infinite data (d) as part of typechecking, the Oot compiler determines whether or not a variant implementation uses stack space constant regardless of the input, and prefers those that are (e) if the Oot compiler cannot choose a variant implementation with constant stack space, this is a compile-time error unless the programmer has attached an annotation asserting that they are aware of this fact (f) oot can automatically generate variant implementations which are strictifications of other variant implementations (g) the programmer can provide hints like 'i'll be doing a lot of insertions into this data structure, give me a variant implementation with good performance in that case' (h) oot doesn't know about the definition of abstract function above, that's just a human convention; oot just knows that functions assigned to the same abstract function are interchangable except when annotations say otherwise. (i) the syntax for assigning a function to an abstract function is similar to the syntax for assigning a function to an interface/typeclass. You can retroactively assign someone's else function in a library whose source code you don't control, or don't possess, to an abstract function.

the point is that in Oot:

(a) for the most part, you don't have to think about implementations, only abstract functions -- but if you want total control over choice of implementation, you can have it

(b) for the most part, you don't have to think about foldl, foldr, foldl', foldr' and the like -- except when you want to, or when the compiler is not able to statically determine a safe choice

(c) programs are more extensible because it is impossible for a library writer to write a function which cares about which implementation it is given

so if annotations at the callsite can choose among variant implementations, then what happens when you use a library A that uses another library B with annotations at the callsites in A that call into B that specify particular variant implementations? Wouldn't this fix the choice of variant annotations beyond your control, since you cannot modify the code in A?

no; the caller of A can override the annotations in A. Perhaps to make this simple (simple syntax, and also allowing you to do this without possessing A's source code or knowing about A's internal structure), all they can do is redirect the annotation at a per-module granularity, e.g. say, "whenever A demands module B, replace this with a demand for module C".

note that this could be confusing if you replaced calls from module A demanding module A implementations with some other module B. So disallow replacing self-demands.

this is probably similar to ML's module functor system, although i haven't read about that yet so that's just a guess.

one annoying detail there; if you use library A and also library B, and library A uses libraries B and Z, and library B uses library Y, and library Y uses library Z, might you want to say:

"when i call library B directly, it should use library Y using library Z, but when A calls library B, it should use library Y and replace Z with Q"

it's clear how to do this (allow paths to be the pattern matched on for replacements), but it makes the syntax more complicated, and it might blow newbie's minds, esp. because if you do this, then when one part of your program returns a data structure of abstract type X, and another part of your program returns a data structure of abstract type X, these two may have different implementations and so may require time-or-space-expensive interconversion each time they are used together.

otoh it seems pretty necessary if you want the language to be ultimately optimizable, because certainly sometimes you will be doing something with a lot of inserts, and other times you will be doing something with few inserts and a lot of lookups or traversals, etc. by the 'no flexibility penalty for factoring', if you can tell module A to use one implementation and module B to use a different one, you should retain this power even if A and B are refactored to use a common module C.