OCaml's functors vs. typeclasses

@skaller wrote:

[There is an unrelated question to the syntax: do you REALLY want type classes? Ocaml style modules are more powerful but harder to use. Of course you can have both. Type classes are probably OK for scripting languages, that's why I chose them for Felix, but they have limitations.]

I wrote about this 6 days ago, and I think you are referring to the fact that OCaml's unique first-class functors recently have added implicit selection, so combined with modules this can apparently emulate typeclasses and more.
Could you explain about the limitations?

Actually no, I'm referring to something simpler: Consider a TotalOrder type class. So Integer is totally ordered right?
Which way? Up or down?
You see? In Ocaml it is no problem because you have
module IntegerUpOrder = ...
module IntegerDownOrder = ...
but in Felix or Haskell you're screwed. You only get ONE bite at the cherry. Type classes are strictly weaker. They fix the semantics of some notation permanently and irrevocably. Another example from Felix which is very annoying: I had to define AdditiveGroup and MultiplicativeGroup. TWO type classes. One uses + and one uses * operator. But they're both groups with the same structure.
In Ocaml, no problem. One functor. Two instances. Because the instances are nominally typed.
Of course the nominal typing is a serious PITA which makes Ocaml functors really hard to use compared to say C++ templates or Felix type classes.
Roughly, a type class is a nominal type which provides structural typing for instances.
BTW: both mechanisms are pretty bad in the sense that neither supports composition very well. You just try to define a Ring out of two Groups in Ocaml!
How does maths do it? With context sensitive language. That is, DSSLs.  You can't read any maths papers without first understanding the symbolic language used in that domain, and, often, in that particular paper!

@skaller wrote:

Haskell you're screwed. You only get ONE bite at the cherry. Type classes are strictly weaker. They fix the semantics of some notation permanently and irrevocably.

I had written about this before (citing Robert Harper from CMU) that in Haskell a typeclass can only be implemented in one way, but afaik this is because of Haskell's global type inference. Yet with local selection of implementations, then it is possible to have multiple variants of implementation for a typeclass for a particular data type. Are you referring to something else because I don't see a limitation being inherent to typeclasses or how OCaml has fixed something?

I had to define AdditiveGroup and MultiplicativeGroup. TWO type classes. One uses + and one uses * operator. But they're both groups with the same structure.

Why not define a Group typeclass that takes a type parameter for its group operation?

Of course the nominal typing is a serious PITA which makes Ocaml functors really hard to use compared to say C++ templates or Felix type classes.
Roughly, a type class is a nominal type which provides structural typing for instances.
BTW: both mechanisms are pretty bad in the sense that neither supports composition very well. You just try to define a Ring out of two Groups in Ocaml!

I'm too lazy to try to map out what you mean. Could you elaborate a bit or show example?

FYI, AFAIK Haskell doesn't have type inference at all (it has kind inference though). In any case even if the instance bindings are local, you still have s problem if you want two distinct bindings for the same types in the same context.
The reason I can't define a Group typeclass that takes a type parameter for the group operation is that types are not functions. The group operation is a function. Felix typeclasses only allow type parameters, not function or value parameters.
Of course I could add function parameters. But guess what? That's just an Ocaml functor which takes a module argument, where modules include both types AND functions.
As to composition, its well understood that neither type classes nor modules are easy to combine. I once asked on the Ocaml list how to make a Ring out of an AddGroup and a MulGroup and it took the foremost experts a couple of days to get it right. The reason is that the types of each are distinct as written and so to make them the same type requires tricky syntax, which turns out to be ad-hoc and limited in what it can do.
In Felix (and I guess Haskell) you can derive a type class from one or more others, but such derivation is not combinatorial. What we want is combinators to systematically add features together and this is really only possible for type classes that have a single type, and functions that accept such type but return an invariant type. In other words, its just OO at the compiler level, with the same limitations (covariance problem).
In principle, we "know" how to combine things because category theory tells us. In practice the modelling is so complex no one can understand it. That's basically why people use dynamics, because the correct static modelling is just too hard.
So actually, the way to do this is part of the design goals of Zen: the compiler's type system has to be a full scale purely functional programming languages. That doesn't tell you how to implement the required combinators but it does at least ensure that when you figure it out, you have the tools to do it.

@skaller wrote:

Haskell doesn't have type inference at all (it has kind inference though)

Ah I guess we just used different terminology where you mean group types aren't inferred by type constructors are. I would need to think that out a bit...

even if the instance bindings are local, you still have s problem if you want two distinct bindings for the same types in the same context.

Ah so overloading, but how do you select the desired instance within the context? Do you annotate somehow or is the proper overload inferred from context somehow?
Excuse my myopia.

That's just an Ocaml functor which takes a module argument, where modules include both types AND functions.

Seems we are back full circle to the point of what I wrote 6 days ago (as linked from my OP).

In Felix (and I guess Haskell) you can derive a type class from one or more others, but such derivation is not combinatorial. What we want is combinators to systematically add features together and this is really only possible for type classes that have a single type, and functions that accept such type but return an invariant type. In other words, its just OO at the compiler level, with the same limitations (covariance problem).

A code example might help me understand better.

@skaller wrote:

even if the instance bindings are local, you still have s problem if you want two distinct bindings for the same types in the same context.

Ah so overloading, but how do you select the desired instance within the context? Do you annotate somehow or is the proper overload inferred from context somehow?

I think what you mean is that you don't want to subsume the implementations of the typeclass to the typeclass, but rather track the intersection type of the two available implementations and then monomorphize that statically at the call site based on which implementation the call site requires?
So I think a typeclass that takes the group operation as a type parameter suffices, as the function definition can require a specific group operation instance for the typeclass.
The key insight appears to be my solution to the Expression Problem so you don't lose track of the type, so this delayed binding to instance is possible.

"Ah so overloading, but how do you select the desired instance within the context? Do you annotate somehow or is the proper overload inferred from context somehow?"
You're hitting the point backwards. The point is you CANNOT select the proper instance. Just think of i < j, where you have Up integer order and Down integer order. How can you possibly choose?
In Ocaml you choose because functor applications have nominal types: you have to name them:
UpInteger.less (i,j) or DownInteger.less (i,j).
Since these are modules you can also do:
open UpInteger
... less (i,j) ..
to avoid explicit qualification everywhere. In Haskell and Felix you CANNOT do that because the instance doesn't have a name. It is selected entirely by the type.
A typical work around is like this (in Felix code):
union DownInt = Down of int;
instance TotalOrder[DownInt] { ... }
and now
.. Down i < Down j ..
to get the unusual reversed total ordering. The problem is, you cannot add two DownInt. You have to define addition (in Felix code again):
fun + (x: DownInt, y: DownInt) => match x,y with
| Down i, Down j => Down (i+j)
endmatch;
So really, DownInt's are not integers, until you equip them with all the usual operations. Usually you don't, you just use the Down constructor where you need it to force a distinct typeclass instance but you cannot do that if you are trying to use an existing algorithm that requires Down ordering and 20 other functions defined on ordinary integers but not downwards ones.
So the workaround is only a local workaround. the only real solution is to define another function such as "reverse_less" in the total order type class and then you have to parametrise ALL your algorithms that require a total order to say which order to use.

So the workaround is only a local workaround. the only real solution is to define another function such as "reverse_less" in the total order type class and then you have to parametrise ALL your algorithms that require a total order to say which order to use.

The answer is type classes are used to model algebras.
Order is an operation, so you pass a relation as an argument. There 'ralation' would be a type class.
See Stepanov's "Elements of Programming" it's all explained in there.

Sorry I don't have it (Stepanov) and it isn't online so I can't read it (and I'm not rich enough to buy a book with examples in C++). But you have missed the point. With Haskell (or Felix) type classes you can have an algorithm and pass the ordering in as a type class, but you can only have ONE ordering for a given type such as integer. What I explained was that there is a local workaround where you use instead a variant "Down of int" which is of a distinct type so you can construct a different order for it and pass that in. Unfortunately, you can't add those integers. So you have to make a complete copy of the whole model of an integer for Down integers.
Which is entirely nontrivial and in fact probably completely impossible if you have foreign libraries which use integers directly instead of using a type class. The simple fact is most uses of integers are using integers, not a type class based model of integers with instances other than integer.
Unfortunately many types have more or less unique properties and modelling everything with type classes is going too far. In fact one could argue that types are so specialised that to use classes, be they OO classes or type classes, is a waste of time since to get a refined enough view, you would only have one function per class. At that level, composition is isomorphic to a soup of functions: you gain no benefit because you have not abstracted anything.

@skaller I have difficulty understanding your explanation. I am unable to be sure if I can guess what you are describing in words, and a complete example might be helpful.
My best guess is you want to compose over functions that employ the less operation, and you want the caller to select which ordering is employed for the entire tree of call hierarchy under a call site.
One solution appears to be what @keean suggests of having all such functions manually input the operation function separately from the data type which is being input. But I am thinking I don't agree @keean that this can't and shouldn't be done with typeclasses. Edit: I see @skaller has made a similar point:

At that level, composition is isomorphic to a soup of functions: you gain no benefit because you have not abstracted anything.

Another way appears to be to select into scope only the implementation instance of the TotalOrder typeclass that the caller wants to employ at the call site, so the compiler with monomorphise the call accordingly. Again as I understand it, Haskell won't let you scope which implementations are available to the compile since it is global inference process, but I might be mistaken about that.
So I guess I am failing to see why the problem can't be handled with typeclasses?

