leanprover / fp-lean

Functional Programming in Lean
Other
64 stars 18 forks source link

type-classes.md -- suggestion #75

Closed lovettchris closed 1 year ago

lovettchris commented 2 years ago

The way I have come to think of it now in relation to object oriented languages is like this. The decoupling of type classes from their instances means you can extend that type without messing up your type hierarchy (no need for subclassing) because the specialization by instances has become an orthogonal issue, which I think is really nice. But I don't know the perfect language to convey this - but I think there's a powerful concept in here that needs to be explained.

david-christiansen commented 2 years ago

It makes me think a bit about Lisp or Julia-style multimethods, where behavior and structure are related by types (run-time rather than static in those cases), but both the collection of available behaviors and the implementations of each behavior for a given type combination are independently extensible.

How do you think something this would work for someone with an OO background?

Type classes are used similarly to interfaces in Java and C#. Both type classes and interfaces describe a conceptually related set of operations that are implemented for a type or collection of types. Similarly, an instance of a type class is akin to the code in a Java or C# class that is prescribed by the implemented interfaces. Unlike Java or C#, however, types can be given instances for type classes that the author of the type does not have access to. In this way, they are very similar to Rust traits.