type narrowing · ideas · Zulip Chat Archive

If I match on a tag, I know that subsequent matches can't be that tag (that y : [Bar, Baz]), but the compiler still gives me an exhaustiveness warning.

app "repro"
    packages { pf: "https://github.com/roc-lang/basic-cli/releases/download/0.3.2/tE4xS_zLdmmxmHwHih9kHWQ7fsXtJr7W7h3425-eZFk.tar.br" }
    imports [pf.Stdout, pf.Task]
    provides [main] to pf

main =
  x : [Foo, Bar, Baz]
  x = Foo
  when x is
    Foo ->
      Stdout.line "Foo"
    y ->
      when y is
        Bar ->
          Stdout.line (f y)
        Baz ->
          Stdout.line (f y)

f : [Bar, Baz] -> Str
f = \x ->
  when x is
    Bar -> "Bar"
    Baz -> "Baz"

── UNSAFE PATTERN ────────────────────────────────────────────────── repro.roc ─

This when does not cover all the possibilities:

13│>        when y is
14│>          Bar ->
15│>            Stdout.line (f y)
16│>          Baz ->
17│>            Stdout.line (f y)

Other possibilities include:

    Foo

I would have to crash if I saw one of those! Add branches for them!


── TYPE MISMATCH ─────────────────────────────────────────────────── repro.roc ─

This 1st argument to f has an unexpected type:

15│            Stdout.line (f y)
                              ^

This y value is a:

    [Foo, …]

But f needs its 1st argument to be:

    […]

Tip: Looks like a closed tag union does not have the Foo tag.

Tip: Closed tag unions can't grow, because that might change the size
in memory. Can you use an open tag union?

────────────────────────────────────────────────────────────────────────────────

Richard Feldman (May 07 2023 at 17:51):

yeah, @Ayaz Hafiz wrote up an issue for this (and I always forget where it is) - it's a common question! :big_smile:

Sky Rose (May 07 2023 at 17:52):

I thought it might be a common question, but I didn't see it in the GitHub Issues

Brendan Hansknecht (May 07 2023 at 17:58):

I thought this didn't work without a relayout of the type or gradual typing. I know we have discussed it before it didn't sound like a feature we planned to support, but maybe that changed

Ayaz Hafiz (May 24 2023 at 20:07):

Ayaz Hafiz (May 24 2023 at 20:08):

Artur Swiderski (May 24 2023 at 20:09):

yes I would like to have that feature it seems natural when language is so strict on types, I always know what is underneath so why not to exploit that fact

Ayaz Hafiz (May 24 2023 at 20:10):

This blog post has a discussion of what this feature would look like for a language like Roc and what the tradeoffs are. There is no need for gradual typing, but there would be some cost at runtime to relocate value memory layouts

Artur Swiderski (May 24 2023 at 20:34):

btw this feature is working to some degree because you can divert "wrong" tags to other path

    myset = Set.fromList [Tag1]


    indict =
        Dict.empty {}
        |> Dict.insert "key1" Tag1
        |> Dict.insert "key2" (Gang "problem" )

    content = Dict.get indict "key2"

    when content is
        Ok (Gang val ) ->  Tag1
        Ok someTag ->
            newSet = Set.remove  myset  someTag
            someTag
        _ -> Tag1

Stream: ideas

Topic: type narrowing

Sky Rose (May 07 2023 at 17:49):