Algebraic Data Types: Kinds and cardinality

Let’s get this out of the way before we go any further: This is a massive chapter. There is a so much content in here, and there is no way that I’ll be able to summarize it all in one neatly packaged post. Instead, I’ll be focusing on the things that struck me as particularly important: kinds and cardinality.

That means that in exchange for covering a few topics more thoroughly, I will not be devoting many words to newtypes, arity, what sum and product types are (see chapter 4 and chapter 9), or constructing and deconstructing data types (see chapter 7a).

Kinds

This section has several references to the data type known as Maybe. We have not covered this data type previously in this series, so a short introduction is in order if you’re not already familiar with it.

Maybe is used to model data that you may or may not have. It has two data constructors: Just and Nothing, takes one type parameter, and is in some ways similar to how a lot of other languages have a null value, though more robust. It is similar to the Option type in other languages such as Rust, OCaml, and F#.

The data declaration is as follows:

data Maybe a = Just a | Nothing
deriving (Eq, Ord)

Kinds are to types what types are to terms. Or, put differently, a kind can be seen as a type constructor’s type or as a type one level up. It sounds convoluted, but bear with me.

Keep in mind that, as covered in chapter 4, a type constructor is one of two constructor types in Haskell (the other being data constructors). It is the name of the type. Type constructors are used only at the type level, in type signatures, and in typeclass declarations and instances.

We represent kinds with the * symbol. If you have a fully applied, concrete type constructor, such as Bool or [Int], then the kind is *. If you have a type constructor that is still waiting for a type parameter—such as Maybe—then that has the kind * -> *. A kind is not a type until it is fully applied. In other words, Maybe isn’t a type, but Maybe String is.

Second, we only talk about kinds on the type level. That is, Bool is a type and has kind *. False is a term (or value) and does not have a kind. For data constructors that share names with their type constructors (e.g. []), this can be confusing, but remember that kinds only operate on type level constructors.

To make this clearer, let’s turn to the ever faithful GHCi. To print the kind of a type constructor, we use the :k (or :kind) command followed by the constructor we want information on. Let’s have a couple of examples and see what we can learn.

Prelude> :k Bool
Bool :: *

Bool is a fully applied type in and of itself. it takes no type parameters and as such has kind *.

Prelude> :k Maybe
Maybe :: * -> *

Maybe is our first higher-kinded type (more on that in a bit), which means it’s a type constructor that requires another type before it’s complete. In other words, you couldn’t simply put Maybe in a type signature without saying what type of maybe it is.

Prelude> :k Maybe Integer
Maybe Integer :: *

Maybe Integer, on the other hand, is a concrete type. As opposed to just Maybe above, we also know what the type is (Integer). As such, it is fully applied and of kind *.

Prelude> :k (,)
(,) :: * -> * -> *

This one is quite interesting. This is the type constructor for a tuple. Without any type parameters, it’s of kind * -> * -> * because it needs two types to be fully applied.

Higher-kinded types

According to the book, there are only ‘a few’ kinds, and the default (and the only one covered in this chapter) is *. Kind signatures work the same as type signatures, i.e. using the same :: and -> syntax.

Higher-kinded types are types that require type parameters to be fully applied, to become real types—that is, their kind is at least * -> *. Lists, tuples, and Maybe are good examples of higher-kinded types.

Cardinality

The cardinality of a type is the number of different values it defines. A value defined by a type is also known as an inhabitant of said type. Types’ cardinalities can be anywhere from as small as 0 (empty types) and as large as infinite.

To demonstrate this concept we’ll use these arbitrary sum types, modeled after the starters in the mainline Pokémon games (just pretend we’re in 1999 for simplicity’s sake):

data StarterType
= Grass
| Fire
| Water

data Starter
= GenI StarterType
| GenII StarterType

The cardinality of StarterType is 3 because it has only three possible inhabitants. The cardinality of Starter is 6, because it has two data constructors, each of which also require a StarterType. As such, we get 2 ⋅ 3 (or 3 + 3), which is 6.

Above, the Starter type demonstrates why it’s called a sum type: We can calculate the cardinality of the type by summing the number of possible values of each of it’s data constructors.

If you’ve got a friend with a link cable, then maybe you’ve traded some pocket monsters and ended up with two starters—lucky you! In this case, you now have a tuple of starters, i.e. (Starter, Starter). A tuple is a product type, so that means we find the cardinality by multiplying the cardinality of each of its contained types. As such, the cardinality of (Starter, Starter) is 6 ⋅ 6 = 36.

