Implementing and Understanding Type Classes (2014)(okmij.org)

118 pointsby jezvor 8 Jahren26 comments

Implementing and Understanding Type Classes (2014)

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

29 comments

calebhvor 8 Jahren

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.

Drupvor 8 Jahren

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.

leshowvor 8 Jahren

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)

calebhvor 8 Jahren

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.

s4vi0rvor 8 Jahren

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.

calebhvor 8 Jahren

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

catnaroekvor 8 Jahren

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

jahewsonvor 8 Jahren

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

calebhvor 8 Jahren

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

gsgvor 8 Jahren

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

tomevor 8 Jahren

> 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___vor 8 Jahren

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.

tomevor 8 Jahren

I agree, but you can't have the latter in a dynamic language anyway so I don't see why calebh said dynamic language users would miss it.

mbidvor 8 Jahren

> arbitrarily nested lists

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

harpocratesvor 8 Jahren

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.

baddoxvor 8 Jahren

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.

joshlemervor 8 Jahren

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

catnaroekvor 8 Jahren

I don't see anything wrong with rose trees:

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

Do you?

brianbernsvor 8 Jahren

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.

cjhanksvor 8 Jahren

(6)