ceylon icon indicating copy to clipboard operation
ceylon copied to clipboard

type classes

Open CeylonMigrationBot opened this issue 12 years ago • 35 comments

[@gavinking] Scope

The purpose of this proposal is to allow the definition of operations which:

  • conceptually belong to a type, but may be called without an instance of the type, and
  • are polymorphic, that is, independently defined for various types.

The terminology is not intended to imply that this feature is exactly the same as Haskell's type classes. In particular, this is not a proposal for introductions. A type class in this proposal is specified when the type is defined, not where it is used.

Concept

I would like to be able define a generic sum() function that accepts {Element*}, rather than {Element+} as it does at present. This means we would need to make Summable into a true monoid rather than just a semigroup. We would like to be able to write:

Value sum<Value>({Value*} values) 
        given Value satisfies Summable<Value> {
    variable value sum = Value.zero;
    for (val in values) {
        sum+=val;
    }
    return sum;
}

Ceylon is a perfect language for implementing this kind of thing, since we already have reified generics, so we already pass an object to the type parameter Value when we call sum().

So, conceptually, zero is a member of the metatype of Value, i.e. of the object Value. A very strawman syntax for defining such a setup would be:

interface Summable<Other> of Other
        is Monoid<Other>
        given Other satisfies Summable<Other> {
    shared formal Other plus(Other other);
}
interface Monoid<Other> {
    shared formal Other zero;
}

Now, the constraint given Value satisfies Summable<Value> would additionally imply that Value is Monoid<Value>.

Alternatively, we could move the type class constraint is Monoid<Other> from the definition of Summable to the definition of sum(), i.e.

Value sum<Value>({Value*} values) 
        given Value is Monoid<Value> satisfies Summable<Value> { ... }

but that seems a bit less convenient and would result in more repetition. Whatever.

Anyway, so for a concrete class that actually implements Summable/Monoid, we would wind up with, approximately:

class String() 
        satisfies Summable<String> {
    .... 
}
object String is Monoid<String> {
    zero => "";
}

Not sure what to do to clean up the syntax here. It could also, potentially be a separate object declaration.

