Copilot + Static Typing = <3

I’ve been using Github Copilot for a while to write Haskell (and Typescript) for the TextQL backend MVP, as well as mkprompt. To my surprise, it’s been a good experience, despite Haskell not being one of Copilot’s officially supported languages. Just look at this!

Reason 1: Type Checking Invalid Completions

The best part about having a powerful type system is that the type checker can catch certain classes of errors before the program is run. For example, in the above snippet the type of ServerState’s websocketConnection field is MVar (Maybe Connection). MVar is a synchronized mutable variable, Maybe is Haskell’s optional type, and Connection is a WebSocket connection. The type system will catch these common errors before the program is even run:

• The MVar needs to be dereferenced before using the value stored in it with readMVar
• The result is a Maybe, so the empty case needs to be handled
• websocketConnection is a field on ServerState, not on the request or some global variable.
• The request needs to be encoded into a bytestring before sending it across the websocket connection.

Unsurprisingly, catching errors before runtime also extends to Copilot completions. That means I can be a bit more aggressive accepting completions, knowing that the type checker will catch any obvious errors. And when an error does get raised, the type mismatch is typically a great starting point for fixing up a completion that’s mostly right. Of course, there are bugs that won’t be caught by the type checker, so blindly accepting completions is still a bad idea even after type checking. But we can mitigate this problem by investing more into robust type representations, the classic “make invalid states unrepresentable”. If you were writing shop software, you could represent price and quantity of a product each with their own types, rather than using a simple numeric type for both of them. This prevents both you and Copilot from mixing up price and quantity in the code, and in many languages comes with zero runtime cost.

Reason 2: Type Signatures are Good Prompt Engineering

Anyone who’s played around with LLM-based tools knows that a good prompt is a big part of getting the model what you want it to do. A good prompt includes:

1. What you want the language model to accomplish.
2. Relevant context to help the model complete that task.

Type signatures simultaneously accomplish both of these! Let’s say that I want to write a function that takes the value from an MVar if it’s present, otherwise returning a default value. All I do is write the type signature and watch Copilot do the rest:

Or perhaps, I want to use a per-type default value (provided by the Data.Default module) instead of a user provided one. All I have to do is change the type signature, and the completion changes as well to reflect the new goal:

And going back to Reason 1, I can easily verify the validity of either implementation by running the type checker to see if the definitions matches the provided signature. In the second case, it complains that Default is not in scope, so I add import Data.Default to the top to fix the error.

Reason 3: Copilot automates Type System boilerplate

A downside of typed languages is that they come with a lot of boilerplate for writing type signatures, type declarations, type casts, instance/interface declarations, and in the case of Haskell, newtype construction and destruction. This extra boilerplate tends to persist even with type inference. Copilot can help automate much of this boilerplate, making working with typed languages more efficient and enjoyable.

When declaring request and response types I’m declaring Show, Generic, FromJSON, and ToJSON every single time, so Copilot gets it right every single time (because I did it 10 other times in the same file.)

Conclusion

I didn’t expect Copilot to be good at writing Haskell. To my surprise, it not only writes Haskell but synergizes with the type checker to a point where I like it more than using it with untyped JS/Python. A lot of the same benefits extend to my Typescript code as well, and I expect it’d be the same for Rust too. On the other hand, I’m mostly writing web apps. Copilot might be worse if you’re writing code that pushes the limits of the type system, but still useful since even these use cases have automatable boilerplate. Regardless, the synergy between Copilot and type systems is worth exploring and can greatly improve the efficiency and enjoyability of progamming.