OK, sorry. Here is a simple example, from the Felix library:
fun sort[T with Tord[T]](x:list[T])=> ....

That sorts a list. Now consider something that builds, say, a N-M search tree or something really complicated and messy. A Zen compiler maybe .. :)
Now what can you do if the order is the reverse of what you need? You cannot provide a second type class using the other order for the same type. You're only allowed one, so you can only sort in ascending order.
The problem is you wrote the code making assumptions, and didn't explicitly pass in the ordering function. You use a type class instead and now you're very sorry!
Any single example I give will admit a modification, but the point here is that if you wrote the nasty complicated algorithm using an Ocaml module, you could reverse the order without changing the nasty complicated algorithm. You can't fix it with type classes, you have to either BYPASS type classes to fix it, or, you have to construct a new type, an integer with the usual ordering reversed, and use that.
The latter solution is not workable in more general cases, because you often have simple data types modelling complicated things.
The problem is that tying the algebra to the types is just wrong. Algebras have to be modelled entirely with functional relations using categories (modules in Ocaml) and various constructions including functors (functors in Ocaml). Type classes just don't work. Basing structure (algebra) on types is wrong.
Technically, two types have ONLY one property of any significance: they're either the same type or not. That is the end of it. Types have no other utility than providing identity.
Just for example consider a product like int * string, value (42, "Gitchiker"). you may think this type has structure. WRONG. A product is NOT a type. Its a pair of projections!
What I mean is that a product is characterised by the projections. The actual type has no utility other than the fact it is different to other types. That difference determines which projections can act on it. Its the projections that have the universal properties that define what a product is.
So again: type classes are wrong. Because they base a fixed set of related functions on some specific types, as if the types have some significance.
But this doesn't mean not to put them in Zen. I have them in Felix. Haskell has them.
Just know that the model is deficient. Its a good compromise for a scripting language.

@skaller wrote:

Now what can you do if the order is the reverse of what you need?

Here is where you lose me. Who is 'you' in the code? The caller of sort?

@skaller wrote:

So again: type classes are wrong. Because they base a fixed set of related functions on some specific types, as if the types have some significance.

Afaics, you are not factoring in that the selection of the implementation of a typeclass is not solely determined on the data type being implemented for. As I pointed out before, it is also possible to control the selection at the call site (although apparently not for Haskell).
How else could you possibly do it other than to select a set of operations to pass into the call? What does OCaml do which is better than that?

@skaller wrote:

The problem is that tying the algebra to the types is just wrong.

Having written several large programs using both module and typeclass systems, I feel able to comment:
Modules produce a proliferation of boilerplate. In effect if you parameterise a function on modules you have to provide all the modules explicitly. Modules have type parameters, and you rapidly run into the situation where you need to provide the same type parameter to several modules. When you do this you introduce redundancy into the signature, that invites mistakes at worst, or is needless repetition at best.
The advantage of type classes is precisely that they are implicit. When I call '+' on a type, the type provides all the information to know what implementation of plus to choose. We can correctly have a type class for '>' or '<'.
So I am not sure what your problem with type classes is? Sorting is an algorithm, not an algebraic operator.
You have this very problem in English, if I say "sort this class of people by height" what order will I get them back in?
We can only say something is in a ordering, or partial ordering with respect to a particular relation operator.

Afaics, you are not factoring in that the selection of the implementation of a typeclass is not solely determined on the data type being implemented for. As I pointed out before, it is also possible to control the selection at the call site (although apparently not for Haskell).

How else could you possibly do it other than to select a set of operations to pass into the call? What does OCaml do which is better than that?

Actually he is right. Type classes select which implemenration to run purely on the type of the arguments (not their values) hence the name type-classes.
Different implementations can get despatched from the call site only because the types of the arguments are different.

I agree with your analysis: type classes are weaker but easier to use. The problem is simple, for a class X there is only one instance for T = A. You cannot pass a function parameter to a type class, the index is exclusively a (list of) type(s). Ocaml functors allow you to also pass functions as parameters.
The theory is simple in principle: a functor is a mapping which takes a subcategory of TYPE as an argument and produces a new sub-category. Anything else is weaker. Type classes are therefore weaker because they only take types to construct a new subcategory. The arrows are missing as parameters.
Its a tradeoff between ease of use and power. Functors are correct, because category theory is correct. It is the only known working model of abstraction and structure. Exactly how to represent them in a programming language is another issue though :)
TYPE is the name I give to the category of types and functions, Haskell calls it asterisk. This is the category we write code for. Denotational semantics is nothing but a functor from TYPE to SET, the category of sets and functions. In Felix you can actually define functors:
typedef fun swap (x:TYPE, y:TYPE): TYPE => y,x;
which is a bifunctor from TYPE * TYPE to TYPE. The effect on the functions is left out, but can be captured with the Functor type class which has method "fmap" in Haskell (it should be called map but they messed up by already defining it :)

@keean wrote:

Different implementations can get despatched from the call site only because the types of the arguments are different.

Disagree. I can control which implementation gets dispatched for each type by choosing which implementations I import into the scope.

@skaller wrote:

The problem is simple, for a class X there is only one instance for T = A.

I request you please take the time write more coherently. I can't follow your descriptions.
Please take the time to explain so that readers can understand what you are talking about. From my perspective you are largely writing incomprehensible gibberish. Perhaps @keean can read between the lines, but I can't. Please be more explicit.

Shelby, how do you "control which implementations get imported into the call site"?
You cannot do that in Haskell. You cannot do that in Felix. And you cannot do it (legally) in C++ either.

 It should have read
class X<T> .. with T = A

meaning the instance of X with T set to concrete type A. The less and greater signs got gobbled.

@skaller wrote:

Shelby, how do you "control which implementations get imported into the call site"?
You cannot do that in Haskell. You cannot do that in Felix. And you cannot do it (legally) in C++ either.

Only what you import is visible to the compiler in the file or module you are compiling. C++ has an include.

Disagree. I can control which implementation gets dispatched for each type by choosing which implementations I import into the scope of the call site. Which is what I already wrote two times in this thread.

This is true if overlapping instances are allowed. Normally instance sets are required to be coherent, so only one instance globally can match one type, this means changing what you import cannot change the meaning of the program.
We probably want to warn if instances are incoherent.

@keean we can't enforce globally and have true Git-style modularity. I explained this to you before and apparently you forgot already, because this concept is apparently foreign to the way you conceptualize. You keep thinking that you can have a runtime loader that enforces some global consistency, but that is the antithesis of decentralized development. You keep forgetting the Second Law of Thermodynamics. Just abandon global consistency and global soundness, as it does not exist.

@shelby3 instances need to be coherent to avoid non-local definitions changing local behaviour.
If instances go not have global coherence then importing a module or runtime loading a DLL could change the behaviour of the program in unexpected ways.
You need global coherence of instances so that you can reason locally about code, without remote changes affecting it.

@skaller The point of type-classes is to enable generic programming. When we write a function we want to be able to set various requirements on the types passed in. For example:
copy_bounded(fi : I, li : I, fo : O, lo : O) requires Readable<I>, Iterator<I>, Writable<O>, Iterator<O>, I.ValueType == O.ValueType

So here we can see the copy should be passed two Readable Iterators and two Writable Iterators, where the ValueType of both iterators is the same.
The things we are passing to the function are Iterator objects, and we want to constrain the types to have certain properties.
So you can understand type-classes as constraints on types.
I don't really see the relevance of your criticisms of type classes.

Ok, so in Felix,
(1) each file is separately parsed, then the parse trees are concatenated based on include directives. Then we have
(2) desugaring of terms to more basic ones. Then we have
(3) binding/lookup/type checking. During binding, all type classes and instances are collected.Then we have
(4) monomorphisation (this is new).
(5) Optimisation
(6) Code generation (C++)
During monomorphisation polymorphic bindings to type class functions are mapped to instance functions. An error is possible if the instance function does not exist. Instances can be defined anywhere at all. They do not have to be visible from anywhere at all. The typeclass must be visible to the instance.
Felix allows overlapping instance definitions, and they can be polymorphic. If there are several instances definitions providing an instance definition of a type class function, then the one defined in the most specialised typeclass is selected if it exists, otherwise it is an error. Note that in Felix an instance does not have to provide all of the type class functions, this is not an error unless you try to use one you didn't define.
Thus in Felix, if you include a file F containing an instance for a type class, Felix uses that, if instead you include G containing a different instance, Felix uses that, and if you include both it choses the most specialised. However file inclusion in Felix is transitive, has no impact on parsing, and is independent of the location of the include directive: all AST's of included files are concatenated.
If you read that carefully you will see you cannot include a file in any scope other than the global scope, and inclusion can impact both binding and choice of type class instance, but I consider this a design fault in the system, precisely because it allows what is called hijacking, of both ordinary overloading, and also of the kind of overloading type classes provide.
In Felix, type classes do not cause any run time overhead.
In Haskell, a function accepts a dictionary containing an instance at run time. This is necessary because Haskell has separate compilation. Haskell, however, does not allow overlapping instance definitions. Thus, type classes introduce a performance overhead in Haskell.
In Fortress, the choice of the most specialised method is done the same way as in Felix I think, however the choice is made at run time (late binding). Its a very sophisticated OO system with multi-methods based on run time type class stuff.
In Ocaml, module instances are always visible at the point of use but abstraction introduces indirection and a performance overhead (unless the definition happens to be local or the trans-compilation unit inliner fixes it up). However Ocaml classes work differently, they perform run time (delayed) binding of methods. It uses lookup, but hash coding (like polymorphic variants) makes the lookup reasonably fast.

