OCaml's functors vs. typeclasses

@skaller

[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

@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 improved this?

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

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

@shelby3

@shelby3 wrote:

@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

@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 will monomorphise the call accordingly. Again as I understand it, Haskell won't let you scope which implementations are available to the compiler since it is global inference process, but I might be mistaken about that.

So I guess I am failing to see why the intended goal 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

@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

@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

@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 :)

@skaller

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.

Could 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

@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

@keean I don't know what "associated type" is? Need to see code.

I don't understand how records are applicable to 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?

Basically eveything you wrote is meaningless to me because I can't relate the terminology to anything concrete.

@shelby3

@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<A> = 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<Int> = 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<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.

@keean

@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

@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

@keean wrote:

No the type of ValueType is defined in the implementation

I know that the type unification is in the implementation. I meant where is a in your definition. You had instead A and *.

@keean

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

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.

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.

However we will need run-time-type-information for the types in the union to implement the type-case (I know we are both aware of that, but I am putting it in for completeness).

The above could work with modules, but you would have to pass a set of modules in that match the types in the union and do the type-case manually, which is lots of extra boilerplate, but you can do this already with the records we have.

refresh

@shelby3

@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

@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

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

@skaller

@skaller wrote:

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.

I'am with you with semantic specifications.
But are semantic specifications easily verifiable?
IMHO, if you define laws for an operator/function which operates on the instance of a typeclass, then the law has to be checked for all values of that instance.
For example: Int implementing Eq[Int], then reflexivity, symmetry and transitivity has to be verified/checked for all values in Int for each function/operator parameter which should slow down the compiler, right?

Navigation Menu

Repository navigation

OCaml's functors vs. typeclasses #22

45 remaining items

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

OCaml's functors vs. typeclasses #22

Description

Activity

skaller commented on Oct 2, 2016

shelby3 commented on Oct 2, 2016

skaller commented on Oct 2, 2016

shelby3 commented on Oct 2, 2016

shelby3 commented on Oct 2, 2016

skaller commented on Oct 2, 2016

keean commented on Oct 2, 2016

skaller commented on Oct 2, 2016

shelby3 commented on Oct 2, 2016

skaller commented on Oct 2, 2016

shelby3 commented on Oct 2, 2016

shelby3 commented on Oct 2, 2016

keean commented on Oct 2, 2016

keean commented on Oct 2, 2016

skaller commented on Oct 2, 2016

45 remaining items

shelby3 commented on Oct 4, 2016

keean commented on Oct 4, 2016

shelby3 commented on Oct 4, 2016

keean commented on Oct 4, 2016

shelby3 commented on Oct 5, 2016

shelby3 commented on Oct 5, 2016

keean commented on Oct 5, 2016

shelby3 commented on Oct 5, 2016

shelby3 commented on Oct 5, 2016

keean commented on Oct 5, 2016

keean commented on Oct 5, 2016

shelby3 commented on Oct 5, 2016

shelby3 commented on Oct 5, 2016

shelby3 commented on May 20, 2017

sighoya commented on Jan 31, 2018

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions