Idea: Extensible Union types and benefits they bring for real world Elm code

Thanks for the answer! I’m not sure if I was clear about my intent with the comment. I just wanted to point out that I think there is the subproblem of enabling anynomous union types that you can give inline in a function type declaration. (It’s simply implicit in your blog post, e.g. when you talk about extensible unions being type aliases and not types anymore, which means that we give a new name to a valid, anonymous type declaration.)

I definitely see the appeal of extensible sum types. My goal was not give a counterargument, it was just to break the problem down into two smaller problems. :wink:

Your point about type inference is really good, I hadn’t thought about that. Even though inferring a more general, extensible record type is really helpful, it would be possible without. It could just be the tightest type. So f record = record.someField could be a f : { someField : a } -> a . (Luckily, the actual type of .field0 is an extensible .field0 : {a | field0 : b} -> b.)

Similarly, anonymous sum types would enable this type inference:

try =
  if doACalculation < 0 then
     @Negative
  else
     if isOnline then
       @Successful
     else
       @Offline

--> try : @Negative or @Successful or @Offline

If I had written a declaration try : @Negative or @Successful, it would see that there is an extra case not present and could warn me. If I write try : @Negative or @Zero or @Successful or @Offline, it would fail due to non-exhaustiveness.

As for your example value = @SomeTag 1, why wouldn’t it be the singleton value : @SomeTag Int?

All of these are points you cover in the blog post, and this example does not use extensibility. That’s why I felt it might be interesting to split the problem into anonymity and extensibility.

-- Note the blog post assumes that variant tags must have 1 argument,
-- but that's not particularly important here
value0 = @Negative
value1 = @Successful
value2 = @Offline

try =
  if doACalculation < 0 then
     value0
  else
     if isOnline then
       value1
     else
       value2

What should the types of value0, value1, and value2 be? If they’re all inferred as @Negative, @Successful, and @Offline respectively then for try to be inferred as @Negative or @Successful or @Offline you need subtyping, which brings in all the other baggage I talked about. That is you need @Negative or @Successful or @Offline to be a valid replacement for @Negative in certain circumstances (i.e. in function outputs), but not in others (i.e. in function inputs), which complicates Elm quite a bit (this is e.g. why Scala’s type system is sometimes perceived as “complicated”).

Note this is quite different from the way that Elm currently works, where in the absence of type variables, two type signatures must match exactly for the two to be considered compatible.

Basically unfortunately the two issues aren’t quite orthogonal. You need some form of “extension” whether that’s subtyping or extensible type parameters as soon as you have structural types given Elm’s current language design.

try number =
  if isSuccessful number then
    @Success
  else
    @Failure
--> try : Int -> @Success or @Failure

process userInput =
  case extractInput userInput of
    Just number -> try number
    Nothing -> @InvalidInput
--> process : String -> @Success or @Failure or @InvalidInput

type alias AllErrors
  = @Success
  or @Failure
  or @InvalidInput
  -- Somewhere else in the program:
  or @NetworkError

printError : AllErrors -> String
printError error =
  case error of
    @Success -> "Success"
    @Failure -> "Failure"
    @InvalidInput -> "InvalidInput"
    @NetworkError -> "NetworkError"

-- Used at the edge of the program, where all errors might have occurred:
printError (process "test")

I think writing try : Int -> AllErrors should not compile, because we know what variants it can be (@Success or @Failure) and it’s nice to have the exhaustiveness check when I add new variants to AllErrors. So in this case, we would restrict the inferred type tightly.

Am I understanding correctly that we then can’t easily make it so that we can write printError (process "test"), where we give a narrow sum type (3 variants) into a function expecting a wider sum type (4 variants) is valid? Is this type variance that is complex/difficult to implement? Because it seems really straightforward to me.

And yes, now I see that printError (process "test") basically means we need to have implicit extensible sum types. At least I don’t see how we could opt in to this behavior at the call site, as we do at the function type declaration site for extensible records. Thanks for getting me here. :slight_smile:

And thank you for being so patient! I have a tendency to be wordy so you’re being very gracious for bearing with me here.

I’m going to address one thing in your comment because I think it’s a very interesting look at how small things can have ripple effects across a language.