@keean wrote:

instances need to be coherent to avoid non-local definitions changing local behaviour.

Can't happen. The locality is in control of what it imports.

If instances do not have global coherence then importing a module or runtime loading a DLL could change the behaviour of the program in unexpected ways.

The locality can import the implementations it desires. If there is a conflict with other imports, the compiler should give an error.

You need global coherence of instances so that you can reason locally about code, without remote changes affecting it.

I don't see why you think so.

Can't happen. The locality is in control of what it imports.

If you have a type class with a generic implementation (ie implements a function for a polymorphic type) and you use that in a module, and you import another module that does something useful (maybe written by someone else) that implements a more specific instance of the type-class  for some type you are using, then the code will swap to using the new instance instead of the generic one. If the new instance is written in a different way it can change the behaviour.

@skaller I am thinking what you want is to be able to pass in a data type and an interface to that data type orthogonally, and so that the binding of implementations is delayed and only the ones you have specified are selected early.
f(x: A) where A: Int+TotalOrder =>

@keean I think we should consider adding this functionality combined with the ability to select different implementations for the same data type at the call site. It is very powerful and will work with the unions concept I created to solve the Expression Problem.

@shelby3 as I pointed out elsewhere a total order typeclass is underspecified because it does not specify the relation operator that the order is based on.

@keean wrote:

and you import another module

Locality is in control of what it imports.
Shouldn't the compiler warn that there is less specific option conflicting? If not, how will you never assurance coherence any way?

@keean wrote:

as I pointed out elsewhere a total order typeclass is underspecified because it does not specify the relation operator that the order is based on.

The relation operator is set in the implementation of the typeclass. That is the entire point.

Note edit:

and so that the binding of other implementations for other typeclasses is delayed and only the ones you have specified are selected early.

The relation operator is set in the implementation of the typeclass. That is the entire point.

Actually a total-order is not a typeclass at all, it is a precondition (or postcondition).
To test whether a collection is a total order requires knowing what operation the order is based on, and then actually testing the collection with it.

@keean : I do know what type classes do since I use them in Felix :) However they do not introduce constraints on the types at all. This is a wrong idea. What they actually do is introduce signatures into the function scope so the function can be bound. There is a constraint: you have to implement the required instance methods somewhere, but this is a constraint on functions not types.
Let us please separate two things: operation of type classes, and, the categorical view of the world in which types are meaningless points. The latter issue is very high level, and there is no doubt whatsoever it is correct and all models based on anything else are either incorrect or deficient. Categories are the only known modelling tool that can handle abstraction correctly. There ain't no other way. OO certainly fails.
My comments on type class weakness are unrelated to that issue: i merely point out that you can really only have one instance for a given type, whereas with Ocaml modules this is not so.
Type classes provide no functionality. They merely allow the programmer to use a systematic notational convention which is hard to provide with ordinary C++ style overloading. It's important, but its just lookup.

There is a constraint: you have to implement the required instance methods somewhere, but this is a constraint on functions not types.

Type classes are definitely a constraint on types.

@keean regardless, you are entirely going away from the salient point, which is to bind some implementations early and some delayed, by not discarding the data type when passing in a type class dictionary for that type. In other words, the type class dictionaries should be first-class, like a functor in OCaml. That is the point.

refresh

refresh again

@skaller type classes are equivalent to C++ concepts which are constraints on types.
Consider:
f(x : A) : A requires Show<A>

The function f is constrained such that it only type checks if the type A had an implementation of Show, this can be checked statically at compile time, and therefore the program is proved correct, because any value can be passed at runtime and the type checker has already proved that the type of those values implements Show.

@keean your reply to @skaller ignores my prior comment.

@shelby3 wrote:

In other words, the typeclass dictionaries should be first-class, like a functor in OCaml. That is the point. This abstraction does introduce a performance penalty though.

I disagree for most cases because it introduces lots of boilerplate. You are better off using first class functions to pass the relation operator into sort.
Records already provide this functionality, a record can have a value dependent implementation of a function, and you can pass in the record first class to provide the operators you want.

@keean wrote:

You are better off using first class functions to pass the relation operator into sort.

Nope. because that can't interopt with typeclass bounds downstream. Must make it first-class as I have pointed out. Please take some time to think before replying.

Nope. because that can't interopt with typeclass bounds downstream. Must make it first-class as I have pointed out. Please take some time to think before replying.

I don't understand your point. Please expand.

We could argue terminology forever. But I will tell you point blank, in a function with a given type class required it is not a constraint. It has no impact whatsoever on the type. It does in fact add functions to the scope in which the function is bound. That's precisely what a type class must do. It extends the lookup environment.
You can consider this a constraint only in the sense that a scope containing some functions f1, f2, etc, is extended to add extra functions such as g1, g2, etc. Technically, that is a constraint, but not on the types. Defining a function f: A -> B does not impose a constraint on A or B in my books. In fact you cannot add constraints to types in a categorical world view, it is utter nonsense. Types have no properties, they either exist or they don't, two types are the same or not, but technically that is the whole story.
Indeed type annotations do not specify ANYTHING about types at all. Because you cannot say anything about types. They don't have any properties. They do not have relations. They are just glue that joins functions or not (composition). You can ONLY talk about the relations between functions, never types.
Thus, a product type is a misnomer. There are no product types. A product type is actually a pair of functions called projections. For sum types, injections. In general, the term data type is rubbish. There is no possibility of any such thing. What we actually mean is a collection of methods. And the flaw in OO: the methods are not owned by any type. They're just functions A -> B and that means always there are two types.

We could argue terminology forever. But I will tell you point blank, in a function with a given type class required it is not a constraint. It has no impact whatsoever on the type. It does in fact add functions to the scope in which the function is bound. That's precisely what a type class must do. It extends the lookup environment.

I treat them exactly as constraints on types, and use a pure prolog logic engine to solve them. Types translate into logic as atoms, and type classes as rules and clauses, so the function above gets translated as:
show(A)

The logic engine resolves the type classes, using backtracking, as some type class matches can happen fairly deep, for example the rules for adding Peano numbers in the type system using type classes (in Haskell)
data Z
data S x

class Add a b c | a b -> c
instance Add a Z a
instance (Add a b c) => Add a (S b) (S c)

This directly translates into the following Prolog program:
z.
S(x).

add/3 : (in, in, out)
add(A, z, A).
add (A, s(B), s(C)) :- add(A, B, C)

@shelby3 here is the type signature for sort_n:
sort_n(f : I, n : DistanceType<I>, r : R)
    requires Mutable<I>, ForwardIterator<I>, Relation<R>,
    ValueType<I> == Domain<R>

So you pass a mutable iterator into the collection to be sorted, the length of the part of the collection to be sorted, and the relation the sort is defined on. Notice we constrain the function passed to be a relation (that is a binary function returning a bool with the domain being the type of the objects stored in the collection).
This is exactly how I think sort should be declared. Algorithms should have "one best most generic" way of implementing them. I imaging in time peer-review of improvements to algorithms like sort with a repository you would access them from.

@shelby3
Continuing with the 'records' thing, we can create a record with a function in:
Note I am trying to use elipsis and indenting instead of '{}' for records as it seems more in keeping with the rest of the syntax... but maybe this wont work?
data Ord<A> = Ord ...
    relation(A, A) : A

Now we can define a value:
let gt_int = Ord ...
    relation(x : Int, y : Int) : Int => x > y

You now can pass this as a first class dictionary to a function:
sort(collection, 10 , gt_int)

Inside sort you can refer to the relation:
sort(c, n, ord) =>
   ...
   if ord.relation(x, y) ...

The equivalent to a functor on a module is just an ordinary function on a record.

Right. And Prolog is just unification. But here is the reality, Felix notation sorry:
//1
fun f[T] (x:T, y:T) => add (x,y);

Fails because add is not in scope.
//2
fun add[T] (x:T, y:T) => ...
fun f[T] (x:T, y:T) => add (x,y);

Works because now add is in scope.
//3
class Addable[T] { virtual fun add: T * T -> T; }
fun f[T with Addable[T]] (x:T,y:T) => add (x,y);

Binds correctly because it is exactly the same as the previous example, except that the function add is added to the scope of the function f, not the containing scope.
//4
class Addable[T] { virtual fun add: T * T -> T; }
open Addable[T];
fun f[T] (x:T, y:T) => add (x,y);

Binds correctly because this is exactly the same as example 2: here the open directive injects the name add into the scope containing f, exactly as if it had been written there.
This localises the scope better:
//5
class Addable[T] { virtual fun add: T * T -> T; }
fun f[T] (x:T,y:T) = { open Addable[T]; return add (x,y); }

So far there are clearly no constraints on any types. All we have done is add functions to the scope.
//6
fun f[T] (x:T, y:T) (add: T * T -> T) => add (x,y);

Works fine, this is just another way to add the function add to the scope of f. Its more general than using a type class because the particular function used can have any name at all, and can vary with each call to f. Irrespective of that, the function f works because add is in scope.
So far, there are obviously no constraints on any types. Now:
//7
class Addable[T] { virtual fun add: T * T -> T; }
fun f[T with Addable[T]] (x:T,y:T) => add (x,y);
var x = f (1,2);

