I've looked at this page and some other documents since I wanted to implement type classes in Juniper (a FRP language for the Arduino). It turns out that the dictionary passing is only necessary if you want to support polymorphic recursion. In all other cases, the call to a function that is part of a type class can be monomorphized.
Hindley-Milner has problems with inferring types in the presence of polymorphic recursion, and a user provided type annotation is usually necessary. Polymorphic recursion does allow some cool things such as arbitrarily nested lists. This is a feature that users from a dynamically typed language might miss.
Inferring the most generic type in the presence of polymorphic recursion is not decidable. It's not that HM has a problem with it, it's just plain not possible.
OCaml and Haskell support it by requiring type annotations.
In general, polymorphic recursion is occasionally useful for some specific data structures (see Okasaki's purely functional datastructures for some examples) and when playing with GADTs.
Maybe I'm misunderstanding, but isn't it possible to implement type classes as monomorphized as well as using dictionary passing. Rust has traits which I think map very closely to type classes (minus HKT), and that's all done through monomorphisation.
Additionally, GHC will try to monomorphise bounded functions if it can, because it's simply much faster without the extra layer of indirection.
I could be equating a few things which aren't equal, but I'd love to hear your take (or anyone elses)
To call a function declared by a type class, you can use dictionary passing or monomorphization. GHC uses monomorphization as much as possible since it has zero overhead. Dictionaries are required only in very specific situations.
I thought the problem was related to subtyping? AFAIK the reason Scala doesn't have HM inference is because something about the existence (nominal?) subtyping makes it impossible/super hard to infer types that may seem obvious/easy - even with monomorphic functions.
Ex.
def fact(n: Int) =
if (n == 0) 1
else n * fact(n - 1)
will fail to compile and tell you that you need to provide a return type.
Type inference for systems with subtyping is a different problem. There has been progress on this issue, most notably Stephen Dolan's thesis on "Algebraic Subtyping":
Not too long was it figured out how to reconcile subtyping with type inference. However, this requires doing subtyping in a very specific way, which most users of languages with subtyping will not find pleasing. In particular, the design of the type system must pay very close attention to issues of polarity and existence of certain universal objects in the categories of types. This work caters more to designers and users of ML-style languages who want to add subtyping, than to designers and users of more traditional languages who want to add type inference.
> Hindley-Milner has problems with inferring types in the presence of polymorphic recursion, and a user provided type annotation is usually necessary.
Strictly speaking Hindley-Milner never requires type annotations. It can infer the type of any well-formed expression. You must be thinking of some extension of HM (of which there are many).
Hindley-Milner monomorphizes the type of a function inside the body of the function, so if you make a recursive call on a different type the type checker will complain. There are many subtle "gotchas" with type inference that are often not encountered by most programmers. Unless you've implemented a type inference engine yourself, you probably don't know about these sort of restrictions.
> Polymorphic recursion does allow some cool things such as arbitrarily nested lists. This is a feature that users from a dynamically typed language might miss.
What do you mean? You can implement arbitrarily nested lists (rose trees) in Haskell.
Some other applications are more interesting. For instance, finger trees (which back the efficient implementations of a handful of immutable data structures) usually are implemented in a way that requires polymorphic recursion.
I believe the commenter may have been talking about what I've seen called fix-point recursion, and it is exactly as you say, it is for representing arbitrarily nested tree structures in a statically typed way.
For example in scala, maybe you have data about Users
case class User(id: Long, name: String, friends: List[User])
However, this structures is kinda inflexible, you don't always want to deal with an entire tree of users at a time. Maybe, you just want to have the friend userids, so you can introduce a type parameter for the recursive data
case class User[Friend](id: Long, name: String, friends: List[Friend])
and then you can have a User[Long] which contains the friend ids, or User[String] which contains the friend names. However, if you want to go back and have the list be of Users themselves, you would have to know statically how deep the tree you're returning is. For example, this type would include full user information down to the grandchild level, but then terminate with the ids:
User[User[User[Long]]]
This is actually very useful! Sometimes we may want exactly this deep of a structure. If we want to get an arbitrarily deep tree of users, we would need to have an infinitely nested type like
User[User[User[User[User[User[...]]]]]]
which is of course impossible. So instead, people have a work-around using higher-kinded types, called `Fix`:
case class Fix[F[_]](unfix: F[Fix[F]])
This signature may look scary, but if you apply it to User you get
Fix[User](unfix: User[Fix[User]])
and all this means is that now we can deal with Fix[User] which means the same thing as User[User[...]]. You can construct one such Fix[User] differing levels like so:
Fix(
User(
id = 1L,
name = "Josh",
friends = List(
Fix(
User(
id = 2L,
name = "John",
friends = List(
Fix(
User(
id = 3L,
name = "Stacey"
friends = List.empty
)
)
)
),
Fix(
User(
id = 4L
name = "Mary"
friends = List.empty
)
)
)
)
As an F# developer (no type classes), I found this very informative. Thank you. I'm looking forward to the day when .NET languages (including C#) support type classes.
Are you kidding? Let's take C++: Templates are a dark art, generics are confusing and ugly, and inheritance is so so easy to screw up. Python: You use inheritance or duck typing, neither of which provide you any guarantees.
Come on, even Herb Sutter thinks that the way people contort the template metaprogramming system leaves something to be desired, hence the constexpr blocks and metaclasses proposals coming down the pipeline.
Comprehensibility is a function of both the author and the recipient.
I find that a lot of functional enthusiasts (e.g. people who are very, very comfortable with type classes) truly lack the relate-ability to make the material accessible to people who lack the same background as them.
Hindley-Milner has problems with inferring types in the presence of polymorphic recursion, and a user provided type annotation is usually necessary. Polymorphic recursion does allow some cool things such as arbitrarily nested lists. This is a feature that users from a dynamically typed language might miss.