Am I understanding correctly that we then can’t easily make it so that we can write printError (process "test") , where we give a narrow sum type (3 variants) into a function expecting a wider sum type (4 variants) is valid? Is this type variance that is complex/difficult to implement? Because it seems really straightforward to me.

This isn’t quite the entirety of the issue.

value0 = @Tag0 0
value1 = @Tag1 "some string"

myExpression0 = case someBool of
    True -> value0
    False -> value1

This probably seems really easy to resolve from a type perspective. Just glom the two types of value0 and value1 together. Great! No extensibility required. myExpression0 has a type of @Tag0 Int or @Tag1 String.

However, what happens if we wrap it in a list?

myExpression1 = case someBool of
    True -> [ value0 ]
    False -> [ value1 ]

What should happen here? There seems to be three possibilities

  1. Compiler error, myExpression1 does not typecheck.
  2. myExpression1 : List (@Tag0 Int) or List (@Tag1 String)
  3. myExpression1 : List (@Tag0 Int or @Tag1 String)

All of these are pretty big changes to Elm.

Let’s start with 1. If myExpression1 does not currently typecheck, it probably should if I manually line up the types of value0 and value1 to match (i.e. I give them both type annotations of @Tag0 Int or @Tag1 String). However, this is a pretty big ergonomic change for Elm when it comes to type inference. Previously any program that compiled with type annotations would also compile without those annotations, but that’s no longer true. In other words, we’ve lost global type inference.

Alternatively you could require that all types wrapping structural types are themselves wrapped in an outer layer of structural types, but that bifurcates Elm’s type hierarchy in two (right now records play perfectly fine with Elm’s normal union types).

In the case of 2, what we have is a tagless union type (this is different from a structural union type where we still have tags, i.e. the @!). When we go to try to do a case match on myExpression1 that means we’re going to have something like

case myExpression1 of
    xs : List (@Tag0 Int) -> ...
    ys : List (@Tag1 String) -> ...

That’s really different from the way Elm currently works! Through the clever use of variant tags in Elm today (and with tagged structural union types) values at runtime have no types (at least no Elm types). This allows for a variety of optimizations to be made for runtime performance. Here, because the case match happens at runtime, myExpression1 must carry its type information at runtime as well to know which path to take (instead of just a variant tag name). This means pretty big changes to the way that Elm generates Javascript code.

In the case of 3, we really need do need subtyping and variance. Sure maybe List (@Tag0 Int) and List (@Tag1 String) are allowed to unify as List (@Tag0 Int or @Tag1 String), but what about

type MyCustomType a = MyCustomType (a -> Int)

? MyCustomType (@Tag0 Int) can’t unify with MyCustomType (@Tag1 String) to become MyCustomType (@Tag0 Int or @Tag1 String) because the type variable is now an input to a function (and we previously stated that we can’t make the input to a function more “lax”). So now we have to label which types are allowed to unify (e.g. List) and which types are not allowed to unify MyCustomType (this is what I meant by type variance).

In all three cases there are a lot more complications that arise in the absence of extensible union types.

EDIT: To make this clear I do not think subtyping is the way to go. I think subtyping is what happens if you try to ignore the extensible part of structural union types.

2 Likes

I’m not personally familiar with “extensible type parameters” in the languages I have seen, and I’m not sure if folks in this thread know the full performance and usability costs of supporting subtyping in a language that aims for full type inference. (Putting aside cases where the inference is confusing, the perf cost is rather serious in type inference according to the people I’ve met who work on the Scala compiler.)

Do you have typing rules anywhere for this idea? Like Figure 2 in here or Figure 3 in here?

Or a language that implements this proposal?


Note: I get that you are enthusiastic about the idea, but I do not want potential downsides to be downplayed when many readers are not familiar with the details of type inference performance and error specificity. For example, the full OCaml review is:

When to Use Polymorphic Variants

At first glance, polymorphic variants look like a strict improvement over ordinary variants. You can do everything that ordinary variants can do, plus it’s more flexible and more concise. What’s not to like?