This is the basic concept of cardinality in types. It’s pretty straightforward, and it’s a good thing to keep in mind when designing systems.

The function type is exponential

We’ve seen that sum types are the addition operator and that product types are the multiplication operator when it comes to calculating inhabitants of types. However, we haven’t mentioned function types, which act as the exponent operator: given a function a -> b, the formula for the number of inhabitants is ba. So if we have a function StarterType -> Bool, for instance, the number of possible implementations is 23 = 8. This relationship continues as the number of parameters increases, so for a -> b -> c it’s equal to cba (or (c ^ b) ^ a).

If this is a bit confusing: don’t worry, I’m right there with ya. But let’s give it a go. Let’s write out all possible permutations of the function StarterType -> Bool.

acceptStarter1 :: StarterType -> Bool
acceptStarter1 Grass = True
acceptStarter1 Fire = True
acceptStarter1 Water = True

acceptStarter2 :: StarterType -> Bool
acceptStarter2 Grass = True
acceptStarter2 Fire = True
acceptStarter2 Water = False

acceptStarter3 :: StarterType -> Bool
acceptStarter3 Grass = True
acceptStarter3 Fire = False
acceptStarter3 Water = True

acceptStarter4 :: StarterType -> Bool
acceptStarter4 Grass = False
acceptStarter4 Fire = True
acceptStarter4 Water = True

acceptStarter5 :: StarterType -> Bool
acceptStarter5 Grass = False
acceptStarter5 Fire = False
acceptStarter5 Water = True

acceptStarter6 :: StarterType -> Bool
acceptStarter6 Grass = False
acceptStarter6 Fire = True
acceptStarter6 Water = False

acceptStarter7 :: StarterType -> Bool
acceptStarter7 Grass = True
acceptStarter7 Fire = False
acceptStarter7 Water = False

acceptStarter8 :: StarterType -> Bool
acceptStarter8 Grass = False
acceptStarter8 Fire = False
acceptStarter8 Water = False

Whew. And that’s with only two possible result values and three possible inputs. Yeah, this gets wild pretty quickly.

Closing up

While the format is a bit different from previous posts in the series, I hope you found something useful here too. The rest of what the chapter covers is definitely interesting, but not eye-opening in the way that kinds and cardinality are. The next chapter is on handling errors and includes Maybe, Either, more higher-kindedness, and anamorphisms (if that sounds interesting, why not check out this post on corecursion and anamorphisms in the meantime?). Stay tuned, and it should land at some unspecified future date.

Until next time: stay safe.

Craft yourself a new weapon!

The Magit logo was created by Prospect One, © Jonas Bernoulli. Licensed under CC BY-NC-SA 4.0 and available on GitHub. No changes were made to the logo.

Some tools are so good that once you start using them, you can’t imagine not using them. Magit is one such tool. If you’re also working with GitHub or GitLab, you can use Forge to make life even better.

In this post, I’ll be giving a brief overview of what Forge is, how to get started (well, at least what’s not in the manual), and the problems I ran into.

Magit and Forge

Magit is a ‘Git porcelain inside Emacs’. In other words, it’s a Git UI inside Emacs, providing access to repo status and a number of different commands. Magit is so good, that even if I used another editor for developing (hah, as if!), I’d still switch back to Emacs to handle my Git business.

Forge is a Magit extension that allows deeper integration with certain forges1, such as GitHub and GitLab. For instance, when using GitLab, it allows you to create and comment on issues and pull requests, assign tasks, add labels (with auto-complete), open and close issues and more; all from within Emacs.

Motivation and early impressions

After posting this article to Reddit, I was asked about my motivation for using Forge over the GitLab UI. This section attempts to outline why I wanted to switch and what my impressions are after having used it actively for work for a couple of days.

Why not the GitLab UI?

I use GitLab for work, and while I think it’s great in a lot of respects, it also has its share of issues, especially with the user interface. In general, navigating between projects, issue boards, and merge requests is very clunky and takes far too many clicks for it to be a good experience.

Because of this, I have bookmarked various projects’ merge request overviews and issue boards, and use the bookmarks for navigating. It’s not ideal, but it works tolerably well.

What doesn’t work very well, however, is creating issues or merge requests. Not only do you need to write fairly long-form content, but you will also frequently want to add ‘labels’ or assign someone to a task. GitLab does have so-called quick actions, but they don’t seem to work when used in the web UI.

This means writing and editing text in plain HTML text areas (without your favorite key bindings) and then having to use your mouse to navigate a UI, find multiple searchable lists of elements and filter and find the items you’re looking for.

Overall: not a great experience.

Other options

As was pointed out in the Reddit thread, there are a number of ways to deal with the web UI issue. Notable contenders are the Edit with Emacs extension for Chrome and Firefox, Emacs Application Framework (EAF) and it’s browser, and Vimium and Surfingkeys.

I’m already a heavy user of Surfingkeys (though I realize I still have a lot of key bindings to internalize), and it’s great for navigating your average website, but GitLab has so many things you can click on and interact with that it gets quite messy.

I tried Edit with Emacs, and while it’s a really neat way to interact with text, it wasn’t for me (for GitLab). I still had to activate it using my mouse, and it didn’t relieve me from using the mouse to interact with the label and assignment menus either.

As for Emacs Application Framework, I’d never heard of it before. It looks super cool, but I’m a bit scared that if I go down that road, I’ll never make it out alive. Further, this post by u/DarkNightened has some really good points on why the EAF might not be the right fit for this use case (as well as some pretty 🔥 Surfingkeys tips).

Early impressions

After having used Forge for a few more days, my impression is overwhelmingly positive. There are a few things it doesn’t do, but I imagine some of that may be limited by the API that GitLab exposes. It also seems like GitHub receives more attention than GitLab, so it’s quite possible that that integration has more features.

In the following sections, I’ll be referring to issues and merge requests (MRs) collectively as topics, which is what Forge calls them.

The good parts

Issues and MRs in the Magit status buffer
This is the most basic thing that Forge gives you. In addition to just displaying these topics, it also displays labels (correctly color-coded) and whether a topic is open or not. If you expand an MR it’ll list the commits it is made of. Viewing one of these items (by pressing <RET>) will also display assignees, all related comments and actions that have been taken.
Easy creation of issues and MRs from within Emacs
Of all the things that Forge does, this is what I wanted more than anything. I’m pleased to say that it works incredibly well. There are a few things that you can’t do from Emacs (see the next section), but these are minor issues.
Autocomplete on typing when referencing issues and MRs, assigning users and labels

