[frankpf]

I've been writing an interpreter with Nim and overall the language is really good.

One feature that I'm excited for is DrNim[1]. It's not distributed with the stable version just yet (you have to compile it yourself, but that's very straightforward), but it's supposed to bring refinement types to Nim. These allow you to write things like:

    proc safeDivide(a: int, b: int): float {.requires b > 0.} =
        a / b

and DrNim will check at compile-time that all code paths lead to `b` being greater than 0, e.g.:

    var x = stdin.readLine.parseInt
    safeDivide(1, x) # DrNim will error at compile-time 
    var y = stdin.readLine.parseInt
    if y > 20:
       # no error since DrNim (using Z3) can
       # prove that y is always greater than 0 here
       safeDivide(1, y)

[1]: https://nim-lang.org/docs/drnim.html

[steve_adams_86]

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.

[frankpf]

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...

[mixedCase]

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]

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

[machiaweliczny]

Seems like subset of dependent types to me

[asib]

For me that's a game changer in terms of using Nim for future projects. I've used LiquidHaskell[1] a bit but always been hesitant to use in production just because I'm not confident enough with the Haskell type system. Nim's been on my radar for a while but have held off diving into it for whatever reason, so this is very cool to see.

[1]: https://ucsd-progsys.github.io/liquidhaskell-blog/

[mcintyre1994]

This looks really nice. Do you know if type narrowing is a form of this as well? TypeScript has this pretty neat feature where if you have a variable x of union type A | B and you're in a code path where you've checked if x is of type A then the type is automatically narrowed to A in that code path without you doing any casting etc.

    function num(x: number | Array<string>): number {
      if (typeof (x) == 'number') {
        return x + 10;
      } else {
        return x.length;
      }
    }
    console.log(num(5)) // 15
    console.log(num(["A", "B", "C"])) // 3

I think they just refer to it as type narrowing but it feels kind of similar in concept, so I'm wondering if it's a limited form of refinement types.

[411111111111111]

At first it looks like a guard, but if it's a compile-time guard, it's even better then the original concept!

Reminds me of static analysis tools like sonarqube, but even more integrated

[still_grokking]

Looks more like flow typing than refinement types to me.

The (static) type of 'y' changes seemingly implicitly in the body of the 'if'. It's an 'int' at assignment but needs to be an 'int {.requires ??? > 0.}' (or however the one would write that type literal in Nim), and some flow typing determines than that that cast form 'int' to 'int {.requires ??? > 0.}' is safe in the body of the 'if', and performs this cast implicitly.

The question now is: Is 'int {.requires ??? > 0.}' a type on its own in Nim? It doesn't seem like that as 'b' has 'int' ascribed as its type, and not 'int {.requires ??? > 0.}'.

It's also not dependent typing as the constraint on 'b' can't be an arbitrary function. (I guess, please correct me if I'm wrong; but in that case this typing wouldn't be decidable, even with the help of SMT).

The type of 'safeDivide' could be a "depended function type", tough.

[frankpf]

> Looks more like flow typing than refinement types to me.

I'm not super familiar with the theory behind refinement types and I could be wrong :)

My familiarity with refinement types comes from things like Liquid Haskell and F*. If you look at Liquid Haskell's manual[1], their definition of refinement types seems to pretty much match what DrNim is offering here.

I've never seen the term flow typing used outside of TypeScript-style analysis, where that means narrowing types like `string | null` to `string` inside an `if (x != null)` block.

> The (static) type of 'y' changes seemingly implicitly in the body of the 'if'. It's an 'int' at assignment but needs to be an 'int {.requires ??? > 0.}' (or however the one would write that type literal in Nim), and some flow typing determines than that that cast form 'int' to 'int {.requires ??? > 0.}' is safe in the body of the 'if', and performs this cast implicitly.

I think the hard part is that the language must keep track of these implicit types (e.g. ranges of values an integer can be) inter-procedurally, i.e. throughout the whole call graph.

But yes, the type does change implicitly, and I don't think `int {.requires ? > 0.}` can be expressed as a type in Nim. But I was also under the impression that you can't express that "explicitly" in e.g. Liquid Haskell (I could be completely wrong).

> It's also not dependent typing as the constraint on 'b' can't be an arbitrary function. (I guess, please correct me if I'm wrong; but in that case this typing wouldn't be decidable, even with the help of SMT).

I think you're right. From my understanding, dependent types are more powerful than refinement types but also more cumbersome to use, refinement types can use SMT solvers and are generally more approachable IMO. There's a nice discussion here[2].

[1]; https://ucsd-progsys.github.io/liquidhaskell-tutorial/01-int... (see section 1.2) [2]: https://www.reddit.com/r/dependent_types/comments/ay7d86/wha...

[zie]

This looks amazing, off to read about it now! Thank you!!!

[half-kh-hacker]

I'm curious: Is there anything you're using for parsing in Nim?

[frankpf]

I'm in the process of rewriting the language from typescript to nim, so right now it's a recursive descent parser written in typescript[1]. Typescript generates the textual bytecode and that feeds into a Nim interpreter.[2]

I think I'll keep the recursive descent parser even after rewriting to Nim. It's easy to change the grammar and understand how it works, and I can have good error messages & handling.

IMO the main problem is that right now the code for parsing infix expressions is fairly repetitive, I'd like to eventually use Pratt parsing for that.

[1]: https://github.com/frankpf/kiwi/blob/vm/src/parser.ts [2]: https://github.com/frankpf/kiwi/blob/vm/src2/src/interpreter...