Forem: Denis

My approach to Neovim

Denis — Wed, 05 Jul 2023 22:45:46 +0000

The story

I always found myself looking towards those terminal based modal editors like Neovim, but every time one thing really held me behind: the amount of time I needed to put into configuration. You have to spend quite a lot of time to configure a stable feature-complete version of Neovim, and it actually doesn't quite pay off in the beginning, because it's so tempting to stay with your comfy VS Code and don't waste time. I tried to configure Neovim like 3 times in my entire career, every time with a goal to build a complete editor, but having successfully accomplished it only with my latest attempt.

When I was most disappointed configuring Neovim, I have found Helix, a Neovim alternative with lots of features built in. It really made me interested when I first heard about it. Because configuration is minimal, I could focus more on the editing itself without thinking much about what plugin I need to install next, and so Helix became the editor which introduced modal editing to me. When using Neovim in the beginning, I was more focused on just making it look good ("tUrn yOuR vIm iNto a fUlL fEaTuRed IdE" kind of videos, you know), but I didn't study much the "vim way" of editing. I was using only some keys like hjkl, maybe some w and b, sometimes mouse, which by themselves are very far from making the editing experience productive. Though I eventually left Helix, it contributed much to how I approached modal editing.

After becoming comfortable with Helix, some crazy idea popped up in my head: "now if I am good at Helix, and Helix is like Neovim, what if I try to configure Neovim similarly to Helix? Then, with powerful plugin system, I could gradually improve my experience, the thing I cannot do with Helix which lacks plugins". After thinking a little, I've cleaned my old ~/.config/nvim directory, and got my hands dirty. And to my very surprise, the idea worked like a charm: I actually went to a minimally viable working Neovim config with essential plugins and features in a single init.lua file really, really fast! It took me nearly a couple of days to configure without much pain, unlike my any previous attempt. Great!

I think why it really worked for me this time is because my requirements for an editor were much more "real" when I switched from Helix to Neovim. When you switch from something like VSCode, you want those features that GUI editors have, which are mostly very different from what you get in modal editors. You switch the editing paradigm which you haven't yet understood and accepted, and that's why you expect something from Neovim which it cannot provide (for good though). That's why some people misinterpret Neovim as being an IDE, because they want to see it as an IDE, which eventually lead to frustration.

What I learned from this is that Neovim is a different code editor. And if you want to learn it well, you should approach it differently, as a new thing, without bringing your old habits from traditional editors.

The approach

Below are the points that changed Neovim for me. Having all these makes me really happy with my current configuration.

1. Keymaps