This binds correctly. It uses unification engine (actually specialisation), which leads to the MGU which sets T->int. This imposes a constraint alright: but not on the binding. The constraint it imposes is that you have to define Addable[int]::add. So that program above fails, this one works:
//8
class Addable[T] { virtual fun add: T * T -> T; }
fun f[T with Addable[T]] (x:T,y:T) => add (x,y);
var x = f (1,2);
instance Addable[int] { fun add (x:int, y:int) => x + y; }

Yes, there is a constraint. But it is NOT on any type. The constraint is that you have to provide an instance function add: int * int -> int. The constraint is checked during monomorphisation, which uses specialisation (unification, which is the same as Prolog). Again, it is not a constraint on types. It is a constraint on existence of functions. It is a constraint on instances of the type class, not any type. And the constraint is NOT imposed by the type class. It is NOT imposed by using the type class in the function f either. It is imposed by applying f to a pair of values of type int * int.
If you do not apply f to such a value, you do not have to provide the requisite instance. Therefore the constraint is not imposed by the type class, and it is not imposed by the definition of f either, it is imposed by using f on a particular type, and the constraint is not on that type or any other, the constraint is on YOU to provide the instance definition.
Note also that the idea there is a constraint "on a type" is clearly nonsense since a type class can involve two types. You would have to say it is a constraint on a pair of types. In fact, as noted, it is not a constraint on types at all. It is an existential constraint that requires a function.
You see, it is nonsense to say we have imposed a constraint on type int. There is no such constraint, the constraint is that you must define add: int * int -> int. If you call that a constraint on int then of course I would have to agree with you. Technically the existence of such a function does provide structure (hence a constraint), but it is not the type int which has the structure but the category of functions to which we added the function add.
For example, we can say a category "has products", and that is indeed a constraint, because not all categories have products. We can say a category "has coexponentials" and that is a constraint because Set does not have coexponentials (for example). But the constraint is on the category. It is not a constraint on a type, which is just an object in a category. It is the WHOLE category we must deal with, and its structure is entirely specified in terms of relations and properties of the arrows (functions). Its nonsense to speak of properties of types. They cannot have properties.
You have to change your world view. Only functions matter. Type checking is just a way to say checking functions can be composed. If you have f: A -> B and g: C -> D then the composition f . g is well defined if, and only if, B = C. That is a constraint on types, and it is the ONLY constraint allowed on types (equality). And in pure categories, there are no types ONLY functions and a set of composition rules.  They're convenient labels for describing which functions can be composed and which can't, and nothing more.

constraint is checked during monomorphisation

And if the type system uses parametric polymorphism (instead of universal quantification) then all types monomorphise, hence it is enforced by the type system.

@skaller
Actually if you view the type of a program as a theorem, then the program is the proof. You can have constraints in the theorem, and those constraints are part of the theorem, hence are constraints on types. They are not part of the proof.
The program is the proof, so if an instance for Show exists for A it proved the theorem f(x : A) requires Show<A>.
So the constraint is on the type.

@shelby3 : you have an example with ForwardIterator<I>. This is C++ nonsense. The correct formulation must be ForwardIterator<I,V> where V is the value type. The type class requires both types or the dereference method cannot be specified.

@skaller wrote:

you have an example with ForwardIterator. This is C++ nonsense. The correct formulation must be ForwardIterator<I,V> where V is the value type. The type class requires both types or the dereference method cannot be specified.

The value type is an associated type. (effectively a type-family tied to the type-class). It is an output type, whereas the type parameters are input types. In other words the type parameter of the the iterator type-class uniquely determines the value type.

Let me re-explain what I was thinking last night.
So in one module we have:
module First {
   typeclass LessThan<A>
      less(A, A): Bool
   typeclass Sort<T<A>> extends LessThan<A>
      sort(T<A>): T<A>
   List<A> implements Sort<List<A>>
      sort(list) => ...

   g(x: T<A>): T<A> where Sort<List<A>> + LessThan<A> => x.sort()
}

And in other module:
import First._

Int implements LessThan<Int>
   less(x, y) => x <= y      // forward ordering

f(x: T<A>) where A: Int, LessThan<A> => g(x)

And in another module:
import First._

Int implements LessThan<Int>
   less(x, y) => x >= y      // reversed ordering

f(x: T<A>) where A: Int, LessThan<A> => g(x)

Instead of:
module First {
   typeclass LessThan<A>
      less(A, A): Bool
   typeclass Sort<T<A>> extends LessThan<A>
      sort(T<A>): T<A>

   g(x: T<A>): T<A> where Sort<List<A>> + LessThan<A> => x.sort()
}

import First._

List<A> implements Sort<List<A>>
   sort(list) => ...
Int implements LessThan<Int>
   less(x, y) => x <= y      // forward ordering

f(x: T<A>) where Sort<T<A>> => g(x)

Or instead of:
module First {
   typeclass Sort
      sort(): This

   g(x: T): T where T: Sort => x.sort()
}

import First._

List<A> implements Sort
   sort() => ...

f(x: T) where T:Sort => g(x)

Added:

Note how the selection of the implementation of Sort is separate from the LessThan. I think this is what @skaller wants in terms of orthogonality of composition.

Essentially afaics what the above is doing is combining a typeclass object for the LessThan with a delayed binding on the Sort.

Let me catch up on your comments while I was sleeping and relate my vague thoughts from last night dumped above to what you all have written hence.
@skaller wrote:

You can consider this a constraint only in the sense that a scope containing some functions f1, f2, etc, is extended to add extra functions such as g1, g2, etc. Technically, that is a constraint, but not on the types. Defining a function f: A -> B does not impose a constraint on A or B in my books. In fact you cannot add constraints to types in a categorical world view, it is utter nonsense. Types have no properties, they either exist or they don't, two types are the same or not, but technically that is the whole story.

I think I probably agree with this from one perspective. The typeclass request isn't constraining what the data type is. The data type doesn't change based on the typeclass request. Rather it is constraining the set of dictionaries that must be in scope.

Indeed type annotations do not specify ANYTHING about types at all. Because you cannot say anything about types. They don't have any properties. They do not have relations. They are just glue that joins functions or not (composition). You can ONLY talk about the relations between functions, never types.

How about combining nominal and structural typing? The nominal type now has relevant members for structural typing. Is that just a projection also mapping the nominal to the structural projections?

Thus, a product type is a misnomer. There are no product types. A product type is actually a pair of functions called projections. For sum types, injections. In general, the term data type is rubbish. There is no possibility of any such thing. What we actually mean is a collection of methods. And the flaw in OO: the methods are not owned by any type. They're just functions A -> B and that means always there are two types.

Okay whether we refer to them morphisms or types, does it matter to our type checking and inference engine?

@keean wrote:

sort_n(f : I, n : DistanceType<I>, r : R)
    requires Mutable<I>, ForwardIterator<I>, Relation<R>,
    ValueType<I> == Domain<R>

With your way of structuring sort, my idea applies to for example being able to specify the implementation of Relation orthogonally at earlier binding in different modules than the other typeclasses which could be bound later. I believe your structuring avoids the T<A> that I had in my structuring, but otherwise my same concept applies. Your structuring seems to binds the chosen algorithm to the abstraction whereas mine doesn't (i.e. the implemention of mine could be implemented with enumerables or iterators, but yours commits and commits to mutable form of bubblesort instead of mergesort).

The categorical view of the world doesn't impact how you do type checking as such, it influences your language design. It tells you for example, having "interfaces for types" is a wrong idea. It tells you a type class has some types A,B,C ... and functions between them, that no types are special, because the types only serve to specify function domains and codomains.
It tells you C++ classes and virtual functions and that kind of object oriented design is a special case, not a general paradigm, even before you see the proof that it cannot work in general due to type violations.
It also hints that applicative programming is suspect. The idea is based on set theory: a type is a set of values, a function is applied to a value to yield another values. Category theory says no, there are no values, only functions, there is no application, only composition. In Haskell they say "point free" meaning "without variables", or "entirely in terms of functions".
You can recover application. For example given the type 1, also called unit, of an empty tuple (), and consider the type int. Then where previously you have a value 42 in the set int, and a function sqr to square integers, incr to add 1
42 . sqr . incr

in reverse application notation, you can eliminate the value terms except () by
() . (fourtytwo |-> sqr |-> incr)

where |-> means reverse composition. (Just inventing some notation for demo). So here
fourtytwo: 1 -> int

is the unique function with unit argument () to int that "picks out" the value 42, i,e, fourtytwo () = 42. Constant function of "no arguments" if you like. The point is once you have such a function you can forget the unit value too and now your combinator is associative, and your domain of operation consists entirely of functions. (Well known example language: Forth).
The point of seeing the idea is that, since you only have functions and do composition instead of application .. there are no values. And so what role do types have???
In fact, you do not need types at all! They're a convenient label of no significance to write
f: A -> B
g: B -> C

so now you know that f |-> g is well defined, because the codomain of f is the same type as the domain of g. Clearly you don't actually need any types to check the composition is well defined, you could use a table of well defined function compositions instead, the type notation is just familiar.
The point is, sure, yes, you still do type checking. But you do not think about types as having any meaning. They're just labels on the "joining points" of functions. A product type such as A * B tells you there are two functions which satisfy the universal law for products, you probably understand cartesian product already in terms of the idea that the "projections are orthogonal" but now you completely drop the idea that a product has a meaning as a pair of values.
Similarly, you may think that in functional programming, functions can be values. This is utterly wrong. It is not true. If you think that way you get a serious design fault, and Ocaml has that design fault because of wrong thinking. Functions are arrows in a category. What you think of as a function value, or closure, is not the same thing at all.
You can see this writing ordinary code! Even in C. The expression f (x) means to apply a known function to x. Your compiler will definitely have a special instruction for this, in Felix it is called "apply_direct". If you only have a closure, it is "apply_indirect" and the first argument is an expression not a function. Totally different: can't be optimised, you only know the type. And you will have another operator "make_closure" which converts a known function to a closure.
Why do these operators exist? Because functions are not the same as closures, even though the distinction is glossed over in many concrete syntaxes. It tells you that in Ocaml the construction:
let f x  = x * x;;

