Fill typed holes with ease. Generate idiomatic Haskell solutions using pattern matching, class methods, and even recursion.See it in action
Introduce complete case statements for any variable in scope. Automatically expand top-level splits into multiple equations.See it in action
Wingman is built on LSP, so it works out-of-the-box in most editors. Just hover over a typed hole to get started!
Wingman for Haskell automates away the old hole-driven design workflow. You probably know the one — where you put down a hole, and ask the compiler what type it has. After a little bit of thinking, you add a little bit of code around the hole, and then ask the compiler again. Over time, the expression gets written, but it seems like the compiler is doing most of the work. Sometimes it can feel like all you're around for is to write down what the compiler says.
Instead, imagine a world where you can just ask "hey, fill in this hole for me, please." Wingman is that world. A typechecker is nothing but a series of rules that determine what type an expression has. By running these rules backwards, we can instead look at what expressions could produce a certain type. Search through a few thousand well-typed expessions, score them, and give back the best one.
As you might expect, running the search is the easy part. Keeping it
fast and making sure it returns good results is where the challenge comes
in. And often, these goals are in tension. Always returning
undefined would certainly be well-typed and fast, but it's
clearly not what you had in mind.
Wingman tries really hard to write the code you would have written youself. It prefers linear solutions, ensures productive recursion, and has a reasonable knowledge of common Haskell idioms — including eta-reduction and every-day combinators.
Of course, sometimes human ingenuity is necessary to get a function out the door, and no automated tool can do the job. Even when you're not asking Wingman to fill holes for you, it can still help. By running small pices of the code synthesizer, it can perform case splits, introduce lambdas and, in general, help move you closer to the important part of the problem.
Make sure you have the Haskell Language Server installed, then try writing out the following:
my_foldr :: (a -> b -> b) -> b -> [a] -> b my_foldr = _
Simply hover over the
_ and run the
Attempt to fill
hole code action (under in VSCode.) Prepare to be
Attempt to fill hole — try to synthesize a complete solution to the current hole. Fails if it can only make partial progress.
Case split on — pattern match on
a local variable. Comes in many varieties, for creating homomorphisms and
Introduce lambda — add a lambda abstraction, binding every function argument.
Refine hole — make one step in the "obvious direction." Introduces a lambda or uses a data constructor if it's the only one that can match.
Split all function arguments — make a function head for every possible combination of its arguments.
Use constructor — use the specified constructor, adding new holes for each argument.
The Haskell Language Server is best thought of as a platform for writing specific tools. It provides a bridge between the editor and the compiler, and ensures that build artifacts are up to date.
Wingman is built on top of HLS, and that's the reason it doesn't require dedicated editor support. We're bundled together in the spirit of symbiosis and convenience — Wingman provides some features otherwise lacking in HLS, but also wouldn't be possible without HLS.
No, just better branding.
Internally, the project is still known as
hls-tactics-plugin, due to its intentions to be tactic
meta-programming tool for Haskell. On the inside, Wingman makes heavy
use of Reed Mullanix's excellent refinery
tactic library for doing its code synthesis.
Maybe one day we'll get to tactic meta-programming. But for now, this
is just an implementation detail, and
isn't exactly a name that inspires enthusiasm.