Guide: Alejandro Serrano

[serras]

I'm Alejandro Serrano, a PhD student in the area of functional programming, currently working in Utrecht University. I use Haskell for my daily job, but I also like to explore what it is out there, especially in the world of logic (like Prolog) and functional-logic programming (like Curry), and in the large space of theorem proving. I am a fierce defendant of strong typing, although some days I wake up and think "if only we could have true Lisp macros in Haskell and ML...".

I am the author of Beginning Haskell and have worked in enhancing IDEs for the Haskell world as part of two Google Summers of Code. I have developed several open-source libraries, including a generalization of regular expressions to arbitrary data types and a Constraint Handling Rules engine.

As I said above, I am working on a PhD thesis. The topic: better type error diagnosis for domain-specific languages (aka DSLs). Full story short: we love embedding domain specific languages; they really make programmers more productive. However, when the compiler is not happy with what the user of the DSL wrote, the error message it gets is given in terms of the host language. Thus, we break the abstraction barrier: internals of the DSL leak through error messages, and even worse, the user of the DSL needs to know them to understand error messages. During the past years, my supervisor and I have developed a wide range of techniques for dealing with this problem. If you are interested, you can check my page at DBLP where all my papers are indexed.

I am happy to present most introductory topics in Haskell, depending on the demand. However, based on my expertise, I would be interested in talking about some of these topics:

• Techniques for embedding DSLs. There are manu ways to embed a DSL in Haskell. You can create a combinator language. Use a GADT to get a so-called "initial encoding". Or arrive to the "final encoding" by means of type classes. Meta-programming also gives you a lot of tools. Furthermore, if your DSL has some notion of sequentially, it makes sense to make it a monad, but how: by hand? using a free monad? using an operational monad?

  The idea is to explore the wide range of possibilities in this area. We shall focus on how good each choice works in terms of syntax, analizability of the code (so we can optimize or detect errors at compile-time) and flexibility in interpretations (so we can write the code once but execute them on different contexts).

• Haskell type system. As part of my job, I have scrutinized almost all literature related to Haskell (and GHC) type system:

  • The many ways to do polymorphism, from simple parametric polymorphism to higher-rank and impredicative polymorphism.
  • The initial distinction between types and kinds and how it is blurred by data type promotion and kind-in-kind.
  • Type classes, and its "functional" counterpart, type and data families.
  • The differences between flexible, overlapping, undecidable and incoherent instances.
  • Functional dependencies and injectivity annotations.
  • Extending the language to deal with the local reasoning coming from pattern matching on a GADT.
  • How to speak of constraints generically, using the Constraint kind.
  • Boxed and unboxed types and how to write generic functions over those with levity polymorphism.

  We can explore together examples of all these features, and argue when and how to use them.

• Category Theory in Action. During LambdaConf 2015 I realized that many people (definitely more than I thought!) is interested in category theory. I am definitely not a category theory expert, but rather a category theory user. We can explore the basic notions of category theory: categories, arrows, functors, natural transformations, monads and adjunctions, always keeping an eye at how these notions translate back to functional programming. (Are instances of the Functor class functors?, this kind of questions).

  Furthermore, I would like to show the power of category theory with two beautiful constructions. One is how to enhance the performance of a monad, almost for free, by using the Yoneda construction. The other one is how to understand a monad as the composition of two adjunctions.

I am very interested in exploring the ideas underlying Common Lisp: macros, multimethods... they seem like a completely different style of programming! Or in a broader sense, the meta-programming facilities found in many languages: Lisp macros, Elixir meta-programming, Template Haskell, MetaOCaml. We can even rethink some of those and hack a small meta-compiler! I am also willing to explore the world of "reactive" libraries, from React-like libraries like ClojureScript's Om, to Purescript's Halogen or even .NET Reactive Extensions.

Of course, if you have any other ideas, feel free to comment below! I'm sure we will all have a very enjoyable time at LambdaConf Winter Retreat 2017!

[serras]