is a disaster, because f is now a function value not a  function. Which is why Ocaml is hopeless dealing with cross module recursion, whereas C can do it in its sleep. Design fault. Functions are NOT the same as function closures. In Felix the distinction is extremely clear: a function in Felix is a C++ class. A closure is a value of the C++ class. Big difference between a class and a value, eh?
So roughly, its a conceptual change: stop thinking about values, start thinking about functions. Stop thinking types mean anything more than what functions they connect. This is not to say don't use types, just think about them as what they really are: meaningless labels.
So when you think about "type classes" and "interfaces" and stuff think that the "type parameters" are just an arbitrary collection of labels used to specify how the functions connect:
class ForwardIterator[I, V]
   virtual fun next: I -> I
   virtual fun get: I -> V
   virtual fun atend: I -> bool

This is a purely functional forward iterator. It is clearly an abstraction of a list:
instance[V] ForwardIterator[list[V], V]
  fun next (x: list[V]) => match x with
    | Cons (head, tail )=> tail
    | Empty => halt "Empty List!"
  fun get (x:list[V]) => match x with
    | Cons (head, tail) => head
    | Empty => halt "Empty List!"
 fun atend (x:list[V]) => match x with
    | Cons _ => false
    | Empty => true

Note the instance is polymorphic in the value type still, but the iterator type is now fixed to be a list functor applied to the value type. The point is that the abstraction admits other functions than the three I gave for list, obviously you can do it for arrays and such like. The critical thing is that you're talking about three functions. The type class isn't specifying "interfaces for types", the types just say how the functions compose.
This particular type class is not good, because it does not specify any semantics. There should REALLY be axioms that say that applying next or get is only meaningful if atend is not true.
Although commonly the value type of an iterator depends on the iterator, it does not have to depend in any well defined way. This is wrong thinking again. The types are just labels. I can easily change the get function to contain this:
| Cons (head, tail) => head.str

Now the value type is string. I could also put this:
| Cons (head, tail) => head.str + "!!!!"

and now type classes are screwed because that is a distinct get function, even though the type is the same. So technically, you should label the instances so you can chose one of the many possible instances for a given pair of iterator/value type pairs. As I mentioned earlier in the common workaround for this design fault is to label one of the types instead (remember Down to label integers as sorting descending instead of ascending?)
Really at this point, you see you need modules and functions like in Ocaml because the application of the functor to a module, yielding a module, has to be named, which solves the problem.
In practice you do type classes ANYHOW because they're easier to use. But you have to recognise they're a feature for representing concepts in the language YOU the language designer feel are fairly fundamental, such as iterators, and you just accept that you're fixing a particular kind of way of doing things: type classes basically allow you to invent systematic notation systems, but you only get to use the notation one way, so you use them with care to pick the right use for your language.

@keean Let me see if i understand what you mean by an output type: you would write something like
class ForwardIterator [I => V]
   virtual fun get: I -> V

to say that V is a type label to use in a function signatures, but it is "dependent on I". Then you have to specify it in your instance:
instance ForwardIterator[list[int] => int]
fun get (x: list[int]) : int => ....
Apart from my notation, is that the idea? The instance supplies, not only the functions, but it also supplies output types as well?
Obviously, this is even more constrained than if the type V above were a parameter, but as we know type classes are even more constrained than modules and functors because you cannot index them on functions, whereas you can do that with modules/functors. So the additional constraint weakens the definition even further, but such weakening also has the advantage of reducing even more the amount of specification required to use them.
i hope I understand. Felix doesn't have such dependent types and not having them means some constructions with type classes require manually adding the dependent type to the input list, which destroys the convenience of the notation.
Do I understand correctly?

@skaller wrote:

Do I understand correctly?

Yes the output type is functionally dependent on the input types. It is weaker than giving both as a parameter, but that is not what you want when programming. Given a collection of type 'x', I want to derive an iterator from the collection that iterates over the type of objects in the collection. Hence the iterator should determine the type of object.
Its not just about ease of use, its about getting the algebra of collections and iterators to have the desired properties.

Let me try to understand how the typing works. Consider first (Felix again sorry):
class Fwd[I,V] { virtual fun get: I -> V; }
fun f[V,I with Fwd[I,V]] (x:I) : V = { var x : V = get I; return x;}

Since V is specified as a parameter, we can type check the assignment and the function return type.
However this code has a serious problem in Felix! The procedure argument has type I: we cannot deduce the type V. So this use:
... f it ...

will fail because V cannot be deduced. We have to write instead
.... f[int] it ...

for example, to specify the value type (the iterator type is deduced). We have to do this because there is no constraint on the value type, it could be anything. Now clearly the dependent output type solves that problem, because you can now call f, and the iterator type I is deduced from the iterator argument.
But what is the return type of f?  That's a problem! It's not enough to know that it depends on I.
So this is a real problem as I see it. We only know the type when monomorphisation selects the instance which then specifies the type. It's not good enough, because we bind the code polymorphically first. We can't type check. Felix does polymorphic type checking, instance binding happens later during monomorphisation.  That is, the type checker just assumes the type class functions are parametrically polymorphic, even though this is a lie because only selected specialisations are actually defined in instances.
I'm confused. I do not see how this can work. The problem is that the "functional dependence" of V on I is not accessible in the type class, that is the type function that calculates the type of V does not exist there: that function is the map from I to the type class instance settings of V for that I (for each concrete value of I). But when binding we do not consider instances. That happens later. The type checking is already complete.
I have to know the type of every expression in Felix, because Felix has overloading. For any expression e, and a set of overloaded functions f, the choice of which f is made in an expression f e  based on the type of e. The choice cannot be deferred. We have to make the choice immediately, to determine the type of f e.
This is not true if you do not have overloading. You can defer the choice and use type inference to fill in the type variables later, because you only have one function f: you can just give the most general possible type and specialise it as you get more information. At least my algorithm for overloading cannot do that.

@skaller wrote:

that no types are special, because the types only serve to specify function domains and codomains.

It seems to me we use types because it is model in which we want to think when doing composition. We wish to think in terms of data, not in terms of relations of morphisms.
Because it seems without types, we have a huge system of simultaneous equations of domains and codomains. Instead we create a model with the rigidity of types so we apply local reasoning. This has the disadvantage of reducing the degrees-of-freedom, whilst the advantages of approachable reasoning and feasible type inference. Category theory can only takes us so far, because humans can't program coherently in that model.

@skaller The functional dependence is on the type. If we have a collection of type Array<Int>, then the iterator for this collection has a type that is parametric on the type contained in the collection. The instance of iterator for the collection has a free type variable. Something like this:
typeclass Iterator
    data ValueType
    ...

Array<T> implements Iterator
    data ValueType = T
    ...

So the type of ValueType only depends on the type of the collection being iterated over, but that does not need to be a parameter of the Iterator type class.

@keean I think @skaller is coming at this from the perspective of wanting types to not provide any rigidity and instead be entirely flexible to what function compositions proscribe.

@skaller wrote:

for example, to specify the value type (the iterator type is deduced). We have to do this because there is no constraint on the value type, it could be anything.

Maybe I am misunderstanding, but this seems like a problem to me.  Presumably that's a type error. If you can statically detect the type error, then clearly you already know that the allowable type is f[int], so why not infer it? Unless you can only detect that error at runtime, which would make the type system unsound.

Edited:

Sorry but if only 0.1% of the programmers can understand your code, then it is useless on any scale of mainstream open source (although might be acceptable for an open source niche such as mathematics).

@shelby3 wrote:

@skaller math doesn't come in only one conceptual abstraction. There is more than one way to skin a cat. Type theory is not the same as category theory. We create type systems and syntactic conventions that optimize the programmer experience, not the arbitrary chosen mathematical abstraction. That is not to claim that there isn't more degrees-of-freedom in a category theory model with only functions as nodes on a graph and types as graph edges. @keean's typing model is types as nodes on the graph and edges between them for inference.

I feel I don't understand OCaml's functors well enough to understand what @skaller thinks we could do better? And I didn't get any feedback on my idea upthread.
Would we please get some clear elucidation from you experts on whether we need some form of later or variable selectable binding of implementation to data type?
I want to nail down the syntax and it seems the choice of syntax for typeclasses may depend on whether we need such a feature.

@shelby3 Did you see my post about records providing some of the functionality, and if you use records, functors become ordinary functions (which is good in my opinion as why create a new category of functions that are somehow different from ordinary functions). Records have type parameters like modules.
If records have associated types and private functions in the implementations (can easily be done by returning a record instance from a closure) we just need to make opaque types a global feature and I think we can do anything the OCaml module system can do with records. It would also remove the separate syntax for modules, as they would simply be records.
And guess what, union types solve the module typing issue too, as the type of an associated type would be the union of all the different associated type definitions in the record values. I am not yet sure whether we can infer this type, or if you would have to list the possible types in a union in the record type.

@keean I don't know what "associated type" is? Need to see code.
I don't understand what records what to do with late or selectable binding of implementations of typeclasses?

