Typechecker internals · beginners

I'm interested in learning more about the typechecker and its theory (I don't know enough to be able to contribute, I'm just curious). Is there maybe an overview documented somewhere? From my beginner point of view the type system is HM with row polymorphism, polymorphic variants, some additional layer of types for task effects tracking, and then there will be traits (abilities) for ad-hoc polymorphism... I think there probably aren't any scientific papers about Roc (yet!), but maybe there are papers that influenced Roc that I could read?

Michał Łępicki (Oct 19 2022 at 20:42):

» foo = \a ->
…   when a is
…     A x -> B x
…     y -> y
…
… bar =
…   when foo C is
…     B _ -> "ok"
…     C -> "ok"
… bar

── UNSAFE PATTERN ──────────────────────────────────────────────────────────────

This when does not cover all the possibilities:

10│>        when foo C is
11│>          B _ -> "ok"
12│>          C -> "ok"

Other possibilities include:

    A _
    _

I would have to crash if I saw one of those! Add branches for them!

Ayaz Hafiz (Oct 19 2022 at 20:53):

You are exactly right, it is HM with row polymorphism, polymorphic variants, and ad-hoc polymorphism. Effects are modeled entirely with polymorphic variants, there is nothing "special" there. Our model of ad-hoc polymorphism is simpler in expressiveness from most related systems. However we also have another sort of types that are not exposed to the user used to track how functions are called, and perform defunctionalization.

There aren't any papers directly but the extensible records are like OCaml's, and polymorphic variants are like OCaml's but simpler (this is no [<] constraint for variants like there is in OCaml). The model of specializing ad-hoc polymorphism (at least in the interesting ways) is described somewhat in this document in the repo

Ayaz Hafiz (Oct 19 2022 at 20:56):

Also, records can have optional keys (I don't know what this was what inspired by, @Richard Feldman or @Folkert de Vries likely do). Roc's optional record keys mean "polymorphic in optionality", for example, a record type { a ? Str } is not concrete, but rather a generalization of both {} (which does not have the record key) and { a : Str }. So optional record keys have no runtime representation, and hence can only be pattern-matched with default values.

Richard Feldman (Oct 19 2022 at 20:59):

Ayaz Hafiz (Oct 20 2022 at 01:46):

by the way, i’m always excited to talk about this stuff with anyone who is interested. I also have a project that faithfully implements Roc’s polymorphic variants and ad-hoc polymorphism in much smaller core languages that may be easier to study and experiment with, if you are interested.

Michał Łępicki (Oct 20 2022 at 06:06):

I saw that, "cor", pretty cool! I appreciate putting out simpler examples, thank you!

Stream: beginners