A quick-and-dirty check that a type-level string starts with a certain prefix

🎉I am writing these notes at Brick, a magical mystery no-bullshit publishing platform. Turns out writing goes much faster when I don't have to hit “Publish” or do git commit.

You can use it too — check it out at Brick.do.

Problem statement

For some nefarious purposes, you want to check that a type-level string, "id-13", starts with "id-". You know the prefix statically. You want this:

> :kind! IsId "id-13"

IsId "id-13" :: Bool
= 'True

What do you do?

Solution

Here's a trick: you can't deconstruct type-level strings easily, but you can compare them. So you just need to check that "id-" ≤ s < "id.", because . is the next char after -. Let's do this.

Necessary stuff:

> :set -XDataKinds -XTypeOperators
> import GHC.TypeLits (CmpSymbol)
> import Data.Type.Bool ((||), (&&))
> import Data.Type.Equality ((==))

The implementation:

type IsId s =
    "id-" == s ||
    (CmpSymbol "id-" s == LT && CmpSymbol "id." s == GT)

Test:

> :kind! IsId "id-13"
IsId "id-13" :: Bool
= 'True

> :kind! IsId "foo"
IsId "foo" :: Bool
= 'False

P.S.

I said “you can't deconstruct type-level strings easily”, but it's still possible using an extension of this approach — take a look at Parsing type-level strings in Haskell and the symbols library.

The trick above is just a quick-and-dirty (but faster) solution.