Implementing and Understanding Type Classes (2014)

http://okmij.org/ftp/Computation/typeclass.html

by jez • 8 years ago

118 19 8 years ago

calebh4• 8 years ago

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.

mbid• 8 years ago

arbitrarily nested lists

"Cool" as it might be, please don't inflict it on others.

baddox• 8 years ago

I’m not aware of the specific type features the commenter was mentioning, but that doesn’t sound too different than a tree or graph data structure.

harpocrates• 8 years ago

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.

catnaroek2• 8 years ago

I don't see anything wrong with rose trees:

    datatype 'a tree = T of 'a * 'a tree list

Do you?

s4vi0r• 8 years ago

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.

calebh4• 8 years ago

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":

https://www.cl.cam.ac.uk/~sd601/thesis.pdf

catnaroek2• 8 years ago

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.

https://news.ycombinator.com/item?id=13781467

jahewson• 8 years ago

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

calebh4• 8 years ago

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.

Here is an example of the type error (I used the datatype from the Wikipedia article on polymorphic recursion): https://repl.it/@CalebHelbling/PolymorphicRecursionError

Drup• 8 years ago

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.

leshow• 8 years ago

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)

calebh4• 8 years ago

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.

gsg• 8 years ago

Monomorphising doesn't work for rank-n polymorphism, either. (This is mentioned on the page.)

tome2• 8 years ago

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.

g___• 8 years ago

Right, you can have rose trees without polymorphic recursion:

data Tree1 a = Leaf1 a | Node1 [Tree1 a]

flatten :: Tree1 -> [a]

But this type needs it:

data Tree2 a = Leaf2 a | Node2 (Tree2 [a])

flatten2 :: Tree2 -> [a]

Tree1 can vary in depth between nodes, while Tree2 is either a, [a], [[a]], [[[a]]] etc.

brianberns• 8 years ago

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.

Implementing and Understanding Type Classes (2014)

Related Stories