Comment by steve_adams_86 | Hacker News Reader

Comment by steve_adams_86 | Hacker News Reader

Parent Full thread

I didn't know that this is called a refinement type! I've been wanting it badly, both in Nim and in Rust. Now I have a way to search for what I'm looking for to learn more.

Would it be possible to use this to ensure a string matches a certain pattern? For example, maybe I want the string to look like a phone number or zip code. I know I can use an abstraction to do this and have some level of safety, even without a statically typed language, but I love the idea of implementing that with primitives. As far as I know it isn't really a thing though. I'm assuming a refinement is only really a refinement of a type within the same system, and doesn't allow for special logic like pattern matching. That would be amazing though.

I've spent so much of my career working with dynamic languages, it's hard to know exactly which tools are available to me with these kinds of type systems. I love it though. Learning to leverage types has been such a fun shift.

I don't think you can use _refinement types_ for this, at least not as of now (e.g. you can't do {.requires validEmail(email).}), but you can use distinct types[1] in nim to model what you want:

    type Email = distinct string

Now Email is a type that is incompatible with string, even though its runtime representation is a string (i.e. no additional overhead). To convert a string to an Email, you can call Email("a"). In real-world code, you would call that constructor only in a few "safe" functions:

   # I'm raising an exception, but you could use an option or a result type
   proc validateEmail(str: string): Email =
      if email.contains("@"):
          return Email(str)
      raise newException(InvalidEmail, "not valid")

Then, in your client code you can have:

    proc createUser(email: Email, password: Password) =
       ...

And the type system guarantees that you only call createUser with "Email"s, not plain strings. Of course, you have to be dilligent not to use the Email constructor directly and instead use the validateEmail function to create "Email"s.

[1]: https://nim-lang.org/docs/manual.html#types-distinct-type

EDIT: The sibling comment mentioned io-ts.

The pattern for doing this in io-ts (and TypeScript in general) is very similar to Nim, although they call it "branding"[2] as it abuses the structural type system to simulate nominal typing.

[2]: https://michalzalecki.com/nominal-typing-in-typescript/#appr...

Not sure about Nim, but you can do this in TypeScript. There's even a library called io-ts that allows you to create composable types of this form for runtime validation which then turns the result into proper types.

Wow, that's really helpful. I'm working on a TS project at the moment and that might come in handy. Thanks!

Seems like subset of dependent types to me

Reply on news.ycombinator.com