In reality, regular variants are the more pragmatic choice most of the time. That’s because the flexibility of polymorphic variants comes at a price. Here are some of the downsides:

  • Complexity - As we’ve seen, the typing rules for polymorphic variants are a lot more complicated than they are for regular variants. This means that heavy use of polymorphic variants can leave you scratching your head trying to figure out why a given piece of code did or didn’t compile. It can also lead to absurdly long and hard to decode error messages. Indeed, concision at the value level is often balanced out by more verbosity at the type level.
  • Error-finding - Polymorphic variants are type-safe, but the typing discipline that they impose is, by dint of its flexibility, less likely to catch bugs in your program.
  • Efficiency - This isn’t a huge effect, but polymorphic variants are somewhat heavier than regular variants, and OCaml can’t generate code for matching on polymorphic variants that is quite as efficient as what it generated for regular variants.

All that said, polymorphic variants are still a useful and powerful feature, but it’s worth understanding their limitations and how to use them sensibly and modestly.

Probably the safest and most common use case for polymorphic variants is where ordinary variants would be sufficient but are syntactically too heavyweight. For example, you often want to create a variant type for encoding the inputs or outputs to a function, where it’s not worth declaring a separate type for it. Polymorphic variants are very useful here, and as long as there are type annotations that constrain these to have explicit, exact types, this tends to work well.

I added the bold there. This matches the experience of a buddy of mine who wrote OCaml professionally and got really excited about this feature breifly, then came to regret his choices. Basically the advice here is to only use this in cases like this:

-- BEFORE

type LocalID = NewID String | OldID Int

func : LocalID -> LocalID


-- AFTER

func : @NewID String or @OldID Int -> @NewID String or @OldID Int

This seems to be a relatively low payoff for the various downsides (perf of inference when subtyping disallows use of Union Find, error message length, multiple ways to do the same thing, etc.)

I understand you are advocating for a system more restricted than the OCaml version in some way, but I’d personally need to see the typing rules to evaluate what that might mean in practice.

7 Likes

The man himself! Thanks for all you’ve done for us here!

So subtyping is definitely not what I’m suggesting here. I’m suggesting parametric polymorphism in the same that records are currently parametrically polymorphic. The approach I’m suggesting is actually exact part of the subject of Leijen’s paper that you’ve linked! Look at section 5 of https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/scopedlabels.pdf. It actually involves no changes to the underlying type checking semantics of that proposal.

Ah so I was in the middle of writing down my thoughts RE OCaml but since you’ve replied I’ll write down an abbreviated version of it and then continue on with a longer version later.

I’m going to be talking a bit more quickly here (I’ll try to go back and re-translate all of this to pseudo-Elm for folks who aren’t familiar with OCaml).

OCaml’s warnings about the dangers of polymorphic variants arise from a combination of three factors that are all missing from this proposal of polymorphic variants.

  1. The ability to impose both min and max type bounds on row types (currently Elm’s extensible records and my proposal for polymorphic variants both only have min bounds). Another way of stating this is that OCaml’s approach at its heart is essentially subtyping while I’m advocating for polymorphic parametricity.
  2. Implicit extensibility from incomplete matches
  3. The ability to add and remove variants

I’ll go one by one in order of complexity, error-finding, and efficiency as detailed in the OCaml link and how these three factors affect those.

I don’t have the time at the moment to translate the examples at the link of inscrutable and strange type errors into Elm pseudo-syntax, but for those people who can read OCaml, the example that the Real World OCaml section talks about as being a “fairly complex inferred type” arises from

