3 ms·

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

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.

machiaweliczny 6y ago
Seems like subset of dependent types to me
mixedCase 6y ago
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.
- steve_adams_86 6y ago
  Wow, that's really helpful. I'm working on a TS project at the moment and that might come in handy. Thanks!
frankpf 6y ago
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 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/#approach-4-intersection-types-and-brands https://michalzalecki.com/nominal-typing-in-typescript/#appr...

machiaweliczny 6y ago

Seems like subset of dependent types to me

mixedCase 6y ago

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.

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

frankpf 6y ago

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 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/#approach-4-intersection-types-and-brands https://michalzalecki.com/nominal-typing-in-typescript/#appr...