If records have associated types and private functions in the implementations (can easily be done by returning a record instance from a closure) we just need to make opaque types a global feature

I have no idea what all that means. Could you translate it to a code example or otherwise explain it for a mere n00b like myself?

@shelby3 An associated type is one where the type depends on the type parameters of the record, module or type class. consider:
data Rec A = Rec ...
    type ValueType : *

The type of ValueType is completely determined by the type of `a`

This means we might do:

let x : Rec Int = Rec ...
type ValueType = String
So what this means is that the record has a property called `ValueType` which is a type, not a value;

Regarding late binding, we can have a record like this:

data Number = Number ...
(+) (A, A) : A
(-) (A, A) : A
(*) (A, A) : A
(/) (A, A) : A
We can define a value of this record type:

let integer : Number = Number ...
(+) (x, y) = ...
(-)  (x ,y) = ...
(-)  (x, y) = ...
(/) (x, y) = ...
We can then pass this to a function as a first class value:

f(z : Number) : Number =>
5 z.+ 6
So we can pass in any record instance that provides functions that match the Record type, can then call them from within the function.

@keean wrote:

data Rec A = Rec ...
    type ValueType : *

The type of ValueType is completely determined by the type of a

Do you have a typo? Where is a defined?

@keean wrote:

Regarding late binding, we can have a record like this:
data Number<A> = Number ...
    (+) (A, A) : A
    (-) (A, A) : A
    (*) (A, A) : A
    (/) (A, A) : A

That binds interface type to data type which breaks any solution to the Expression Problem.

We can then pass this to a function as a first class value:
f(z : Number<A>) : Number<A> =>
    5 z.+ 6

So we can pass in any record instance that provides functions that match the record type, can then call them from within the function.

That does not provide late binding of selecting which one of multiple implementations of an interface we want for a particular data type.

That does not provide late binding of selecting which one of multiple implementations of an interface we want for a particular data type.

The function called is determined by the record passed at runtime, which is as late as you can get.

Do you have a typo? Where is a defined?

No the type of ValueType is defined in the implementation
Different implementations for different types can provide different definitions for ValueType.
In the lambda cube this is a type dependent type. We want all corners of the lambda cube except types that depend on values.

@keean wrote:

No the type of ValueType is defined in the implementation

I know that. I meant where is a in your definition. You had instead *.

@keean wrote:

The function called is determined by the record passed at runtime, which is as late as you can get.

The selection of the data type is late, but the binding of the interface to the data type is early. And I am repeating myself.

refresh

The selection of the data type is late, but the binding of the interface to the data type is early. And I am repeating myself.

This is true, but this is how modules and functors in OCaml work.
I believe I understand what you have in mind for the expression problem. If we have a polymorphic function on type A like
f(x : A) where Show<A>

and we call this from something where the type is unknown until runtime like:
var x
if random ...
    x = "Hello"
else ...
    x = 43
f(x)

Then although the type of x is not determined until runtime we can construct a union type for x that would be Int | String. So we know that when typing f we have that Int | String must implement Show, which means both Int _and+ String must implement Show, and at runtime we must pass both dictionaries. Then finally at runtime when the call to show happens in f the correct dictionary is chosen based on the type argument passed to f. As we know all the types in the union type, the compiler can emit a complete type case statement that is type-safe because it cannot go wrong (receive a type it is not expecting) at runtime.

refresh

@shelby3 wrote:

Fundamentally you do not seem to maintain a conceptualization of the Expression Problem, and I often have to reexplain it. I will be making a long comment to explain all of this including what I think @skaller wants.

Done.

@shelby3 wrote:

module First {
   typeclass LessThan<A>
      less(A, A): Bool
   typeclass Sort<T<A>> extends LessThan<A>
      sort(T<A>): T<A>

   g(x: T<A>): T<A> where Sort<T<A>> => x.sort()
}

I realize the above is not @keean's preferred form. Any way that could be written instead (with a correction above as well):
module First {
   typeclass LessThan<A>
      less(A, A): Bool
   typeclass Sort<T<A: LessThan>>
      sort(T<A>): T<A>

   g(x: T<A>): T<A> where T<A>:Sort => x.sort()
}

I was trying to decide if I had to abandon the OOPish form of typeclass specification and I don't think so.

@skaller wrote:

The idea is based on set theory: a type is a set of values, a function is applied to a value to yield another values. Category theory says no, there are no values, only functions, there is no application, only composition.

But without types, then we do not have the foundational axioms for logic. I quote from Wikipedia:

The heart of Curry's paradox is that untyped lambda calculus is unsound as a deductive system, and the Y combinator demonstrates that by allowing an anonymous expression to represent zero, or even many values. This is inconsistent in mathematical logic.


Create functions to pull vendor connection details from folio

A la VMA.
Organization records might need to be created in FOLIO for some (e.g. pod). Interfaces will need to be created for data exports. Blocked by https://github.com/sul-dlss/FOLIO-Project-Stanford/issues/626

folio-test has a POD organization with the data to connect to POD: https://folio-test.stanford.edu/organizations/view/7c010c6a-dc51-46ff-b698-7ee5d9a6dfd1

See #626
In standup on 4/9/2024, we discussed the use cases for inputing connection info in folio and how it is not yet a task for library staff and we decided that library systems will be the ones that input connection info directly in airflow for now.


sonobuoy: 0.56.13 -> 0.56.14

Automatic update generated by nixpkgs-update tools. This update was made based on information from https://github.com/vmware-tanzu/sonobuoy/releases.
meta.description for sonobuoy is: "Diagnostic tool that makes it easier to understand the\nstate of a Kubernetes cluster.\n"
meta.homepage for sonobuoy is: "https://sonobuoy.io"
meta.changelog for sonobuoy is: ""
Updates performed

Golang update

To inspect upstream changes

Release on GitHub

Compare changes on GitHub

Impact

Checks done (click to expand)

built on NixOS
The tests defined in passthru.tests, if any, passed
found 0.56.14 with grep in /nix/store/07awlwimxmjnhj89qvy6n28v9xkgsdk6-sonobuoy-0.56.14
found 0.56.14 in filename of file in /nix/store/07awlwimxmjnhj89qvy6n28v9xkgsdk6-sonobuoy-0.56.14

Rebuild report (if merged into master) (click to expand)

1 total rebuild path(s)

1 package rebuild(s)

First fifty rebuilds by attrpath
sonobuoy

Instructions to test this update (click to expand)

Either download from Cachix:
nix-store -r /nix/store/07awlwimxmjnhj89qvy6n28v9xkgsdk6-sonobuoy-0.56.14 \
  --option binary-caches 'https://cache.nixos.org/ https://nix-community.cachix.org/' \
  --option trusted-public-keys '
  nix-community.cachix.org-1:mB9FSh9qf2dCimDSUo8Zy7bkq5CX+/rkCWyvRCYg3Fs=
  cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
  '

(The Cachix cache is only trusted for this store-path realization.)
For the Cachix download to work, your user must be in the trusted-users list or you can use sudo since root is effectively trusted.
Or, build yourself:
nix-build -A sonobuoy https://github.com/r-ryantm/nixpkgs/archive/3f82c23054abfe030480808d43b14a1cc8846de0.tar.gz

After you've downloaded or built it, look at the files and if there are any, run the binaries:
ls -la /nix/store/07awlwimxmjnhj89qvy6n28v9xkgsdk6-sonobuoy-0.56.14
ls -la /nix/store/07awlwimxmjnhj89qvy6n28v9xkgsdk6-sonobuoy-0.56.14/bin

Pre-merge build results
We have automatically built all packages that will get rebuilt due to
this change.
This gives evidence on whether the upgrade will break dependent packages.
Note sometimes packages show up as failed to build independent of the
change, simply because they are already broken on the target branch.
Result of nixpkgs-review run on x86_64-linux 1

1 package built:

sonobuoy

Maintainer pings
cc @carlosdagos @saschagrunert @wilsonehusin for testing.

@ofborg build sonobuoy

At some point the short description should be made 1 line & remove the trailing period


Install and try out @million/lint

Description
https://million.dev/blog/lint
Additional Information

#1597

Tested it out now, but it's pretty broken. At first, it failed hard in the language selector (among others) which is using the Combobox from the design system. This did not happen without million-lint.
When I worked around that (just not showing the Combobox), I got a Should have a queue. This is likely a bug in React. Please file an issue. error. Dropping this tool for now, as I don't get far enough to actually get any value from it.


Feature request: Allow manual setting of cell count

Repro:

In the power menu, set the voltage slider to 2.8v
Power the goggles up from a 12v source (Simulating a 4S 18650 pack at 3v per cell)
The goggles show 3S
You will therefore not get a warning when the voltage drops to 11.2v (4 cells at 2.8v each)

Solution:
The cell count in the power menu needs to be able to be manually set

I added a toggle and slider to the power settings page to switch between auto/manual mode and select the number of cells here: https://github.com/Nikolas-S/hdzero-goggle/tree/feature/manual_batt_s_count
I just preordered my goggles recently so if someone already has goggles and would be willing to test I would appreciate it, so I know if it works before creating a pull request.

I added a toggle and slider to the power settings page to switch between auto/manual mode and select the number of cells here: https://github.com/Nikolas-S/hdzero-goggle/tree/feature/manual_batt_s_count I just preordered my goggles recently so if someone already has goggles and would be willing to test I would appreciate it, so I know if it works before creating a pull request.

awesome, please open a PR right away, we will get it tested and fixed if need be, there.

Removed the bug aspect of this issue, will re-create in another issue so that can now be addressed

Aww crap, I think I noticed a bug.
The Cell Voltage slider is now inoperable.
It's always in the "selected" state (bar is green), and when I select it, it exits the power menu

@Nikolas-S Aww crap, I think I noticed a bug. The Cell Voltage slider is now inoperable. It's always in the "selected" state (bar is green), and when I select it, it exits the power menu

are you sure you are running the latest version of that PR? voltage deal works fine here.

@Nikolas-S Aww crap, I think I noticed a bug. The Cell Voltage slider is now inoperable. It's always in the "selected" state (bar is green), and when I select it, it exits the power menu

Hmm that's interesting, taking a quick look at things I changed that might be relevant, I don't see what could cause that issue.
Is it repeatable?

are you sure you are running the latest version of that PR? voltage deal works fine here.

I was not aware that there was a newer version than the one I tested.
I just re-flashed with this one and all is OK

are you sure you are running the latest version of that PR? voltage deal works fine here.

I was not aware that there was a newer version than the one I tested. I just re-flashed with this one and all is OK

there wasn't. the ci builds every commit that is submitted via PR, you must have picked one from before my last round of review.

I think what caused that issue was that I changed the max element count of the power setting page from 4 to 6 in the latest commit of the PR, if you were using a version where it was still 4, that would explain that behavior. @evilC


Enable HMSS in the kingdom with k9s correctness test for both MPC pro…

…tocols.

This change is


Whitelist @types/got

See https://travis-ci.org/github/DefinitelyTyped/DefinitelyTyped/builds/669145664#L234. Related to: https://github.com/DefinitelyTyped/DefinitelyTyped/pull/43453

This is unneeded since we don't currently have two @types packages where one depends on got (current version) and another depends on @types/got (old version preserved on DT for shipping fixes).


[LRO] Add ApiMessageOperationTransformer

This is the ApiMessage equivalent of ProtoOperationTransformers.

PTAL

PTAL

Reverted status code change.
PTAL


[Enhancement]: Marker clustering on the Map widget

Is there an existing issue for this?

[X] I have searched the existing issues

Summary
Ability to consolidate nearby markers that are presented on the map as a single icon.

https://developers.google.com/maps/documentation/javascript/marker-clustering
Why should this be worked on?
Was requested by a user - https://discord.com/channels/725602949748752515/725609493974614076/989123012144029736

Yes, this is very important when I have over 100,000 potential markers. And the use of a filter is impossible due to implicit criteria. And yet, if possible, it would be very convenient to specify the marker icon in the request.

@danciaclara can you also find out what is the extended functionality here? Does the user also need to expand all the markers if the they click on a certain badge. I am asking this to understand the complexity and effort required. If its just to show this kinda badge it should be easy to implement.

Let me reach out to this user @somangshu


New version: Datadog.dd-trace-dotnet version 2.42.0

Pull request has been created with WinGet Automation :rocket:
Microsoft Reviewers: Open in CodeFlow

@wingetbot waivers Add Validation-Executable-Error


version 1.0.3 on Android 10 using PixelCopy API fails, reverting to 1.0.0 uses MediaProjection and works

on Android 10 (Samsung A9) using the latest version with the following code you get a black screenshot:
public class ScreenshotActivity extends Activity {
    private ScreenshotManager _mgr = null;
    private ScreenshotResult _scrRes = null;

    @Override
    protected void onActivityResult(int requestCode, int resultCode, @Nullable Intent data) {
        // ----> THIS IS NEVER CALLED
        super.onActivityResult(requestCode, resultCode, data);
        _mgr.onActivityResult(requestCode, resultCode, data);
        finishActivity(requestCode);
    }

    @Override
    protected void onCreate(Bundle savedInstanceState) {
        super.onCreate(savedInstanceState);

        // setup screenshotty
        ScreenshotManagerBuilder bld = new ScreenshotManagerBuilder(this);
        _mgr = bld.build();
        _scrRes = _mgr.makeScreenshot();

        // observe the result
        _scrRes.observe((result) -> {
            // ----> THIS IS CALLED, BUT THE RESULTING SCREENSHOT IS ALL BLACK
            Screenshot scr = (Screenshot)result;
            saveScreenshot(scr);
            finish();
            return Unit.INSTANCE;
        }, (ex -> {
            // failure
            finish();
            return Unit.INSTANCE;
        }));
    }
}

after a few digging around, i think it's the new Pixel API which fails somehow (but still report success), and that is used as default on android 10. as you can see from the comment, the observe successful callback is called without the OnActivityResult() handler called first, thus resulting in the black screenshot.
reverting to version 1.0.0 (which uses the mediaprojection api) works correctly, btw .... still, the PixelCopy API implementation is probably flawed/wrong/not applicable.
i would suggest to offer a way to select the API to use instead, without defaulting 'blindly'.... unless until you find a workaround.
cheers!

Thanks!
We will look into it as idea is good. If you wish you can even create a pull request for this issue.

Thanks!
We will look into it as idea is good. If you wish you can even create a pull request for this issue.

Anyway, i looked a bit into it. Probably it is working as intended, coz the PixelCopy API I don't think it can be used to take screenshot of the whole device screen but only for your Activity. So it could be reasonable it returns a black screen, I was trying to capture whole screen screenshot using an invisible Activity on top. Reasonable to add the option to use whichever API one chooses, but still I think this is not a bug and the issue may be closed if you wish.....

We believe that option to choose different APIs is valuable for the library, so we would keep the issue open and we will try in future releases add it.

Hey @valerino, with Screenshotty v1.0.4 we've exposed the option to configure screenshot actions order. Now it's possible to run MediaProjection API as the first action.


Trigger pipeline from other pipeline does not work

We've tried to configure to trigger the pipeline from another repository.  But it didn't work.
Observed behaviour:
when adding the snippet
# this is being defined in app-ci pipeline
resources:
  pipelines:
  - pipeline: securitylib   # Name of the pipeline resource
    source: security-lib-ci # Name of the pipeline referenced by the pipeline resource
    project: FabrikamProject # Required only if the source pipeline is in another project
    trigger: true # Run app-ci pipeline when any run of security-lib-ci completes

Into your pipeline, the resource was referenced (different builds could be selected, when using the "Run Pipeline" dialog.
Expected behaviour:
Completion of security-lib-ci pipeline should automatically start the app-ci pipeline.
We've managed to fix that behaviour, via "Edit" app-ci pipeline -> "Triggers" -> manually selecting security-lib-ci. However, this was not reflected in the yaml.
We also didn't achieve this configuration via the terraform provider.
Is there a way to configure that in an Everything as Code way (AzD Pipeline YAML or Terraform)?

Document Details
⚠ Do not edit this section. It is required for docs.microsoft.com ➟ GitHub issue linking.

ID: 86285f72-9e28-da97-59bb-c29eb60f627d
Version Independent ID: 18d5a591-a7d3-c261-6bff-8808ae433f54
Content: Configure pipeline triggers - Azure Pipelines
Content Source: docs/pipelines/process/pipeline-triggers.md
Product: devops
Technology: devops-cicd-process
GitHub Login: @steved0x
Microsoft Alias: sdanie

@Laetus This might better be addressed as a product question. To make sure it gets in front of the right people, please submit your bug here. Link back to this issue, so we can see if there are documentation fixes we should make.
I'm going to keep this open as a doc enhancement.

@Laetus Did you ever find out if the artifact was necessary?

@AdamSir2 Its unclear if it is, but the linked StackOverFlow posts indicates that it is needed, and from my testing appeared to be the case. The big need for me was changing the default branch, the documentation is not very clear on that. Really if they would just adapt what @ccoutinho wrote there it'd be perfect (along with linking that example).

@aolszowka for those who read in the future - I have this working WITHOUT an artifact as I have a pipeline running Terraform (no -output flag used).
As you have referred to the issue was with the branching - the branch defaults to "main" and you need to explicit tell the pipeline which branches to respond to.

For anyone else that comes across this (assuming Microsoft doesn't shove this down the memory hole like they like to do when its inconvenient). The above StackOverflow post does seem to work still. We never heard back from @AdamSir2 on how to avoid needing a pipeline artifact.

I believe this is the new section in the documentation that is referred to as resolving the issue:
https://learn.microsoft.com/en-us/azure/devops/pipelines/process/pipeline-triggers?view=azure-devops#branch-considerations
If anyone still has trouble with this, please file a new doc feedback which will go into our new system (To learn more about our new feedback system please visit aka.ms/contentuserfeedback), and include a link to this issue.


🧪SPIKE DHCP search function

User Story:
As an engineer I want to be able to quickly and easily search for sites on the DHCP portal so that I am not slowed down in troubleshooting or carrying out my work.
As a DevOps engineer I want to ensure that the ability to search for sites via name on the DHCP portable is scalable so that usability is not impaired as more sites are put onto the portal.
Context:
There is currently no inbuilt search function on the DHCP portal. This means that for engineers to find a site they need to to use control F and rely on their browser to provide this function. This currently works but there is a limited number of sites on the portal and additionally will not be able to query any underlying databases. This means that we cannot add pages onto the portal as the browser search function cannot search in-between pages. This means our current solution limits us to having one page on the portal.
We want to look to provide a basic search function with the option to provide more advanced features later on
To Do:

[x] We have a search function on the NACS portal.  Can we reuse any of this on the DHCP portal?
[x] If we cannot reuse anything look into different methods to provide this feature and quantify the work involved
[x] Attach findings onto this ticket

This ticket is linked to another ticket to add a description on the subnets to the DHCP portal.
The NAC portal has this required search function and this works well.  Please replicate for DHCP

Tom and Jenny to speak with Mary and engineers for further details and requirements. e.g. what do we need exactly to be pulled up in the search function?

Time box - 3 days actual time (not elapsed)

KMS access added to the assume role and tested its working now.
Copied Database dump to s3 bucket

During the SPIKE, we addressed the following areas:

Automated the construction of the Bastion.
Established cross-account S3 access from the bastion for all environments.
Developed a mechanism for generating database dumps across all environments.
Introduced search functionalities on DHCP, utilising site ID, Name, and Subnet CIDR in a Local Build.

Next Steps:
Conduct Testing:

Automated Build and User Acceptance Testing (UAT).
Proceed with Releases:

Deploy to Development & Pre-Production.
Execute Production Release

https://app.zenhub.com/workspaces/nvvs-devops-622a0b371800e400133bb924/issues/gh/ministryofjustice/nvvs-devops/525

Release the feature in to development and pre-production

#525


MCP251XFD_INT_SPI_CRC_EVENT

When using the MCP251XFD_DRIVER_USE_READ_WRITE_CRC driver configuration, I'm always getting MCP251XFD_INT_SPI_CRC_EVENT set in the interrupt flags. When reading the CRC register, it tells me MCP251XFD_CRC_FORMERR_EVENT is set, i.e. a format error.
This is quite odd, because a) I have verified that nCS is properly handled (not release before the last byte has been transmitted) and b) everything else still seems to work fine. Even letting nCS low for some cycles longer does not change the problem.
Do you have any idea what else could be the problem?
(And perhaps a side question... do you think CRC communication is necessary at all?)