This one took me by surprise, but when you start typing out a topic ID (prefixed with # for issues or ! for MRs) you get auto-completion on topics in the project. The completion candidates show not only the ID, but also the topic title. This is super handy if you’re adding related topics or otherwise want to reference them. This applies to seemingly all Magit buffers, including buffers for topic creation and for commit messages.

You’ll also gain tab completion when assigning users to a topic or adding labels.
Quick copy a link to any topic, or open the topic in your browser
Opening a topic in your browser comes with a default key binding, and there is a function for adding the URL of the topic at point to your kill ring (forge-copy-url-at-point-as-kill). The latter wasn’t bound to a key by default, but it’s a very useful command when you need to share the link to a topic with a coworker or the like.
Viewing and checking out MRs is a breeze

It is incredibly easy to check out and create a branch from a merge request. Not much more to say about this, really. See the section on branching in the manual for more information.

The not-so-good parts

Certain values can’t be set from Emacs
When creating merge requests, I haven’t been able to specify that a merge request requires approval before being merged or that the source branch should be deleted after the merge. It’s a minor thing, but it’s something we do all the time on the team I’m on, so it’d be a nice feature to have.
Merge requests show diff between local branches
Say you make a few commits to the master branch (without pushing) before branching off, making a few more commits, and creating a merge request. Forge shows this MR as only containing the commits you made after branching off from master, even if the first commits you made to master haven’t been pushed to the remote.
May (or may not) affect Magit performance
This is very uncertain and probably inaccurate. Magit has felt a bit slow over the past couple of days, but my machine is under quite heavy load, so I don’t actually think it’s been any slower than usual. All Forge updates should be performed asynchronously, so it shouldn’t have a noticeable impact. However, when the minibuffer says ‘pulling <repo>’, my mind tends to automatically assume that Emacs isn’t ready before the pull is successful. It does however relate to the next thing:
When you make a change in Emacs, Forge goes ahead and tries to sync this with the remote right away, but until the sync is complete, the data you see in Emacs is still the same that it was before you edited it. This gives the impression that you must wait for a sync to finish before it’s complete and that Emacs is busy updating, when it actually isn’t. I’d love to see the Magit buffers update with your changes instantaneously, and then rather revert back (with an error message) if syncing with the remote failed.

Getting started

To get started, I’d recommend following the manual, which outlines most of what you need to know and shows you all the keybindings you need. That said, I did run into some issues (both on macOS and on NixOS), and there was some prerequisite knowledge I did not have, so I’ve decided to document that below.

Authentication: using .authinfo

The manual does have a section on getting started that includes some writing on setting up authentication, but, at least for GitLab, it requires some steps not mentioned in the manual.

Emacs uses ~/.authinfo files to handle credentials. I struggled to find much information about the format and what is required, but I can confirm that this entry format works:

machine gitlab.com/api/v4 login <username>^forge password <api-token>

Simply replace username and api-token with your username and your API-token (with ‘api’ scope), put it in ~/.authinfo, and you’re off to the races. Admittedly, I don’t know what the ^forge bit after the username means, but I assume it somehow relates it to Forge.

For more information on secrets and authentication, see this article on Mastering Emacs, which goes into quite a bit of detail of how to deal with encryption and credentials in Emacs.

macOS issues

Can’t fetch topics

When setting it up on macOS, the biggest issue I ran into was that I couldn’t successfully fetch topics (issues and pull requests). This appears to be a well-known bug with the ghub package that Forge uses, and this GitHub issue has a couple of workarounds for it. Personally, I had to force a workaround, by evaluating the following snippet:

(setq ghub-use-workaround-for-emacs-bug 'force)

However, I didn’t put it in my config, and it seems to have worked successfully without setting this on subsequent uses, so it may or may not be necessary.

I also ran into a problem with window-purpose during the setup, causing an error about ‘recursive load’. There is an issue on GitHub that describes it. One of the comments said to put

(require 'window-purpose)

in your .spacemacs file, which seemed to fix the issue for me.

This has not been an issue on NixOS.

NixOS issues: ‘no EmacSQL SQLite binary available’

NixOS required much less fiddling to get set up, but there was an issue with my Emacs missing a binary, causing it to fail on startup. Specifically, I was told that there was ‘no EmacSQL SQLite binary available’, much like this issue about a missing C compiler. There may be a number of ways around it, but the solution I found was to change my installation of Emacs to one that includes the required emacsql-sqlite package. To do that, I replaced my Emacs listing in .configuration.nix with the following:

(emacsWithPackages (epkgs: [ epkgs.emacsql-sqlite ]))

I’ve only just started using Forge, but I’ve been very positively surprised by how much power it gives me directly from my favorite editor. Being able to check out and create branches from merge requests with a single command? Yes, please. Not having to take my hands off the keyboard to set issue labels? Perfect. Editing text and creating issues in an actual text editor and not having to copy it over into a browser window? You had me at Emacs.

I suspect there is still much to discover, though, so let’s get going!

Footnotes

1. According to wikipedia, a forge is ‘a web-based collaborative software platform’

Org mode: tasty tricks

The best thing since last week

The source code blocks in this post are marked as shell code blocks, even though they are actually Org snippets. This is because of limitations with my current blogging setup, which does not permit me to display source code blocks in a nice fashion if the interpreter does not recognize the language.

Intro

Org mode (Wikipedia, official website) is a powerful tool. On the surface, it looks like a lightweight markup language akin to Markdown, but if you look closer, you’ll find that the Emacs major mode is so much more. It’s a scheduler, a task manager, a spreadsheet editor, an organizing tool, and a way to do literate programming. I’ve been using the basic functionality of Org for a long time, but I recently took some time to explore the manual and pick up some new tips and tricks.

Custom TODOs

One of the easiest features to get started with is the TODO-system. Being able to tag a headline as TODO or DONE with a keypress makes it a super easy to get started with task management. I initially used it for logging work at my old job because keeping track of JIRA tickets through a web browser became a bit tedious.

The basic two-state system works well in a lot of cases, but sometimes you want a little more control. For that, you can create your own set of keywords. The paragraphs below give some examples of how I use it and some basic tips. For more information, consult the manual.

Creating and configuring keywords

One simple, but very powerful feature of Org is that you can define your own set of keywords to use as TODO-states. You can do this on a global level or on the file level. While doing it on the global level might be useful if you always want access to a specific set of keywords, defining your keywords at the file level allows you to work with a custom set of keywords for every file you operate on.

To define keywords for a file, use the #+TODO: keyword and list your desired states, using | as a separator between states that need work and states that that are considered closed. For instance, here’s the set of keywords that I’m using for writing this very post. The set indicates whether a heading needs more work, is ready to be reviewed, is done, or if it should be cut:

#+TODO: TODO REVIEW | DONE CUT

Emacs offers you a number of ways to switch the state of an item. By default C-c C-t cycles through the list. You can also use S-<right> and S-<left> (that’s S as in super), to change to the previous and next states, respectively.

When you have more than two states, switching to a specific state can start to get tricky if the flow isn’t necessarily unidirectional. To make it easier to jump to a state, Org also allows you to add a ‘hotkey’ that you can use to set that state. This is done by putting the desired key in parentheses after the keyword:

#+TODO: TODO(t) REVIEW(r) | DONE(d) CUT(c)

Now, when you invoke the org-todo command (C-c C-t), rather than cycling through states, Emacs asks you to enter one of the assigned keys. Thus, if an item is currently marked as TODO, but you want to move it to REVIEW, the whole command would be C-c C-t r.

If you want more information assigned to each state, you can also tell Org to log the date and time of when a TODO-state was assigned as well as prompt you to add a note when that happens. As an example, here’s the setup I’m experimenting with for recording and tracking blog post ideas:

#+TODO: IDEA(i!) DRAFT(d!) UPDATE(u@) READY(r!) | PUBLISHED(p!) ONHOLD(o@)

The ! after a letter tells Org mode to log the time when this state was entered. The @ tells Org mode that in addition to logging the time, I also want it to prompt me for a little note. With the set above, I want to track the times of all state changes, and when setting the state to UPDATE or ONHOLD, I also want to log a little note. This helps me remember why I put it in that state: Was there a paragraph that needed rephrasing? Have I got a better way to do things that I want to update a post with? Did I no longer see the post as relevant?

The ability to log all of these details is great, but it can quickly get messy. For instance, here’s what a heading might end up looking like if we add some timestamps and notes to it:

** CUT Drawers
- State "CUT"        from "REVIEW"     [2020-03-08 Sun 20:17] \\
This is out of scope for now. Consider extracting this into a separate post.
- State "REVIEW"     from "TODO"       [2020-03-08 Sun 20:16]

This can add up fast, so we can make use of what Org calls drawers to keep our file tidy. These are delimited blocks of content that can contain anything but headlines and other drawers. Content put into drawers will be hidden by default (Org collapses it for you), and it will not be expanded by regular visibility cycling. If you want to cycle the visibility of a drawer, place your cursor on the drawer to cycle it.

Logging to a drawer would change the above example to this:

** CUT Drawers
:LOGBOOK:
- State "CUT"        from "REVIEW"     [2020-03-08 Sun 20:17] \\
This is out of scope for now. Consider extracting this into a separate post.
- State "REVIEW"     from "TODO"       [2020-03-08 Sun 20:16]
:END:

Now, no matter how many more entries you add to the log, Org will just show you a collapsed :LOGBOOK: line (that you can expand if you want to). To make Org log into drawers, use the following line:

#+PROPERTY: LOG_INTO_DRAWER t

Org-agenda

Another part of Org that has great synergy with TODO-items is the agenda view. To get started with agenda, you can add a file to the agenda list with org-agenda-file-to-front (C-c [). Then, when you invoke Org Agenda, you can choose between a number of different ways to view data found in all your agenda list files.

I’m still getting into it, but I’ve found immediate benefit from being able to quickly get an overview of all my open TODO items, and being able to easily toggle their states from a unified view, no matter which file they’re located in.

For more information, see the chapter on agenda views in the Org Mode manual.

Org capture templates

Capture templates allow you to quickly and easily record notes and ideas into predefined files using a format you specify yourself. This is great for when you get little ideas that you just need to jot down somewhere and store for later.

I use it to record post ideas and to track the state of certain processes at work. The template allows you to automatically add plenty of context and to prompt the user for specific keywords, making the recording process as painless as you want to. Again, the manual is the best place to go for more information.

Literate programming

One aspect of Org mode that I’m really excited about but haven’t really gotten into yet is literate programming. In short, literate programming is a way of intermingling source code blocks and natural language to be able to express intent and explain choices taken along the way.

There is some documentation on it on the org mode website, and I have done some very limited experiments with tangling and weaving. Writing an Emacs config from the ground up should be a perfect use case for it, as should any upcoming posts that contain code examples that can be compiled into a standalone program.

Closing thoughts

This is just scratching the surface of what Org mode can do. There is so much I haven’t covered here, including working with tables, org-babel, tags, exporting files, and so forth; but even with just this, Org mode is already a force to be reckoned with.

I can see a bright future where my life is nothing but plain text. 🦄

First Prev Page 1 Next Last