[Migrated from ceylon/ceylon-spec#899]

CeylonMigrationBot avatar Jan 14 '14 02:01 CeylonMigrationBot

[@RossTate] Sounds like you want

interface Monoid<Other> {
    shared static formal Other zero;
    shared formal Other plus(Other other);
}

class String satisfies Monoid<String> {
    shared static actual String zero = "";
    shared actual String plus(String string) {...}
}

I know you wanted to get rid of statics, but that's what zero is. We've just made it useful by allowing it to be virtual. Note that there are subtleties here, but I'm offering the basics first.

CeylonMigrationBot avatar Jan 14 '14 21:01 CeylonMigrationBot

[@gavinking] I don't want static because the body of a class is an executable block of code. I do not want to open up the incredible can of worms of why can't I write this:

class String satisfies Monoid<String> {
    shared static actual String zero;
    zero = "";
    shared actual String plus(String string) {...}
}

Remember: static doesn't come on its own. Opening that door lets in the whole nastiness of static initializers.

No, much better to keep your "static"s in a toplevel object which has a separate welldefined initializer.

CeylonMigrationBot avatar Jan 14 '14 21:01 CeylonMigrationBot

[@RossTate] Ah, I hadn't thought about initialization.

CeylonMigrationBot avatar Jan 14 '14 21:01 CeylonMigrationBot

[@RossTate] Another problem is that you may want to change the monoid being used from the default one. My student is working on this via our shapes stuff. So with that (and feel free to change the syntax):

shape Monoid<Other> {
    shared static formal Other zero;
    shared formal Other sum(Other other);
}

class Rational(Integer above, Integer below) satisfies Monoid<Rational> {
    ...
} fills Monoid<Rational> {
    shared static actual Rational zero = Rational(0, 1);
    shared actual Rational plus(Rational other) = Rational(above*other.below + other.above*below, below*other.below);
}

object multiple satisfies Rational.Monoid<Rational> {
    shared Rational zero = Rational(1, 1);
    shared actual Rational this.sum(Rational other) = Rational(above*other.above, below*other.below);
}

CeylonMigrationBot avatar Jan 14 '14 22:01 CeylonMigrationBot

[@gavinking] Interestingly, the following point of view perhaps makes more sense:

interface Monoid<Value> {
    shared formal Value zero;
    shared formal Value add(Value x, Value y);
}
interface Summable<Other> of Other
        given Other is Monoid<Other> satisfies Summable<Other> {
    shared formal Other plus(Other other) => Other.add(this,other);
}

According to this syntax, you can apply the constraint when you define Summable, or when you define sum(). It seems a little more flexible. It would not stop us from having given satisfies Summable<Value> imply Value is Monoid<Value> in the body of sum(), so I think it's more natural.

I'm perfectly happy with this syntax. The bit that has me stumped is how to define the implementation of Monoid for String. Does this feel natural to you guys:

class String() satisfies Summable<String> {
    ...
}

class String is Monoid<String> {
    zero => "";
    add(String x, String y) => String(x.chain(y));
}

The idea is we're kinda splitting the definition of String into two chunks a bit like what we do with get/set pairs.

CeylonMigrationBot avatar Jan 14 '14 22:01 CeylonMigrationBot

[@gavinking]

Another problem is that you may want to change the monoid being used from the default one

I know but I would prefer to not bite that one off, at least not now. Which is why I clarified from the start that this was not a proposal for introductions. Yesyes, I know perfectly well that there are actually two very important monoids for Integer and Float but I have never actually seen people in practice writing code that abstracts over multiplication vs addition.

However, upon reflection, I'm inclined to go there, at least for the purposes of this discussion, since it might help us clarify what the syntax should be. So let's contemplate that we might possibly want to introduce this at some future point.

Well, my proposed syntax which separates the definition of the type class from the definition of the type is actually very easily capable of representing that, and this is another argument in favor of my approach. We could easily add something like this in future:

class Float() satisfies Numeric<Float> {
    ...
}

class Float is Monoid<Float> {
    zero => 0.0;
    sum(String x, String y) => x+y;
}
class FloatMultiplication for Float is Monoid<Float> {
    zero => 1.0;
    sum(String x, String y) => x*y;
}

value sum = sum(floats);
value product = sum<FloatMultiplication>(floats);

To be clear, I'm definitely not advocating that we introduce this now. I'm just trying to use it as a strawman to help motivate the syntax.

CeylonMigrationBot avatar Jan 14 '14 22:01 CeylonMigrationBot

[@RossTate] Yep, makes sense. The one thing I don't like about this syntax is having two separate declarations for Float. Maybe midde-ground that with mine:

class Float() satisfies Numeric<Float> {
    ...
} is Monoid<Float> {
    zero => 0.0;
    sum(String x, String y) => x+y;
}
object multiplication for Float is Monoid<Float> {
    zero => 1.0;
    sum(String x, String y) => x*y;
}

value sum = sum(floats);
value product = sum<Float using multiplication>(floats);

CeylonMigrationBot avatar Jan 14 '14 22:01 CeylonMigrationBot

[@gavinking] This did help me a little.

By analogy with:

interface Foo 
        of foo 
        satisfies Singleton {
    ...
}

Where we have the pattern:

interface <a type> 
        of <a value of that type> 
        satisfies <a supertype of the type>

This, we would have:

interface FloatMonoid 
        of Float 
        satisfies Monoid<Float> {
    ...
}

This to me looks like a reasonable starting point for arguing over the syntax. WDYT?

CeylonMigrationBot avatar Jan 14 '14 22:01 CeylonMigrationBot

[@gavinking]

Yep, makes sense. The one thing I don't like about this syntax is having two separate declarations for Float.

I would have the same concern, if it weren't for the fact that we have already established that pattern with getter/setter declarations:

Foo foo { return ... ; }
assign foo { ... ; }

And, hell, you could even argue that the syntax for enumerated types is similar:

class Boolean() of true | false {}
object true extends Boolean() {}
object false extends Boolean() {}

So I think of this as just an extension of that pattern.

CeylonMigrationBot avatar Jan 14 '14 22:01 CeylonMigrationBot

[@pthariensflame] If Ceylon gets extension methods, then "introductions" will never actually be needed.

CeylonMigrationBot avatar Jan 14 '14 22:01 CeylonMigrationBot

[@gavinking] OK, after a couple of iterations I arrived at this:

    // a type class:
    interface Monoid<Value> {
        shared formal Value zero;
        shared formal Value add(Value x, Value y);
    }

    // an interface constrained to types 
    // that satisfy the type class 
    interface Summable<Other> of Other
            is Monoid<Other>
            given Other satisfies Summable<Other> {
        shared formal Other plus(Other other) 
                => Other.add(this,other);
    }

    // a concrete class that satisfies both 
    // the type class and the interface
    class String() 
            satisfies Summable<String>
            is StringMonoid {
        ...
    }

    //an implementation of the type class
    //for this concrete class
    interface StringMonoid
            satisfies Monoid<String> {
        zero => "";
        add(String x, String y) => String(x.chain(y));
    }

I'm actually pretty happy with this! It preserves the natural meanings of the keywords and avoids introducing any new kinds of declaration. The only really new syntax is the is clause in class/interface declarations.

CeylonMigrationBot avatar Jan 14 '14 23:01 CeylonMigrationBot

[@RossTate] @pthariensflame: Extension methods and introductions or type classes are very different from each other.

@gavinking: Ok, I see you're reasoning about the separation. Then the one thing I don't like is having the overridden implementation be a type. If it's a type, it can be used in all sorts of ways you don't expect. So I think it's better to view it as an object. Conceptually, Monoid<Float> for Float is an interface, and the object implements that interface. Note that your new solution still seems to be mixing up types and objects in a confusing manner.

CeylonMigrationBot avatar Jan 14 '14 23:01 CeylonMigrationBot

[@gavinking]

If Ceylon gets extension methods, then "introductions" will never actually be needed.

I don't think that's right. Extension methods don't let you introduce a new type, they just let you call a function with a diffierent syntax.

CeylonMigrationBot avatar Jan 14 '14 23:01 CeylonMigrationBot

[@pthariensflame] @RossTate I must be misunderstanding what "introductions" are, then. Haskell's type classes (exempting extensions) are exactly covered by this proposal. I thought an introduction was an injection of a method into a type by a type class, which doesn't exist in Haskell (because methods don't exist, at least not in that sense). Am I wrong here? If not, wouldn't an extension method trivially delegating to a type-classed function produce exactly the same effect?

CeylonMigrationBot avatar Jan 14 '14 23:01 CeylonMigrationBot

[@gavinking]

Then the one thing I don't like is having the overridden implementation be a type. If it's a type, it can be used in all sorts of ways you don't expect.

This is certainly the least-motivated thing in what I have right now. The thing that was pushing me in the direction of interfaces here is that if we have a type like String which satisfies multiple type classes, then it has a metatype which is conceptually an intersection of type class types. We already know how to deal with mixing together interfaces, and have well-defined rules surrounding what is meaningful and what is not. Mixing together objects is a whole new thing that I kinda don't want to grapple with.

Does that make sense?

CeylonMigrationBot avatar Jan 14 '14 23:01 CeylonMigrationBot

[@pthariensflame] @gavinking You're not "mixing together objects", you just happen to have more than one instance of a type, which you definitely do already know how to deal with.

CeylonMigrationBot avatar Jan 14 '14 23:01 CeylonMigrationBot

[@gavinking]

I though an introduction was an injection of a method into a type by a type class, which doesn't exist in Haskell (because methods don't exist, at least not in that sense). Am I wrong here? If not, wouldn't an extension method trivially delegating to a type-classed function produce exactly the same effect?

An introduction (terminology I first learned in the context of AOP, but it might be older) means the ability to retrospectively add a whole supertype to a type. It sounds superficially like the sort of thing you can do with typeclasses in Haskell but actually it's broken in various ways.

CeylonMigrationBot avatar Jan 14 '14 23:01 CeylonMigrationBot

[@gavinking]

You're not "mixing together objects", you just happen to have more than one instance of a type, which you definitely do already know how to deal with.

I mean if I have:

class Float() is Monoid<Float> & Ring<Float> & Eq<Float> { ... }

Then the metatype, that is, the type of the expression Float is:

Float() & Monoid<Float> & Ring<Float> & Eq<Float>

I want to, from an implementation point of view, produce an actual value that implements this type, somewhere under the covers.

CeylonMigrationBot avatar Jan 14 '14 23:01 CeylonMigrationBot

[@pthariensflame] Then you want (roughly) what this Haskell code gives you:

{-# LANGUAGE ConstraintKinds, KindSignatures #-}
import Data.Constraint

type DecidableMonoidalRing (a :: *) = ((Monoid a, Ring a, Eq a) :: Constraint)

evidence :: Dict (DecidableMonoidalRing Float)
evidence = Dict

This is, in the proposed Ceylon syntax, just:

alias DecidableMonoidalRing<A> = Monoid<A> & Ring<A> & Eq<A>;

value DecidableMonoidalRing<Float> evidence = Float;

That is, you're just letting the metatype implement all the (meta)interfaces at once. This is just an instance (heh) of the existing confusion with the intersection-like syntax in satisfies clauses. There's no actual problem.

CeylonMigrationBot avatar Jan 14 '14 23:01 CeylonMigrationBot

[@RossTate] @pthariensflame: Extension methods are purely syntactic sugar for calling top-level/static functions/methods.

@gavinking: Okay, I think I see what you're doing. You're taking advantage of the fact that your StringMonoid interface has no undefined methods, so it can be implemented by the String meta-object without any additional specification and it can be mixed with other interfaces being implemented by that String meta-object. If StringMonoid were a class, that wouldn't be possible. It's an interesting exploitation of the existing features. Did I understand you correctly?

CeylonMigrationBot avatar Jan 14 '14 23:01 CeylonMigrationBot

[@pthariensflame] @RossTate Yes, but there's nothing stopping an extension method from delegating to a type class method on the metatype. For example:

public interface Monoid<Value> {
    Value zero;
    Value plus(Value x, Value y);
}

Value plusExtension<Value>(Value this, Value other) given Value is Monoid<Value>
    => Value.plus(this, other);

This gets you pretty much all of the (additional-to-type-classes) benefits of introductions, without basically any of the faults.

CeylonMigrationBot avatar Jan 14 '14 23:01 CeylonMigrationBot

[@RossTate] Huh? You seem to be assuming a way to make a type's metaobject implement an interface, which is what we're trying to figure out here.

CeylonMigrationBot avatar Jan 14 '14 23:01 CeylonMigrationBot

[@gavinking] Please keep in mind that I have the following ulterior goals here:

  • make it very easy to implement this functionality in the JVM, layered over the top of our existing support for reified generics,
  • without any performance compromises, or
  • impact on our type system or operational semantics.

This needs to be a bit more than syntax sugar, but I want it to be not much more.

CeylonMigrationBot avatar Jan 14 '14 23:01 CeylonMigrationBot

[@pthariensflame] @RossTate So you just declare that that's what happens. You can take a (very minor) leaf from universe-polymorphic type theory here: The metatype of a type is simply a type-level code for a kind. That is, it is a reified kind, in the same sense in which Ceylon already features reified types. Subkinding becomes involved, but that is both conceptually and implementationally no different to the subtyping that Ceylon already knows how to handle. An is clause, of the form @gavinking is proposing, is simply a "lifting" of a satisfies clause to the kind level.

CeylonMigrationBot avatar Jan 14 '14 23:01 CeylonMigrationBot

[@gavinking] Rust, one of the up'n'coming languages for systems programming, has a nice system of type classes (called "traits").

http://pcwalton.github.io/blog/2012/08/08/a-gentle-introduction-to-traits-in-rust/

CeylonMigrationBot avatar Jan 17 '14 10:01 CeylonMigrationBot

[@RossTate] From what's in that article, traits are just interfaces. If David Herman's at POPL next week, I'll double-check with him.

CeylonMigrationBot avatar Jan 17 '14 17:01 CeylonMigrationBot

[@gavinking]

From what's in that article, traits are just interfaces.

Ah ... I'm assuming that the reason they have &self as an explicit parameter to methods is that you can have a method without a &self parameter. I could be wrong.

CeylonMigrationBot avatar Jan 17 '14 17:01 CeylonMigrationBot

[@gavinking] Oh. Looks like they plan it but don't have it yet. Well, it will fit really nicely in with the rest of what they have, when they add it.

CeylonMigrationBot avatar Jan 17 '14 17:01 CeylonMigrationBot

[@Zambonifofex] @GavinKing Sorry, but I'm slightly confused by your example... What does given Other Summable<Other> mean? I'm imagining it's a typo?... And, on StringMonoid, why is zero a Float? Shouldn't it be a String? I really like the is syntax, by the way. I feel like it is pretty clean and fits nicely. I'd say it's creatively thought out, if you asked me... :-)

CeylonMigrationBot avatar May 14 '15 19:05 CeylonMigrationBot

[@gavinking]

I'm imagining it's a typo?

Yes, thanks, I fixed it.

Shouldn't it be a String?

Yes of course. Also fixed.

I'd say it's creatively thought out, if you asked me... :-)

Excellent :-)

CeylonMigrationBot avatar May 15 '15 00:05 CeylonMigrationBot