Or let's go crazy and build a web framework based on the idea that links are morphisms in a category of pages! I know some Haskell web libraries such as Servant and Spock for the server and Persistent and Esqueleto for the database part. We just need a category theorist then ;)

[EncodePanda]

I don't have any ideas, but I'm just happy you gonna be there :)

[argumatronic]

I'm interested in all those, but I would especially like to hear you talk about techniques for embedding DSLs.

[mudphone]

The more practice I can get with various approaches to meta-programming the better. I have some intro to such in Clojure and Elixir. Would love to see examples in other languages. I'm also somewhat intrigued by your work with constraints. Is this related to relational programming (like miniKanran)?

I'm also interested in your proposed Haskell Type System and Category Theory in Action topics. I am a novice at both.

[serras]

Since DSLs seem to be something people like and also something different from other guides, I have sketched a small table of contents of such a talk, to see what people think or would like to add:

• What is an embedded DSL
• Simple combinator libraries
• The difference between syntax and interpretation: shallow vs. deep embeddings
• Initial encodings, including GADT tricks
  • Interpretation as a fold
• Finally tagless encoding
  • Interpretation as class instance or module implementation
• Computational DSLs using Applicative and Monad
  • Removing boilerplate using Free and Operational
• Encoding binding
  • Higher-Order Abstract Syntax
  • Locally Nameless using the unbound library
• Meta-programming: Template Haskell and quasi-quotation

I don't know if 2 hours would be enough to cover everything! But everything on the above list is everything I know about embedding DSLs, so it is an upper bound ;)

[serras]

I am also open to discuss the contents of the Category Theory in Action talk during one of the afternoons. This is one talk in which I don't need a projector, just a {white,black}board. If there is another talk which introduces the basic Category Theory concepts, this could be a good way to continue.

[haroldcarr]

Hello Alejandro: I would be interested in Category Theory in Action and the Haskell Type System (in that order).

[nmcb]

Personally? I would benefit and be interested in you doing a Haskell type system talk. Going deep, perhaps compare the system with other languages around? Yes, cat.theory is always interesting, but your knowledge of Haskell, especially your theoretic level combined with your pragmatism, seems very valuable.

[serras]

Given the interest in the Haskell type system talk, here is a foreseeable table of contents:

Part 1: the basics

• Hindley-Damas-Milner type systems
  • Types vs. type schemes
  • Simple checking and inference with algorithm W
• Qualified types: what you have at the left of =>
  • Type classes and type families
  • Termination: flexible and undecidable instances
  • Choice: overlapping and incoherent instances
  • Improvement: functional dependencies and injectivity annotations
  • Elaboration: dictionaries and coercions
• Higher-kinded types, * version
• Qualified constructors and pattern matching: GADTs
• Inference with constraints
  • Architectural overview
  • Skolemization, ambiguity and undischargement errors

Part 2: going crazy with quantification

• More on kinds
  • Introducing new kinds by data type promotion
  • Reflecting on value level: the singletons construction
  • Kind polymorphism
  • Unboxed types: # vs *
• Higher-rank and impredicative polymorphism
  • (Un)decidability of these extensions
• Quantifying over constraints: the Constraint kind
  • Programming your own instance search procedure
• Going dependent: -in-
  • Value-level vs type/kind/sort-level
  • Levity or representation polymorphism
• Generic programming
  • Describing regular types with generics
  • Generic deriving and default implementations
  • Reflection using Typeable, Dynamic and Data
• Bonus: refinement types with LiquidHaskell

Edit: expand the "generic programming" section Edit: added singletons and LiquidHaskell

[jdegoes]

All of these are equally interesting to me, but I'm slightly biased toward Haskell type system and category theory (especially if the latter gets as far as "real" monads, comonads, etc.).

[rezalesmana]

DSL would be great to hear. Category Theory is great as well.

[purefunctions]

Free and other 'scary' monads for beginners :) The many ways to do polymorphism

[ErrorNullPointer]

Haskell type system would be cool

[serras]

Given the input here, I am considering devoting my slot to Haskell Type System. Two hours might be even too little for so much information, though!