let is_positive = function
  | `Int   x -> Ok (x > 0)
  | `Float x -> Ok Float.(x > 0.)
  | `Not_a_number -> Error "not a number"
;;
>val is_positive :
>  [< `Float of float | `Int of int | `Not_a_number ] -> (bool, string) result =
>  <fun>
List.filter [three; four] ~f:(fun x ->
match is_positive x with Error _ -> false | Ok b -> b)
;;
>- : [< `Float of float | `Int of int | `Not_a_number > `Float `Int ] list =
>[`Int 3; `Float 4.]

The complexity here arises from the fact that is_positive is inferred to have an extensible type (i.e. 2) that has a max (not min) type bound (i.e. 1) that then interacts in a complex manner with three and four (values defined earlier with min type bounds). The proposal here basically bans is_positive's type signature.

As for “error-finding” issues, the chapter is mainly talking about situations like this (which it cites earlier up in the chapter).

let is_positive_permissive = function
  | `Int   x -> Ok Int.(x > 0)
  | `Float x -> Ok Float.(x > 0.)
  | _ -> Error "Unknown number type"
;;
>val is_positive_permissive :
>  [> `Float of float | `Int of int ] -> (bool, string) result = <fun>
is_positive_permissive (`Int 0);;
>- : (bool, string) result = Ok false
is_positive_permissive (`Ratio (3,4));;
>- : (bool, string) result = Error "Unknown number type"

is_positive_permissive here is removing variants with the _ -> case (i.e. 3) which covers up typo/fat-finger-like mistakes. This doesn’t happen if you disallow the removal of variants. In particular, the current proposal explicitly disallows a catch-all case value because all case matches must be able to desugar to explicit tag matches.

Efficiency: this is the part I’m a bit wobbly about because I haven’t thought very hard about the code generation aspect so far (mainly been thinking about the language level part), but I have some confidence that the inability to add or remove variants preserves the static structure enough that Elm’s current type erasure still works. In particular, you can “desugar” polymorphic variants that cannot add or remove variants at runtime into a new nominal variant hierarchy at every use site and end up with equivalent functionality (this is an absolutely insane amount of work for a human to do, but isn’t a problem from a theoretical point of view) so that I’m pretty sure you end up with equivalent performance.

Like I said I’m writing out a much longer version of this that presents more of what I’m trading off vs OCaml, Typescript, and Purescript, but that’ll probably take a while before I finish writing that.

2 Likes

As for languages that already implement this, apart from OCaml, the closest next approximation is Purescript with https://github.com/natefaubion/purescript-variant. Now I think there are aspects of that library that don’t work for Elm (and the fact that it’s a library rather than built-in makes its ergonomics pretty terrible compared to the standard that Elm puts forth), but it’s a good example of how it’s really just all row types under the hood (i.e. just piggy-backing off the same fundamental mechanism behind extensible records).

RE the error messages, as I’m translating some current Elm SPA codebases to this pseudo-Elm syntax I’m also starting to build a catalog of potential error messages to try to get a feel for how unwieldy the error messages can get in day-to-day coding. It’ll take a while though before I finish those up I imagine.

2 Likes

I don’t think it’s exactly the same as in Daan’s paper.

For example, every record literal has concrete type. So { x = "hi" } can never have a type like { a | x : String } which is really important for getting good error messages in case expressions.

In contrast, I believe @X "hi" would need to have the open type [a | @X String ] if you wanted to try to make it like record types. I believe this is the only way way it could be fed into a case expressions expecting a closed [ @X String or @Y Int ] type with rules similar to Daan’s. I think that’s an important difference when it comes to error message quality!

And if the literal type is open, wouldn’t the whole case result type be open too? Or is there a special typing rule for case expressions that does not appear in Daan’s paper?

I think these kinds of differences would come out in typing rules specific to your idea.

Note: I included the OCaml quote for readers who may be new to this topic. I personally cannot fully evaluate how a proposal like this differs other things without seeing the specific typing rules.

3 Likes

Yep exactly! This thread may be getting too long for its own good; I think there’s some confusion on exactly what the proposal is at hand. This is long and verbose so I’m not sure if you’ll have the time to read it, but I’ve posted the full (informal) outline of the proposal Shuang Rimu.

I think that’s an important difference when it comes to error message quality!

I don’t actually think the hit to error messages is too high (although I’ll know more about that once I finish writing up that hypothetical error catalog). There’s already an analogous situation in Elm today with field names and records (record literals have concrete types, but field literals have polymorphic types whereas case matches have concrete types and variant literals have polymorphic types). That’s a perfect segue into

And if the literal type is open, wouldn’t the whole case result type be open too?

No, but that’s because a literal used in a case is specialized to a concrete type. case matches can only occur with concrete types (which is why catch-all cases are disallowed).

For example from the scoped labels paper, tab works fine with showEvent even though tab is an open type and showType is entirely closed types.

2 Likes

I’ll have to step out of the discussion for now. I’d need to see typing rules specific to this idea to be able to engage further.

5 Likes

Fair enough. I’ve got to run too, but sometime over the next few days I’ll type out how the whole thing desugars to Leijen’s paper.

4 Likes

Just jamming in a quick thanks for that great explanation of the pitfalls! Really interesting, thanks for taking the time to lay it out!

1 Like

May I provide some interesting reading material about this topic?

From there you can follow the deep rabbit hole of references. I’ve been looking into making a language centered around the idea of extensible data types because it honestly deserves more attention that it’s getting.

2 Likes

Well life made this take a week or two or more than I had hoped to get back to this…

@lboklin good eye! Indeed Koka is the brainchild of Daan Leijen, the guy behind the record paper that I’m desugaring everything behind and whose work forms the basis of Elm’s record types!

@evancz (and anyone else interested): I finally got around to desugaring everything to Leijen’s paper. It’s typed as a PDF because writing proof trees is hell without LaTeX. https://shuangrimu.com/static/extensible-types-leijen.pdf

The PDF ended up being a bit longer than I had hoped it would be, but the main takeaway is the one page that desugars all my examples in my original post to Leijen’s formalisms. The rest of the PDF is just demonstrating that my assigned type signatures are valid.

6 Likes

After only glancing a little over your blog post last time, I’ve now committed to thoroughly reading it this time.

First of all, some nitpicking:

(please skip to “Now, an Idea”, if you want to read interesting stuff)

1

One of the code examples lists this code:

type alias T1 = @A () or @B () or @C ()

decodeFromString1 : String -> Maybe (a or T1)
decodeFromString1 str = case str of
    "a" -> Just <| @A ()
    "b" -> Just <| @B ()
    "c" -> Just <| @C ()
    _ -> Nothing

There’s no syntax for something like { a | Person } in Elm right now, so I don’t quite understand why there should be (a or T1).

Shouldn’t you add the type parameter to T1 directly? Sorry if this came up in the thread already. I think I’ve read through all of this, but that was two weeks ago already.

2

In general, the elm community seems to not recommend using extensible record types.
One of the reasons is that an alternative to extensible records is simply nesting records. That’s what Evan recommended years ago (maybe his views have changed).
But your blog says the recommendation is to ‘Keep your models flat’.
Trying to combine the two recommendations, I’d argue that ‘Keep your models flat’ doesn’t mean ‘Keep your models flat and abstract with extensible records instead of nesting records’, but something like ‘Keep your models flat for now and don’t abstract prematurely’.

3

You make two big points to advocate for extensible union types.

At a high level extensible unions generally bring two things to the table:

  1. The ability to make a type’s size “just right” when a union type is the output of a function.
  2. The ability to use flat hierarchies of union types rather than being forced into nested hierarchies.

I really like how concise they are, btw.

But (unless I’m missing something) these points seems to be more about the structuralness than about the extensiblity of union types. I think it would make sense to ‘pitch’ your Idea to be more about structural union types than about extensible union types. Obviously, you’d need extensible union types, as you need to infer something useful, for e.g. f = @A (), but the big benefits of your proposal could be used without ever writing any extensible union type signatures, just like today many people use the huge benefits of structural record types without ever writing extensible record type signatures, even though the ‘extensible’ feature is absolutely necessary for structural record types to exist in conjunction with type inference.

Though that’s just a mad level of nitpicking about how to pitch this. :smiley:

Now, an Idea

We can (almost) try out (a little less ergonomic version of) extensible union types today!

One huge problem this proposal is set out to solve is to break up huge message types that naturally grow, when you grow an application.

Let’s say you have such a message type Msg. Now you’ve got a view function:

view : Model -> Html Msg
view model =
    layoutSite
        (viewHeader model)
        (viewBody model)
        (viewFooter model)

viewHeader : Model -> Html Msg
viewHeader = ...

viewFooter : Model -> Html Msg
viewFooter = ...

Now, viewHeader and viewFooter have this problem that you mention in your article: They’re over-constrained.
Just like

-- An exaggerated example that people don't do, but illustrative
addOne : Int -> Maybe Int
addOne x = Just (x + 1)

which doesn’t need to return Maybe, viewHeader doesn’t produce any constructor of Msg, but maybe just 6-10 of them, like GoToPage, when you click on a settings icon, or ToggleDarkTheme and some more.

But as you noted in your article, records and unions are dual to each other. So when you have extensible record types, you almost have extensible union types:

viewHeader :
    { a
        -- these fields mirror the signatures of your union constructors
        | goToPage : Url -> msg
        , toggleDarkTheme : msg
        ... -- other messages used by viewHeader
            -- but no messages used by e.g. viewFooter
    }
    -> Html msg
viewHeader =

This way, you make the msg type of your viewHeader function ‘just right’.

What you’d do to use this, would be to create one huge record of all of your constructors for Msg, let’s call that msgConstructors and pass that to all view functions:

view : Model -> Html Msg
view model =
    layoutSite
        (viewHeader msgConstructors model)
        (viewBody msgConstructors model)
        (viewFooter msgConstructors model)

msgConstructors =
    { goToPage = GoToPage
    , toggleDarkTheme = ToggleDarkTheme
    , emailFormSubmit = EmailFormSubmit -- used in viewFooter
    ... -- a field for all other message constructor
    }

However, there are still differences with this approach and actual structural union types:

  1. You have to define this msgConstructors record!
  2. When adding a message constructor, you need to also add it to msgConstructors. Also, msgConstructors and Msg can get out-of-sync and there can be errors in translation.
  3. Abstracting out these ‘extensible union types’ doesn’t take only 1, but 2 type parameters:
    type alias HeaderMsgs a msg =
        { a
            | goToPage : Url -> msg -- what else, if not 'msg'?
            , toggleDarkTheme : msg
            ...
        }
    
    With actual extensible union types, it’s only 1 type parameter.

But I like that it’s almost possible to try out how extensible union types could be used to structure an elm application today. In such a way that it’s also possible to run it and verify that it gives you the benefits you hope for.


Sidenote:
I also remember that something like msgConstructors gets auto-generated in the functional programming language ‘Dhall’ for their extensible union types. They essentiall support this:

type alias HeaderMsgs =
    @GoToPage or @ToggleDarkTheme

msgConstructors = HeaderMsgs -- a value-level identifier generated for the type-level type alias definition.

For more info on that feature see the dhall language cheatsheet.

Earlier I suggested this is not exactly like extensible records for two reasons:

  1. That the type of value @X "hi" would be the open type [ a | @X String ]
  2. There needs to be a special rule for case expressions.

Both of these differences appear in your write up, which makes sense. The fact that the general mechanism is the same does not account for practical differences like this when it comes to implementation and error messages. That’s the point I was trying to make above.

Example

The fact that @X "hi" has an open type has particularly big consequences with error messages. Take this function:

toOutput input =
  case input of
    @A a -> @Quick a
    @B b -> @Brown b
    @C c -> @Fox c
    @D d -> @Jump d
    @E e -> @Lazy e
    @F f -> @Dog f
    @G g -> @How g
    @H h -> @Much h
    @I i -> @Wood i
    @J j -> @Could j
    @K k -> @Wood k
    @L l -> @Chuck l
    @M m -> @Chuck m
    @N n -> @If n
    @O o -> @Wood o
    @P p -> @Coud p
    @Q q -> @Chuck q
    @R r -> @Wood r
    @S s -> @Could s
    @T t -> @Chuck t
    @U u -> @Wood u
    @V v -> @Could v
    @W w -> @Check w
    @X x -> @Wood x
    @Y y -> @Brown y
    @Z z -> @Fox z

Where is the typo? Is there one typo? Zero? Multiple?

And are there any type errors here? How would you even begin to figure that out?

With a closed ADT, the compiler can underline the exact constructor that has a typo or type error, with or without a type annotation.

It is easy to say “this is no problem if people just add the type annotation” but this is not fully true:

  1. You can only give an error for the whole case branch, not for the specific constructor. So with a branch with let x = ... in x, instead of underlining Coud directly, it is going to say "there is something wrong with the type of this let or this let body. If the branch is 10 lines or 20 lines, this is significantly less specific. So even in the best case, the error message is much less specific.

  2. Say you want intend for @Whatever x to have type [ a | @Whatever Int ] but in a large case branch someone ends up using the constructor with a String value. With the current design, you get the error message directly under Whatever x but with the proposed design you can only say “this branch does not match the type annotation” again getting 10 or 20 line chunks on large case branches.

  3. My experience very strongly suggests that if a program can be written, it will be written. People will be looking at 400 and 600 line case expressions hunting for a typo or type error with associated data. At that point, it is fair to say “the error messages are not very good” and there is no real way to get the quality back besides not using the feature.

In the past, we took out the ability to change the type of record fields in the record update syntax specifically because of problems (1) and (2) where you couldn’t get good specificity, particularly with unannotated cases which are not uncommon in practice. Even after restricting the design of records, it’s still hard to underline the specific field name that has a typo.

I hope this establishes the error message quality issues clearly.

Tradeoffs

Say we have this BEFORE and AFTER code, where we are getting the best case error messages for both open and closed union types:

-- BEFORE

type Output
    = Quick String
    | Brown String
    | Fox String
    | Jump String
    | Lazy String
    | Dog String
    | How String
    | Much String
    | Wood String
    | Could String
    | Chuck String
    | If String

toOutput : Input -> Output
toOutput input =
  ...


-- AFTER

type alias Output
    = @Quick String
    or @Brown String
    or @Fox String
    or @Jump String
    or @Lazy String
    or @Dog String
    or @How String
    or @Much String
    or @Wood String
    or @Could String
    or @Chuck String
    or @If String

toOutput : Input -> Output
toOutput input =
  ...

To my eye, the AFTER looks harder to understand and comes with a bunch of downsides that will come up in practice a lot. Conservatively lets say 50% of users don’t think about all the ways the error messages are impacted by the BEFORE and AFTER and many are not writing type annotations, especially beginners. The result is that error messages are worse in practice, and there is nothing that really can be done about it.

The best path to deliver them good quality is to strongly recommend against using this feature at all. Furthermore, beginners would be seeing person A recommending this feature highly and person B recommending against it strongly. What should they do? Should they try both? Is this question important to making the website or game they set out to make? Do teams need to argue about it in their style guide on features to use or not? (Any team I’ve been on that uses C++ or Haskell has had a style guide banning specific features specifically because there are so many trade-offs with extensions, macros, features, etc. The reason these style guides are so common is that there is a real tension between “make working code that others can read and modify easily” and having lots of ways to express the same thing.)

So based on my understanding of the design, it seems like some aspects of error message quality can be addressed (e.g. maybe with pattern part of case branches) but that there are still significant tradeoffs in error message quality in other areas.

Thoughts

I could be wrong about things here, but it feels like this kind of feature is a bit risky for Elm. I try to prioritize ease-of-learning and error message quality very highly. So while I am open to the idea that someone could figure out how to make open union types strong on those points, I would not be comfortable running that experiment in Elm with the information I have at this point.

It seems like a lot of cool things could be done if the core design of the language was “always use open union types” and there just wasn’t closed unions except when you say [ X Int | Y String ]. That would also mean that @Foo could be written as Foo without clashing with another language feature. It’d look a lot cleaner, and it may end up leading towards a different style of typed functional programming that many people could be into. (Lots of people value flexibility and having many ways to do things! E.g. people who prefer Ruby over Python! So even if the error messages are never as good, many people have priorities where that is a worthwhile tradeoff.)

So it feels to me like something worth exploring independently to get a feeling for the full implications in a setting where the culture, best practices, libraries, etc. can all evolve in a coherent way, with flexibility prioritized a bit higher than other things.

18 Likes

I just want to drop my two cents in here:

I am reading this discussion with excitement and joy, even when I don’t really understand the specifics of the details. However, what this discussion boils down to me is this:

  1. It is basically a ‘Keeping Elms integrity and spirit vs. Effort to make beneficial changes’ strong energy investment. To be honest, this one point, in my opinion, is immature to the Language and Community. A lot of theory in this case (which of course is also important) vs. way less practical applications and use case scenarios.

  2. It boils down that some people make a great effort not knowing that their worked out solution works against the core strengths of Elm and others make a great effort for keeping the spirit and core features. So what could we do about that to approach things like this better and invest energy more efficiently ? Even more generally speaking, the culture of developing Elm ? This is what I see in the discussion.

Open unions are still quite useful without the extensible part, the main feature in the examples provided by @yosteden and even the Ocaml guide are the composition part, where different constructors can be composed different ways, like this example How to represent many subsets of an enum?.

Could it possible to have exactly the dual of records for Elm, where features like adding fields/variants are just removed to achieve the same error message experience?

I agree with the trade off part, but can we just force type annotation on functions with open unions (otherwise compilation error with a nice suggestion) to make the experience a bit smoother?

@eimfach I don’t know about @evancz’s feelings here, but I think this current discussion is perfectly cromulent! I view Evan and I as playing out the roles we’re each supposed to have in this discussion. Evan is supposed to be the conservative, wary gatekeeper, one who has seen countless other breathless proposals of “the next best thing since sliced bread” that must be added to Elm.

I play the role of the breathless proponent! As I said at the outset of all this, although I would very much love to see this feature added to Elm, this thread is primarily about sparking discussion around it rather than forcing a decision on its admission.

@Philipp_Krueger after writing out my post I link later in this reply I’m a bit out of gas to give you a full reply that goes into detail about your idea, but I’ll just say that your proposal has legs! You’ve stumbled on a pattern that sometimes goes by the name of the Translator Pattern and is found in a lot of Elm libraries (notably a lot of No Red Ink’s libraries use this pattern). It turns out there’s actually another step forward you can take which is to use a record of functions to entirely represent an extensible union (instead of having an additional output type that the record maps to, e.g. your Html msg). This technique goes by various names (Church encoding, Scott encoding, Boehm-Berarducci encoding, etc.), but the basic idea is the same as yours. Unfortunately it can’t be full implemented in Elm due to the lack of higher-rank polymorphism (it’s a good thing Elm doesn’t have this) and so comes with sharp edges in Elm as it stands.

And as for @evancz’s comments, I’ve typed up my reply as a separate blog post because it’s too long to fit in a single Discourse reply. The post is here: https://shuangrimu.com/posts/elm-extensible-unions-error-messages.html.

Basically, while his comments are true for the way that Elm currently implements error reporting, I don’t think this is intrinsically true of extensible unions. In fact, I think it’s possible to have specific error messages localized to a single offending line even in the case of completely unannotated code, let alone code with annotations!

My post goes into that. The actual algorithm is quite straightforward, but it requires quite a bit of set up to motivate and explain why it works.

Also, my current iteration of the algorithm is somewhat slow and clunky, if straightforward, and I think it can be improved significantly, but I’m putting it out there to show the quality of error messages we can potentially have and to show that the tension between extensible error messages is not an intrinsic one, but an extrinsic one specific to the implementation of an error reporting system.

One big thing to note is that what I propose in this post is potentially independently useful for Elm, even outside of extensible unions. I’ll couch a lot of this reply in the language of extensible unions since that’s what we’re talking about, but everything I say here pertains only to row types, and so pertains to Elm’s records as well. N.B. row types are the types that underlie both record types and extensible union types, the set of types and type tags (i.e. field names in records and variant tag names for extensible unions) within the brackets. As shown earlier here, ultimately the typing judgments for both records and extensible unions are the exact same.

Here’s the overall structure of my post, for easy jumping to the parts that interest readers.

6 Likes

Great writeup. There’s a line I don’t quite understand. Did the sentence cut off?

Assume we have a type error between two row types A and B for a given expression E , at least one of which is polymorphic, take the row type that has two

Another one that’s confusing me:

The dropping of elements in step 3 occurs because we can have irrelevant symbols that are “swallowed” by functions and don’t contribute to the final

What do you mean by ‘C’?

First, unification results in x3 having a type @BB Int which f does not support. Then we collect all our symbols for C , which are the following:

Do you mean value? So, if I understand correctly, you try to list all symbols that appear in value?