I really like the way keymaps are organized in Helix. So my keymaps are organized in a similar way.
Basically, I have 2 types (in Helix they are called "modes") of keymaps - goto and space keymaps. Goto are those keymaps which make you jump somewhere, like "Go to definition", "Go to next buffer", etc. Space are general purpose (space because it's the leader key).

My space keymaps (not exhaustive):

My goto keymaps:

2. Much of Telescope

You can use Telescope for so much of things! File browser, notification history, keymaps browser, filetypes picker, diagnostics, git, DAP command picker, and so on. It's a such fundamental tool that I can't imagine using Neoivm without it.

It just fits so good with Neovim. I don't really like split windows because they are somewhat clumsy in terminal editors, that's why I don't have nerdtree and don't use nvim-dap-ui: I find such "util splits" not so pleasant to work with. Telescope file browser and dap.ui.widgets are just much better (though the latter is not Telescope, but neither is a split window). And a lot of things can be implemented with Telescope. It contributes a very huge part to overall editing experience.

Telescope File browser

Git commits with Telescope

DAP commands with Telescope

3. Enhanced movement

There's not much to say: using leap.nvim adds up to editing speed on mid-range movements, can't really edit in nvim without it.

4. Nice UI

Not related to "the approach", but made me enjoy the editor much more

Normal mode commands, search, code actions at screen center with nice round corners

Pretty notifications

5. Use other tools

I think Neovim is a very powerful editor, but it's still and editor, and sometimes you need more than this. You have so much CLI tools, and the power of pipes, use it to complement your Neovim experience. The following are just some from the top of my head:

jq for json manipulations (using nvim pipes with jq is really cool, for example, you can pipe visually selected json string to jq which will effectively format it)
tmux or zellij for workspace management
ast-grep - helps so much in refactoring.
and pretty much anything you can use in your terminal.

6. No abstraction in config

While it would be quickly tempting for perfectionist minds to start writing custom functions for mapping keys to use everywhere ("wait, nvim-cmp has its own keymaps table which differs from standard vim.keymap.set function? Hell no, I must write a function that abstracts it away!"), I saved so much time avoiding perfectionism and abstractions by writing configuration in a "dumb" way. If you look at my config, you will notice that it's not quite smart, there are no custom functions, some settings I just copy-pasted from somebody else's config. I think you should not waste time on this, unless you are writing a Neovim distro (God be with you: never found them actually any useful).

7. Start with starting configs if you are lost

Initially, I just copy pasted this config and deleted everything I didn't need, gradually adding things adding up. I don't really like Neovim distributions, though you can use them on the early stages of your journey, but make sure to jump off that ship when you feel more confident.

Conclusion

I've learned that you get most power from Vim if you approach it the right way. The editor makes you customize your experience as you want, and it really feels different when you get it. Understanding Neovim got me starting my journey of customizing the perfect dev workflow, and I help this article will help you too. :)

Link to my config: https://github.com/thedenisnikulin/nvim

Small sum types in Golang

Denis — Wed, 21 Jun 2023 20:13:13 +0000

You can model sum types in golang as following

import "github.com/samber/mo"

// tags and their types
type (
    Id    int
    Phone string
    Email string
)

// UserKey is a sum type
type UserKey = mo.Either3[Id, Email, Phone]

I find this implementation to be quite minimal and less clumsy than alternatives. Sure, you don't get nice exhaustive pattern matching. Also, type inference gets in the way when instantiating UserKey (though you can wrap it in constructor functions). But expressing your intent using types still makes your code much more convenient and easier to understand.

Type-level Bubble Sort in Rust: Part 2

Denis — Wed, 16 Mar 2022 17:36:57 +0000

Hello everyone! In the previous post from this series we discussed traits, type-level number representation, and implementation of basic type-level computations. The topic of this article is type-level lists. Make some tea or coffee and let's dive into the details!

Image source: link

Type-level lists

There's a data structure that you are most probably familiar with - a linked list. Each element of a linked list stores a value and points to the next element, and the last element of such list points to nothing. This data structure is easily represented with recursion, where the "nothing" is the base case, and an "element" is the recursive case. We actually will work with recursion quite a lot (the comparison of type-level numbers was also based on recursion), so you may need to learn to understand it.

The way we can define the list in Rust:

struct Nil; // a "null" ref
struct Cons<H, T>(H, T); // value and a ref to next element

The way we can use it in Rust:

Cons<Succ<Zero>, Cons<Zero, Cons<Zero, Nil>>> // a typical type-level list
Cons<Zero, Nil> // smol type-level list
Nil // the smolest of them all

The above examples are the same thing as [1, 0, 0], [0], and [] respectively on the value level.
The names cons and nil are terms from functional programming, but don't let them confuse you, it's just a fancy way of saying things (wikipedia page if you're curious). Also, the type parameters are named after terms head and tail.

Defining basic computations

When implementing bubble sort, we will need a lot of helper "functions" for things like concatenation, swapping, and some others operations on list's elements. Let's define a trait that will represent an operation for prepending a number to a list.

// the naming "ComputeX" is used only for convenience,
// we will have a type alias named simply "Prepend" later on.
trait ComputePrepend<N> {
    type Output;
}

The number N will be prepended to the list for which this trait will be implemented.

The implementations:

impl<N> ComputePrepend<N> for Nil {
    type Output = Cons<N, Nil>;
}

This is quite simple: we prepend arbitrary N to Nil and that results in Cons<N, Nil>.

impl<N, H, T> ComputePrepend<N> for Cons<H, T> {
    type Output = Cons<N, Cons<H, T>>;
}

Here we prepend N to Cons<H, T>. This also seems not so hard to get.

Let's define the type alias:

type Prepend<N, L> = <L as ComputePrepend<N>>::Output;

and test it:

The compiler inferred Cons<Zero, Cons<Succ<Zero>, Nil>> for us, great! Now we have a basic understanding of numbers, lists, and trait multidispatching. We can use it to write the rest of helper traits for our bubble sort algorithm. But first, let's define the algorithm itself.

Recursive bubble sort algorithm

Here's the implementation of value-level bubble sort algorithm in pseudo-code with heavy usage of recursion.

fn bubble_sort(arr)
    if (arr.len() == 0) return arr
    bubbled = bubble(arr)
    return prepend(bubbled.head, bubble_sort(bubbled.tail));

fn bubble(arr)
    if (arr.len() == 0) return arr
    return prepend(arr.head, swapIfLess(arr.head, bubble(arr.tail)))

fn swapIfLess(head, tail) -> arr // swap tail[0] with head if tail[0] < head
fn prepend(head, tail) -> arr //...

Quick code explanation. In the function bubble , we move the least element of arr to the very beginning of the list (i.e. to the head). Then we cut the head off of the arr (since we consider the head sorted) and do the same bubble thing on the tail and again cut the head of that tail off, until the length is 0, and then we construct the whole array by prepending the heads back to their places.

Notice that the implementation is adapted so that it is more convenient for us to express the logic on traits. For example, instead of using swapIfLess it should be written as if (...) swap(...). Although we could define some traits to define if-else logic, I find it cleaner for now to settle for swapIfLess thing.

Actually, there's a problem with this approach. Look at this line:

return prepend(arr.head, swapIfLess(arr.head, bubble(arr.tail)))

The code assumes that arr is passed around by reference, like in javascript for example. For instance, if swapIfLess(arr.head, ...) function mutates arr.head as a result of swapping, the head from prepend(arr.head, ...) is also mutated. We can't mutate anything on the type level, so we need to adapt the implementation for this case.
To solve this, I will define conditional swap and prepend functions as one trait.

It doesn't mean that there's no other workaround for this problem, if you have a better solution, I would be happy to see it!

Bubble sort helper traits

Let's define that big-arse SwapPrepend trait:

trait ComputeSwapPrepend<E, H> {
    type Output;
}

Where E is for "equality" and H is for "head". We will define implementations of this trait for different equality types, so for each equality type the computation result will be different (i.e. a decision "to swap or not to swap" depending on the equality of head and tail[0]).

// For Nil, we just prepend the `Head`
impl<E: Equality, Head: Nat> ComputeSwapPrepend<E, Head> for Nil {
    type Output = Cons<Head, Nil>;
}

// When `Head` and `A` (i.e. 'head' and 'tail[0]' as in the
// pseudo-code example above) are equal, also just prepend the `Head`
impl<A, Other, Head> ComputeSwapPrepend<EQ, Head> for Cons<A, Other> {
    type Output = Cons<Head, Cons<A, Other>>;
}

// When `Head` > `A`, just prepend
impl<A, Other, Head> ComputeSwapPrepend<GT, Head> for Cons<A, Other> {
    type Output = Cons<Head, Cons<A, Other>>;
}

// When `Head` < `A`, we finally swap and prepend.
impl<A, Other, Head> ComputeSwapPrepend<GT, Head> for Cons<A, Other> {
    type Output = Cons<A, Cons<Head, Other>>;
}

type SwapPrepend<E, H, L> = <L as ComputeSwapPrepend<E, H>>::Output;

Next, we define one more comparison trait, but this time it will compare a natural number with a list (i.e. with the list's head). It will help us to compare numbers when we will be implementing a trait for Cons<Head, Tail> where we can't simply get the first element of Tail to compare it with the Head with the old Compare trait, so the new Compare trait will help us with resolving the Tail's first element.

trait ComputeCompare<Rhs: Nat> {
    type Output: Equality;
}

// This impl is only used for completeness.
// We will use `Compare` trait in tandem with `SwapPrepend` trait,
// and `<Nil as SwapPrepend<T, H>>::Output` thing doesn't 
// compare anything and only prepends.
// So the `Output` type doesn't matter in this context.
impl<Num: Nat> ComputeCompare<Num> for Nil {
    type Output = LT;
}

// Just compare `Head` with `Num`.
// `CompareNat` is the old natural number comparison trait.
impl<Head, Num, Tail> ComputeCompare<Num> for Cons<Head, Tail>
    where Head: Nat + ComputeCompareNat<Num>,
          Num: Nat + ComputeCompareNat<Head>,
          Tail: List
{
    type Output = CompareNat<Head, Num>;
}

type Compare<N, Ls> = <Ls as ComputeCompare<N>>::Output;

Above are also some trait bounds for the traits which we should specify to make the situation clear for the compiler.

They are pretty simple:

trait Nat {}
impl Nat for Zero {}
impl<N: Nat> Nat for Succ<N> {}

trait List {}
impl List for Nil {}
impl<H: Nat, T: List> for Cons<H, T> {}

trait Equality {}
impl Equality for EQ {}
impl Equality for LT {}
impl Equality for GT {}

And finally, some little things which will come in handy:

type HeadOf<L> = <L as ComputeHead>::Output;
type TailOf<L> = <L as ComputeTail>::Output;

Their functionality is quite simple, try to understand how they are implemented by yourself.

Bubbling

Now, we are on the key part of the algorithm.

trait ComputeBubble {
    type Output;
}

impl ComputeBubble for Nil {
    type Output = Nil;
}

impl<Head, Tail> ComputeBubble for Cons<Head, Tail>
    // Some big & scary bounds
    where Head: Nat,
          Tail: List + ComputeBubble + ComputeCompare<Head>,
          <Tail as ComputeBubble>::Output: ComputeSwapPrepend<<Tail as ComputeCompare<Head>>::Output, Head>
{
    type Output = SwapPrepend<Compare<Head, Tail>, Head, Bubble<Tail>>;
}

type Bubble<Ls> = <Ls as ComputeBubble>::Output;

The Output type computation is not that difficult, try to understand how it does the job by yourself.
You can see that the 3rd trait bound is quite ugly. It just means something like "The result of bubbling the Tail must support swap & prepending the Head".

Bubble sorting

trait ComputeBubbleSort {
    type Bubbled: List;
    type Output: List;
}

impl ComputeBubbleSort for Nil {
    type Bubbled = Nil;
    type Output = Nil;
}

impl<Head, Tail> ComputeBubbleSort for Cons<Head, Tail>
    // Oh geez...
    where Head: Nat,
        Tail: List + ComputeBubble + ComputeCompare<Head> + ComputePrepend<Head> + ComputeBubbleSort,
        <Tail as ComputeBubble>::Output: ComputeSwapPrepend<<Tail as ComputeCompare<Head>>::Output, Head>,
        <<Tail as ComputeBubble>::Output as ComputeSwapPrepend<<Tail as ComputeCompare<Head>>::Output, Head>>::Output: ComputeHead,
        <<Tail as ComputeBubble>::Output as ComputeSwapPrepend<<Tail as ComputeCompare<Head>>::Output, Head>>::Output: ComputeTail,
        <<<Tail as ComputeBubble>::Output as ComputeSwapPrepend<<Tail as ComputeCompare<Head>>::Output, Head>>::Output as ComputeTail>::Output: ComputeBubbleSort,
        <<<<Tail as ComputeBubble>::Output as ComputeSwapPrepend<<Tail as ComputeCompare<Head>>::Output, Head>>::Output as ComputeTail>::Output as ComputeBubbleSort>::Output: ComputePrepend<<<<Tail as ComputeBubble>::Output as ComputeSwapPrepend<<Tail as ComputeCompare<Head>>::Output, Head>>::Output as ComputeHead>::Output>
{
    type Bubbled = Bubble<Cons<Head, Tail>>;
    type Output = Prepend<HeadOf<Self::Bubbled>, BubbleSort<TailOf<Self::Bubbled>>>;
}
type BubbleSort<Ls> = <Ls as ComputeBubbleSort>::Output;

Again, the Output type is not what scares, but the trait bounds. Actually, I didn't write them by myself, these bounds where suggested by compiler. We can think of them as just a thing to make the compiler satisfied about the types. You can run rustfmt on the code to prettify it if you want to dig into what, for example, the last bound is for, but it can be briefly described as "the result of computing trait A must implement trait B", but following the whole chain of trait invocations.

As I know, there isn't a way to specify an implied trait bound (that is, we know that the result of BubbleSort<TailOf<Bubble<Cons<..>>>> is a List, but for the compiler to be satisfied we must write the whole chain of invocations like <<Cons<..> as Bubble>::Output as TailOf>::Output as BubbleSort and etc in the trait bounds) in current version of Rust, but there's an RFC for this thing which is not implemented yet.

Testing

The computed natural number types were expanded, but you can see that the list became sorted (the N1, N2 types are just aliases for Succ<Zero> and Succ<Succ<Zero>>).

Conclusion

The implementation is far from being perfect, but at least it works. There are ugly trait bounds which are completely unreadable, and I don't know any way to simplify them. But it's enough to show what the Rust's type system is capable of.
It is not worth to say that this variation of algorithm is not practically useful. But it is a good way to challenge your mind and try something extraordinary!

The full source code:

https://github.com/thedenisnikulin/type-level-sort

Links

A much more practically useful type-level programming in Rust
A macro to define type-level logic with value-level syntax in Rust
Type-level Brainfuck in Rust
"Gentle Intro to Type-level Recursion in Rust"
Type-level registers in Rust
Type-level quicksort in Scala"
Type-level sorting algorithms in Haskell
A repo with functions and algorithms implemented purely on types in TypeScript

Type-level Bubble Sort in Rust: Part 1

Denis — Thu, 03 Mar 2022 09:15:09 +0000

In this series of articles, we are going to implement bubble sort algorithm on the type level using (abusing) Rust's type system, which is Turing-complete.

The goal I want to accomplish by these articles is to help you understand what type level programming feels like, try to clear what's behind of all these "traits" and "impls", and to show what Rust's type system is capable of.

Before jumping in, you may need to have a basic understanding of Rust programming language (although the understanding of some FP language like Haskell or Scala should be also good enough).

Basically, type level programming allows us to carry the computations to the compilation phase where the compiler infers relationships between types, rather than computing the values during the program runtime.

How do we express conditional logic with types?

We will use the power of traits. Traits are just like interfaces in C#/Java, except that you can implement traits for existing types (so the mindset is not "a type implements this interface" but rather "there's an implementation of this trait for a type").
Combined with generics, it gives us an ability to write multiple trait implementations for a single type just with different generic type arguments, allowing the compiler to decide what implementation must be picked for a particular case. Let's call it multidispatch.

We will see this in practice a bit later, for now, let's focus on numbers.

Numbers

Well, how do we represent type-level numbers? We can certainly declare a lot of structs for each possible natural number like struct Num1; struct Num2; etc but that's just not a good idea (and is actually impossible since there are infinite amount of natural numbers). We will use Peano number encoding.

Simply put, natural numbers are just all non-negative numbers counted from 0 to infinity one by one. There comes the hint! One comes after zero, two comes after one, so we can say that number 1 is a successor of 0, and number 2 is a successor of successor of 0. This is how Peano numbers encoding work!

In Rust code it's going to look this way:

struct Zero;
struct Succ<N>(N);

For example, in order to represent number 4 we will write this:

Succ<Succ<Succ<Succ<Zero>>>>

Number comparison

Next important thing about numbers in context of sorting is comparison.

Peano numbers comparison is based on the following rules:

0 <= X for every X
Succ(X) >= Succ(Y) if X >= Y

For example, let's try to calculate whether 2 is less than 3 with the help of the above rules. Is 2 less than 3? We can't certainly answer, and according to the 2nd rule we need to compare their predecessors. Is 1 less than 2? Again, we can't say. Is 0 less than 1? Yes, it is true according to the 1st rule. We have proved that 2 is less than 3.

Let's code it.

We will use traits and associated types. Look at this piece:

trait Compare<Rhs> {
    type Output;
}

This trait will be implemented for natural numbers.
Also, we will see multidispatch in action.

Let's write an implementation for the 1st rule of comparison:

// Some zero-sized types for representing equality
struct EQ;
struct LT;
struct GT;

// we've got to impls since we have no "less or equal to" type
impl Compare<Zero> for Zero {
    type Output = EQ;
}

impl<A> Compare<Succ<A>> for Zero {
    type Output = LT:
}

The meaning of these impls are Comparing Zero with Zero produces EQ and Comparing Zero with Succ(A) produces LT. As you can also see, the type for which the trait is implemented is used as left hand side of comparison, and the type parameter Rhs is the right hand side.

In order to invoke the implementation, we need to write

<Zero as Compare<Zero>>::Output

which means "get an implementation of trait Compare for Zero, and get the associated Output from it".

As you can see, the compiler inferred the exact type that we needed. We have just made a computation on type level!

As you have seen, the <Zero as Compare<Zero>>::Output thing is kind of awkward (imagine if there are even nested invocations), and we can actually simplify it with the type aliases:

type Cmp<Lhs, Rhs> = <Lhs as Compare<Rhs>>::Output;

It makes the code MUCH more readable, and allow us to look at traits as just functions operating on types. The generic type parameters (Lhs, Rhs) are function's parameters, associated types are what function returns (Output).

Notice, that I didn't write the implementation for comparison between Succ<A> and Succ<B>. Let it be your home assignment (you can see the solution in the code repository, the link is down below). A hint: it involves recursion.

Thank you for reading the article, that's all for today! In the next part of the series, I am going to discuss type-level lists. Please, leave comments below if you like the article and in case you spotted any mistakes or haven't understood something, I am open for critics and discussion!

The project's source code:

https://github.com/thedenisnikulin/type-level-sort

[ VIM ] Cyberpunk 2077 Color Theme

Denis — Fri, 15 Jan 2021 17:54:09 +0000

Try out: https://github.com/thedenisnikulin/vim-cyberpunk