If @jdegoes finds it OK, we can arrange a room for speaking about Category Theory in the afternoons/evenings a couple of days. Maybe one day we can discuss the basics (category, functor, natural transformations, monads), and the other day look at the topics of the proposed Category Theory in Action (Yoneda for better performance, monad as composition of adjoints). Then people could join either day.

[LambdaMathematician]

+1 Category theory

[serras]

@haroldcarr @rezalesmana @sillypantstoan @mudphone (and any others) When we speak about "Category Theory", at what level are we talking about? That would be very helpful in trying to focus the topic.

My current idea is to have a "mini-course" on Category Theory, which should touch at least category, universal constructions (product, sum, terminal and initial objects), functor, natural transformation, adjoint, free-ness, (co-)monads, (co-)algebras, Yoneda lemma. My aim would not be to formally prove all properties, but rather try to discover them by looking at examples in Haskell (and maybe Scala also).

One possibility I discussed with the organizers is to split such a "mini-course" into 4 or 5 small sessions of 30-45 minutes each day, instead of putting everything together into one big talk where people might get lost. What do you think? Any input is welcome :)

[mudphone]

My understanding of Category Theory is limited to getting stuck at the first few chapters of various books on the topic, and watching all of Bartosz Milewski's Category Theory For Programmers playlist. Your suggestion of using Haskell to understand Category Theory sounds helpful to me.

[serras]

As a matter of concepts, I am definitely going to cover much less than Bartosz's lectures, given the shorter amount of time. My aim is to understand more ideas like:

• How does the general concept of "monad" and "functor" relate to Haskell's Monad and Functor.
• How does a natural transformation look like in Haskell? (Hint: it is a polymorphic function)
• How do we model algebraic data types in categorical terms?

[gilligan]

My vote is definitely for Category Theory. I think CT is something where is such an enormous gain in sitting in the same room so that you can ask questions. Often it is some small detail I get totally stuck with..

anyway: CT baby! :)

[serras]

Here is a concrete description of Category Theory Through Functional Programming. Any suggestion is welcome, both in the topics and in the way in which they can be explained.

Category Theory Through Functional Programming

Language: snippets will be presented in Haskell and Scala.

Target Level: Fire Lubline / Ice Skrig

Functional programming is taking over the world. And with it, categorical thinking is permeating into our code. Notions like functor, monad or free-ness are usual when diving into Haskell or Typelevel Scala. Category theory effectively gives vocabulary for design patterns: the authors of 1, 2 and 3 (you should definitely read this book!) make this connection explicit.

In order to take advantage of these concepts, it is useful to take a step back and understand the underlying ideas of Category Theory and how they all fit together. Let me be clear: diving into intrincate mathematical theories is not my goal. I want you to understand Category Theory in a practical way, in relation to programming. This relation is two-way:

• Code provides us many examples of categorical structures,
• Conversely, in many cases we can implement categorical notions directly inside our favorite programming language.

As a consequence, in order to obtain the maximum return for your time investment, you should have an intermediate knowledge of either Haskell or Scala. If you know how to declare a type class or a trait, what a higher-kinded type (or type constructor) is and have ever used a monad, you are ready. Recent versions of the compiler are recommended, for Haskell GHC 8 is the minimum.

Teaching tons of concepts in just one session makes no sense. Ideas need some time to sink before you can effectively build upon them. Thus, our exploration of Category Theory will proceed in daily small pills, of around 45 minutes every day. The (preliminary) list of topics is:

1. Introduction to categories.
2. Simple universal constructions: (co)products, terminal and initial objects.
3. The principle of duality.
4. Functors.
5. Natural transformations.
6. (Co)monads.
7. Adjoints and their relation to (co)monads.
8. Exponentials.
9. Free constructions.
10. (Initial) algebras for a functor.
11. The Yoneda Lemma.
12. Monoidal functors.

[ghost]

Alejandro, this looks AWESOME. would you recommend attempting to transcribe or implement versions of the code snippets from the talk into Clojure as an exercise? I'm a little more familiar w type theory than I am w category theory so I could be way off in terms of it's relation to lisps, but i'd be curious for the challenge anyway