SPI CRC format error is, as you notice, a frame with a CRC with a byte missing.
To verify, the best is a Logic analyser.
If you really have a byte missing, you should not be able to read the CRC registrer...
I have used the CRC on a critical system where all all data needs an integrity check.
If you think, in your application, it is not necessary to use it, you can stay in normal mode

Yes, it looks perfect.
Do you use the MCP2517FD or the MCP2518FD?
If you use the MCP2517FD, this device is quite tough regarding the SPI (see §17 of the driver library guide or the MCP2517FD errata DS80000792B).

Yeah, I know, no, it's the MCP2518FD. It's really strange. I will crosscheck with another MCP. But since it's definitely not a driver issue, I'll close this here. Thanks.


DMP-121 Schedule Notification requests to Gov Notify using Spring Sch…

…eduler.
https://tools.hmcts.net/jira/browse/DMP-121
Schedule Notification requests to Gov Notify using Spring Scheduler.
Does this PR introduce a breaking change? (check one with "x")
[ ] Yes
[x] No

This PR doesn't cover this part of the task
The cron expression should be able to be configured differently for each environment. This will involve adding some config backed by an env var which can be configured and passed into the process via flux and helm.

I think it would also be better to use a cron expression as this will give us more options, such as not running notifications at the weekend etc.

This PR doesn't cover this part of the task

The cron expression should be able to be configured differently for each environment. This will involve adding some config backed by an env var which can be configured and passed into the process via flux and helm.

done

I think it would also be better to use a cron expression as this will give us more options, such as not running notifications at the weekend etc.

done


changes made

#951
[Cite any related issue(s) this pull request addresses. If none, simply state “None”]
Fixes:  #951
Description
conflict resolved
Type of PR
Feature enhancement
Screenshots / videos (if applicable)
[Attach any relevant screenshots or videos demonstrating the changes. Make sure to attach before & after screenshots in your PR.]
Checklist:

[x] I have made this change from my own.
[x] I have taken help from some online resources.
[x] My code follows the style guidelines of this project.
[x] I have performed a self-review of my own code.
[x] I have commented my code, particularly in hard-to-understand areas.
[x] I have made corresponding changes to the documentation.
[x] My changes generate no new warnings.
[x] I have tested the changes thoroughly before submitting this pull request.
[x] I have provided relevant issue numbers and screenshots after making the changes.

@JanitKumar

Please see the conflicts highlighted in the image above. Resolve the conflicts in the mentioned files. Ensure you pull all the latest changes before pushing your feature/bug fixes to the main branch. After resolving the conflicts, please open a new PR for review.
Thank you!


chore: add path triggers for abe2e

What type of PR is this?
/kind cleanup

What this PR does / why we need it:
adds explicit path triggers for Linux AgentBaker E2E to ensure we only run it when relevant files are changed
Which issue(s) this PR fixes:

Fixes #
Requirements:

[ ] uses conventional commit messages

[ ] includes documentation
[ ] adds unit tests
[ ] tested upgrade from previous version

Special notes for your reviewer:
Release note:
none

Pull Request Test Coverage Report for Build<PHONE_NUMBER>

0 of 0   changed or added relevant lines in 0 files are covered.
No unchanged relevant lines lost coverage.
Overall coverage remained the same at 79.095%

Totals

Change from base Build<PHONE_NUMBER>:
0.0%

Covered Lines:
2255

Relevant Lines:
2851

💛  - Coveralls


Check for filter/exclude fields of an object before deciding if to index or delete

PR for https://github.com/toastdriven/queued_search/issues/8
In particular, I used to have something like qs = self.get_model().objects.filter(foo=1).exclude(related__bar=True) in my model's index's index_queryset method, but this is not being used in queued_search. So this fix makes it possible to define attributes like the following in a model to only index certain objects that pass a filter.
@staticmethod
def queue_filter():
    return {'foo': (1,)}

@staticmethod
def queue_exclude():
    return {'related.bar': (True,)}

sad face again


super-user-spark <IP_ADDRESS>-dev -> <IP_ADDRESS>

Motivation for this change
Upgrade.
Disclaimer
This is my first contribution and I'm not sure how to test this change. Please help?
Things done

[ ] Tested using sandboxing (nix.useSandbox on NixOS, or option sandbox in nix.conf on non-NixOS)
Built on platform(s)

[ ] NixOS
[ ] macOS
[ ] other Linux distributions

[ ] Tested via one or more NixOS test(s) if existing and applicable for the change (look inside nixos/tests)
[ ] Tested compilation of all pkgs that depend on this change using nix-shell -p nix-review --run "nix-review wip"
[ ] Tested execution of all binary files (usually in ./result/bin/)
[ ] Determined the impact on package closure size (by running nix path-info -S before and after)
[ ] Ensured that relevant documentation is up to date
[ ] Fits CONTRIBUTING.md.

Notify maintainers
cc @badi

Hi! Welcome!
You can test by running
nix-build -A super-user-spark

in the root of your nixpkgs checkout (I like adding --dry-run to see a plan first).
A successful build will create $PWD/result as a symlink to the installation so you can run eg:
./result/bin/spark parse ...

I get the following on a nix-build:
test/SuperUserSpark/Compiler/Gen.hs:29:10: error:
    • Could not deduce (GenUnchecked a)
        arising from a use of ‘Data.GenValidity.$dmshrinkValid’
      from the context: GenValid a
        bound by the instance declaration
        at test/SuperUserSpark/Compiler/Gen.hs:(29,10)-(30,32)
      Possible fix:
        add (GenUnchecked a) to the context of the instance declaration
    • In the expression:
        Data.GenValidity.$dmshrinkValid @(Deployment a)
      In an equation for ‘shrinkValid’:
          shrinkValid = Data.GenValidity.$dmshrinkValid @(Deployment a)
      In the instance declaration for ‘GenValid (Deployment a)’
   |
29 | instance GenValid a =>
   |          ^^^^^^^^^^^^^...

test/SuperUserSpark/Compiler/Gen.hs:36:10: error:
    • Could not deduce (GenUnchecked a)
        arising from a use of ‘Data.GenValidity.$dmshrinkValid’
      from the context: GenValid a
        bound by the instance declaration
        at test/SuperUserSpark/Compiler/Gen.hs:(36,10)-(37,42)
      Possible fix:
        add (GenUnchecked a) to the context of the instance declaration
    • In the expression:
        Data.GenValidity.$dmshrinkValid @(DeploymentDirections a)
      In an equation for ‘shrinkValid’:
          shrinkValid
            = Data.GenValidity.$dmshrinkValid @(DeploymentDirections a)
      In the instance declaration for ‘GenValid (DeploymentDirections a)’
   |
36 | instance GenValid a =>
   |          ^^^^^^^^^^^^^...

Alright @badi Great feedback. I just released (on hackage) a new version that doesn't have this build error.
The tests pass for me locally but not on nix, so I turned them off for now.

I think we can close this and continue on #78790

I'm closing it, because of #78790. @NorfairKing I see that you don't plan to maintain super-user-spark, should we close the other PR as well and remove it from nixpkgs? I'm still using it to manage my dotfiles, probably is a good time to start using home-manager

@jlesquembre Yes let's remove it from nixpkgs.
Thanks for closing this.

Thanks @NorfairKing , I created a PR to remove it: #87379


work_contact_and_about_section_of_Portfolio

Create work related 4 sections.
Create about section
create contact section
Remove stylint errors

Thanks. I really appreciate your efforts for such a quick review.


Re-name repo and transfer it

@ViralBShah thoughts on either renaming and removing references to JuliaBox or renaming, removing references to JuliaBox, and transferring to JuliaAcademy?

We can do it once we shut down JuliaBox, which is a few weeks away.

@logankilpatrick There's also this related issue tracking the same thing, i think: #25

Let's track it here since that one is closed.