haspar.us

Syntax Highlighting

Oct 27, 2019 · ☕ 4 min read

Hidden example

Lorem ipsum, dolor sit amet.

/** @jsx jsx */
import { graphql, Link, useStaticQuery } from "gatsby";
import { Themed as s, jsx } from "theme-ui";

import { BlogPostsQuery } from "./__generated__/BlogPostsQuery";
import { Header, Root, theme } from "../components";
import { BlogpostDetails } from "../components/BlogpostDetails";
import { Seo } from "../components/Seo";

const IndexPage = () => {
  const { allMdx } = useStaticQuery<BlogPostsQuery>(graphql`
    query BlogPostsQuery {
      allMdx {
        nodes {
          frontmatter {
            title
            spoiler
            date
          }
          fields {
            route
            readingTime
          }
        }
      }
    }
  `);

  return (
    <Root>
      <Seo titleTemplate="%s" />
      <Header />
      <s.h1 sx={{ mt: 3, mb: 4 }}>haspar.us</s.h1>
      <s.p>
        Howdy! I'm Piotr Monwid-Olechnowicz and this is my personal blog.
      </s.p>
      <main>
        {allMdx.nodes.map((node, i) => {
          const { frontmatter, fields } = node!;
          const { title, spoiler, date } = frontmatter || {};

          return (
            <article key={i}>
              <header>
                <s.h3 sx={{ marginBottom: "0.4375rem", color: "text" }}>
                  <Link
                    to={fields!.route!}
                    sx={{
                      ...theme.styles.a,
                      color: "currentColor",
                    }}
                  >
                    {title}
                  </Link>
                </s.h3>
                <BlogpostDetails
                  date={date}
                  timeToRead={fields!.readingTime}
                />
              </header>
              <s.p>{spoiler}</s.p>
            </article>
          );
        })}
      </main>
    </Root>
  );
};

export default IndexPage;

Text below is taken from /refinement-types blogpost

How can I use them? What will I gain?

I’ve refined the number into Even during my Wrocław TypeScript talk.
Having a type for even numbers doesn’t sound really useful but the idea stays the same for real world types with complex names copied from Jira.

We can call the predicate once and if it’s true, we remember this fact in the type system to avoid accidental errors.

Example time

Almost real example

Assume we’re building a form in which users can enter a list of emails into a textarea to send activation links to give their friends write permissions for the app (let’s say it’s a CMS).

We validate these emails once, and if they’re all valid, we save them, and later, few steps further in the form, we send our activation links. Few days later, we get a new requirement — the user should be able to edit the data at the last step of the form. Cool, the form is pretty long, we understand that it can be useful. Several lines of code and we’re done. We go home happy about the good code we pushed. Next morning we see a new issue in the tracker — “Validate emails after the user does final edits” — We totally forgot about the validation.

How could we save the day with a refinement type?

  • Create a subtype of string called ValidEmail, such that string is not assignable to ValidEmail.
  • Hold already validated emails in a list of type ValidEmails.
  • Now you can’t push a string to a list of already validated emails ✨
  • Change the type of sendEmail function from (email: string) => void* to (email: ValidEmail) => void.
    It doesn’t make sense to send an email to "🦄🐵💣" which is a perfectly valid string.

( * ) or IO, Result, choose your favorite.

Yeah right, but how can I create this “ValidEmail” type?

However you want! It’s just an idea from type theory and you can implement it in your favorite way. Few ideas:

  • you can go full OOP and extend a String,
  • use nominal typing and leave no runtime trail (my favorite option),
  • put the string into a value object, because ValidEmail doesn’t even have to be a subtype of string.
    The key is that string is not assignable to ValidEmail, because we want to ensure validation.

User defined type guards

We can use TypeScript’s user defined type guards to tell the compiler that our predicate checks the type and this is exactly what we’re interested in when we talk about refinements.

Let’s empower our isValidEmail predicate by changing its signature from (s: string) => boolean to (s: string) => s is ValidEmail.

Takeaways

  • Refinements are not implemented in TypeScript, but you can make them in userspace.
  • You can use nominal typing to make sure your refinements have no runtime trail (except predicate checks).
  • You can use them to encode facts about your data in the type system.

Further reading

This is mostly a reading list for future me, but I hope you can also find it interesting.