λm.me/blog

In the last blog post we covered extensible records and how we infer their types in Giml.

In this blog post we'll take a closer look at another interesting feature and the dual of extensible records - polymorphic variants.

There are several approaches for typing polymorphic variants and they have different tradeoffs as well. Giml's system is very similar to OCaml's polymorphic variants system and also shares its limitations. If you are looking for different approaches you might want to look at this/this or this.

I'm also not sure polymorphic variants is the best we can do to have extensible sum types, as having recursive polymorphic variants is quite problematic. But there are still plenty of usecases where they could be used so it's worth including them in a language.

[Word of warning, this is a bit more complicated than previous posts and it might be best to look at this section as a cookbook. If you see something weird or not explained well, it might be a testement to that I'm a little fuzzy on the details myself]

Polymorphic Variants

Polymorphic variants can be seen as the dual of extensible records.

Records are product types, they let us hold multiple values together in one structure at the same time, and by giving a label for each value we can refer to each part.

Variants are sum types, they let us define multiple values as alternatives to one another, and we label each alternative as well.

There are two operations we can do with variants, one is creating a tagged value, for example #Ok 1, the other is pattern matching on variants. For example:

withDefault def x =
    case x of
        | #Ok v -> v
        | #Err _ -> def
    end

The types for polymorphic variants are a bit more complicated. There are actually three different kinds of polymorphic variants: closed, lower-bounded and upper-bounded.

In a closed variant we list the different labels and the type of their payload, for example: [ Err : String, Ok : Int ] is a type that have two possible alternative , #Err <some-string> and #Ok <some-integer>. This type is something that can be generated by applying a polymorphic variant to a function that takes polymorphic variants as input.

An upper-bounded polymorphic variant is open, it describes the maximum set of variants that could be represented by this type, and is represented syntactically with a type variable followed by a little < right after the opening bracket (for example: [ t < Err : String, Ok : Int ]).

Why does this exist? This type can be used when we want to use a variant in a pattern matching expression, and we have a set of variants that we can handle. The pattern matching example above is one like that. In that pattern matching expression we could match any subset of [ Err : a, Ok : b ]. So we use an upper-bounded polymorphic variant to express that in types.

Lower-bounded polymorphic variant is open as well, it describes the minimum set of variants that could be represented by this type, and is represented with a type variable followed by a little > right after the opening bracket (for example: [ t > Err : String, Ok : Int ]). It can unify with any superset of the specified alternatives.

Why does this exist? There are a couple of cases:

One, this type is used when we want to pass a variant to a function that does pattern matching on that variant, and has the ability to match on unspecified amount of variants, for example with a wildcard (_) or variable pattern. For example:

withDefault def x =
    case x of
        | #Ok 0 -> def
        | #Ok v -> v
        | _ -> def
    end

In this case, even if we passed #Foo 182 this pattern matching should work, it will just match the wildcard pattern and return def.

But note that expressions cannot have multiple types (at least not in Giml), therefore we must specify in our case that the #Ok must have a specific type (Int) and we cannot pass #Ok "hello" instead. In the pattern matching above we could match on [ Ok : Int ] or any other type, and we write this like this: [ t > Ok : Int ].

Another case is the type of variant "literals" themselves! This could be considered the dual of record selection: when we specify a tagged value (say, #Ok 1), what we really want for it is to fit anywhere that expect at least [ Ok : Int ].

Implementation

Type definition

So we add 3 new constructors to represent the three variant types:

1. TypeVariant [(Label, Type)] for closed variant
2. TypePolyVariantLB [(Constr, Type)] TypeVar for lower-bounded polymorphic variant
3. TypePolyVariantUB TypeVar [(Constr, Type)] for upper-bounded polymorphic variant

Here, just like with records, we use the row type variable to encoded hidden knowledge about our types.

For lower-bounded polymorphic variants (from now on, LB), we use the row type variable to represent other variants (similar to how with records the row type variable was used to represent other fields).

For upper-bound polymorphic variants (from now on, UB) the row type variable has a different role. We use the row type variable to keep track of which UB we want to merge together (those with the same row type variable), how to convert a UB to LB (constrain the UB row type variable with the merge of the UB and LB fields + the LB row type variable), and when to treat two UBs as normal variants (those with a different row type variable).

We'll explore each scenario soon.

Elaboration and constraint generation

Creating variants

When we create a variant, we:

1. Elaborate the type of the payload
2. Generate a type variable
3. Annotate the type of the AST node as TypePolyVariantLB [(<label>, <payload-type>)] <typevar>

We will see how this unifies with other variants.

Pattern matching

For matching an expression with one or more patterns of polymorphic variants, we elaborate the expression and constrain the type we got with a newly generated type variable which is going to be our hidden row type variable and representative of the type of the expression (and let's call it tv for now).

For each variant pattern matching we run into, we add the constraint:

Equality (TypeVar tv) (TypePolyVariantUB tv [(<label>, <payload-type>)])

By making all variant patterns equal to tv, we will eventually need to unify all the types that arise from the patterns, and by keeping the hidden row type variable tv the same for all of them, we annotate that these TypePolyVariantUBs should unify by merging the unique fields on each side and unifying the shared fields.

Another special case we have is a regular type variable pattern (capture pattern) and wildcard. In our system, a capture pattern should capture any type, including any variant. This case produces the opposite constraint:

Equality (TypeVar tv) (TypePolyVariantLB [] tv2)

Note that this special type, TypePolyVariantLB [] tv2, unifies with non-variant types as if it is a simple type variable, but with variant types it behave like other TypePolyVariantLBs.

Constraint solving

We have 3 new types, TypeVariant, TypePolyVariantLB and TypePolyVariantUB. And in total we have 7 unique new cases to handle:

• Equality TypeVariant TypeVariant
• Equality TypeVariant TypePolyVariantLB
• Equality TypeVariant TypePolyVariantUB
• Equality TypePolyVariantLB TypePolyVariantLB
• Equality TypePolyVariantLB TypePolyVariantUB
• Equality TypePolyVariantUB TypePolyVariantUB (where the row type variables match)
• Equality TypePolyVariantUB TypePolyVariantUB (where the row type variables don't match)

The cases are symmetrical, so we'll look at one side.

Equality TypeVariant TypeVariant

For two TypeVariants, like with two TypeRecs, we unify all the fields. If there are any that are only on one side, we fail.

Equality TypeVariant TypePolyVariantLB

This case is similar to the Equality TypeRec TypeRecExt case, all Fields in the LB side must appear and unify in the TypeVariant side, and the fields that are unique to the TypeVariant should unify with the row type variable of LB.

We don't want the LB to have any extra fields that are not found in the regular variant side!

Equality TypeVariant TypePolyVariantUB

When an upper-bounded polymorphic variant meets a regular variant, we treat the UB as a regular variant as well. This is something that can make seemingly well typed programs to be rejected by the typechecker (in a manner that is similar to not having let-polymorphism) but we do not represent the constraint of a subset/subtype in Giml, only equality, and the two types just aren't equal.

Equality TypePolyVariantLB TypePolyVariantLB

Two lower-bounded polymorphic variant should unify all the shared fields, and their row type variants should unify with a new LB that contains the non-shared fields (and a new row type variable).

Equality TypePolyVariantLB TypePolyVariantUB

LB means any superset of the mentioned fields, and UB means any subset of the mentioned fields. Meaning, we don't want to have a field in the LB said that doesn't exist in the UB side. This is basically the same case as Equality TypeVariant TypePolyVariantLB.

Equality TypePolyVariantUB TypePolyVariantUB (where the row type variables match)

When the two row type variables match, this means that the two types represent alternative pattern matches, so we make sure their fields unify and merge them: we generate a constraint that unifies the merged UB (with the same row type variable) with the row type variable. This is so we can establish the most up-to-date type of the row type variable in the substitution.

Equality (TypePolyVariantUB tv <merged-fields>) (TypeVar tv)

This way we add to the list of alternative variants, add keep track of the row type variable is the substitution and subsequent constraints.

Equality TypePolyVariantUB TypePolyVariantUB (where the row type variables don't match)

We treat these two as unrelated variants that represent the same subest of fields, so the fields should match just like regular variants (Equality TypeVariant TypeVariant).

Instantiation

Instantiation is straightforward, just like all other cases: we instantiate the row type variables here as well.

Substitution

For substitution we need to handle a few cases:

• For UB, if the row type variable maps to another type variable, we just switch the type variable. Otherwise we merge the variant fields we have with the type.
• For LB with no variant fields (TypePolyVariantLB [] tv) we return the value mapped in the substitution (remember that this case is also used for wildcards and captures in pattern matching and not just variants).
• For LB with variant fields, we try to merge the variant fields with the type.

Merging variants happens the same as with records, but we don't have to worry about duplicate variants as the constraint solving algorithm makes sure they have the same type.

Note that this is where a UB can flip and become LB (if it's merged with an LB).

Example

As always, let's finish of with an example and infer the types of the following program:

withDefault def x =
    case x of
        | #Some v -> v
        | #Nil _ -> def
    end

one = withDefault 0 (#Some 1)

First group

withDefault def x =
    case x of
        | #Some v -> v
        | #Nil _ -> def
    end

Elaboration and constraints generation

    +---- targ3 -> t4 -> t5
    |
    |        +---- targ3
    |        |
    |        |  +----- t4
    |        |  |
withDefault def x =
         +------------ t4
         |
    case x of        +---- t7
                     |
        | #Some v -> v

        | #Nil _ -> def
                     |
                     |
                     +---- targ3
    end

-- Constraints:

[ Equality t4 t6
, Equality t5 t7
, Equality t5 targ3
, Equality t6 [ t6 < Nil : t9 ]
, Equality t6 [ t6 < Some : t7 ]
, Equality t7 t8
, Equality t9 t10
, Equality tfun2 (targ3 -> t4 -> t5)
, Equality top0 (targ3 -> t4 -> t5)
]

Constraint solving

-- Constraints:
    [ Equality t4 t6
    , Equality t5 t7
    , Equality t5 targ3
    , Equality t6 [ t6 < Nil : t9 ]
    , Equality t6 [ t6 < Some : t7 ]
    , Equality t7 t8
    , Equality t9 t10
    , Equality tfun2 (targ3 -> t4 -> t5)
    , Equality top0 (targ3 -> t4 -> t5)
    ]
-- Substitution:
    []

1. Equality t4 t6
   -- => t4 := t6

-- Constraints:
    [ Equality t5 t7
    , Equality t5 targ3
    , Equality t6 [ t6 < Nil : t9 ]
    , Equality t6 [ t6 < Some : t7 ]
    , Equality t7 t8
    , Equality t9 t10
    , Equality tfun2 (targ3 -> t6 -> t5)
    , Equality top0 (targ3 -> t6 -> t5)
    ]
-- Substitution:
    [ t4 := t6
    ]

2. Equality t5 t7
   -- => t5 := t7

-- Constraints:
    [ Equality t7 t7
    , Equality t7 targ3
    , Equality t6 [ t6 < Nil : t9 ]
    , Equality t6 [ t6 < Some : t7 ]
    , Equality t7 t8
    , Equality t9 t10
    , Equality tfun2 (targ3 -> t6 -> t7)
    , Equality top0 (targ3 -> t6 -> t7)
    ]
-- Substitution:
    [ t4 := t6
    , t5 := t7
    ]


3. Equality t7 t7
   -- => Nothing to do

-- Constraints:
    [ Equality t7 targ3
    , Equality t6 [ t6 < Nil : t9 ]
    , Equality t6 [ t6 < Some : t7 ]
    , Equality t7 t8
    , Equality t9 t10
    , Equality tfun2 (targ3 -> t6 -> t7)
    , Equality top0 (targ3 -> t6 -> t7)
    ]
-- Substitution:
    unchanged

4. Equality t7 targ3
   -- => t7 := targ3

-- Constraints:
    [ Equality t6 [ t6 < Nil : t9 ]
    , Equality t6 [ t6 < Some : targ3 ]
    , Equality targ3 t8
    , Equality t9 t10
    , Equality tfun2 (targ3 -> t6 -> targ3)
    , Equality top0 (targ3 -> t6 -> targ3)
    ]
-- Substitution:
    [ t4 := t6
    , t5 := targ3
    , t7 := targ3
    ]


5. Equality t6 [ t6 < Nil : t9 ]
   -- => t6 := [ t6 < Nil : t9 ] -- note that we don't do occurs check here

-- Constraints:
    [ Equality [ t6 < Nil : t9 ] [ t6 < Nil : t9 ]
    , Equality [ t6 < Nil : t9 ] [ t6 < Nil : t9 | Some : targ3 ]
    , Equality targ3 t8
    , Equality t9 t10
    , Equality tfun2 (targ3 -> [ t6 < Nil : t9 ] -> targ3)
    , Equality top0 (targ3 -> [ t6 < Nil : t9 ] -> targ3)
    ]
-- Substitution:
    [ t4 := [ t6 < Nil : t9 ]
    , t5 := targ3
    , t7 := targ3
    , t6 := [ t6 < Nil : t9 ]
    ]

6. Equality [ t6 < Nil : t9 ] [ t6 < Nil : t9 ]
   -- => The two sides are the same, nothing to do.

-- Constraints:
    [ Equality [ t6 < Nil : t9 ] [ t6 < Nil : t9 | Some : targ3 ]
    , Equality targ3 t8
    , Equality t9 t10
    , Equality tfun2 (targ3 -> [ t6 < Nil : t9 ] -> targ3)
    , Equality top0 (targ3 -> [ t6 < Nil : t9 ] -> targ3)
    ]
-- Substitution:
    unchanged

7. Equality [ t6 < Nil : t9 ] [ t6 < Nil : t9 | Some : targ3 ]
   -- => [ Equality t6 [ t6 < Nil : t9 | Some : targ3 ], Equality t9 t9 ]

-- Constraints:
    [ Equality t6 [ t6 < Nil : t9 | Some : targ3 ]
    , Equality t9 t9
    [ Equality [ t6 < Nil : t9 ] [< Nil : t9 | Some : targ3 ]
    , Equality targ3 t8
    , Equality t9 t10
    , Equality tfun2 (targ3 -> [ t6 < Nil : t9 ] -> targ3)
    , Equality top0 (targ3 -> [ t6 < Nil : t9 ] -> targ3)
    ]
-- Substitution:
    unchanged

8. Equality [ t6 < Nil : t9 ] [ t6 < Nil : t9 | Some : targ3 ]
   -- => t6 := [ t6 < Nil : t9 | Some : targ3 ]

-- Constraints:
    [ Equality t9 t9
    , Equality targ3 t8
    , Equality t9 t10
    , Equality tfun2 (targ3 -> [ t6 < Nil : t9 | Some : targ3 ] -> targ3)
    , Equality top0 (targ3 -> [ t6 < Nil : t9 | Some : targ3 ] -> targ3)
    ]
-- Substitution:
    [ t4 := [ t6 < Nil : t9 | Some : targ3 ]
    , t5 := targ3
    , t7 := targ3
    , t6 := [ t6 < Nil : t9 | Some : targ3 ]
    ]

9. Equality t9 t9
   -- => Nothing to do


-- Constraints:
    [ Equality targ3 t8
    , Equality t9 t10
    , Equality tfun2 (targ3 -> [ t6 < Nil : t9 | Some : targ3 ] -> targ3)
    , Equality top0 (targ3 -> [ t6 < Nil : t9 | Some : targ3 ] -> targ3)
    ]
-- Substitution:
    unchanged

10. Equality targ3 t8
    -- => targ3 := t8

-- Constraints:
    [ Equality t9 t10
    , Equality tfun2 (t8 -> [ t6 < Nil : t9 | Some : t8 ] -> t8)
    , Equality top0 (t8 -> [ t6 < Nil : t9 | Some : t8 ] -> t8)
    ]
-- Substitution:
    [ t4 := [ t6 < Nil : t9 | Some : t8 ]
    , t5 := t8
    , t7 := t8
    , t6 := [ t6 < Nil : t9 | Some : t8 ]
    , targ3 := t8
    ]


11. Equality t9 t10
    -- => t9 := t10

-- Constraints:
    [ Equality tfun2 (t8 -> [ t6 < Nil : t10 | Some : t8 ] -> t8)
    , Equality top0 (t8 -> [ t6 < Nil : t10 | Some : t8 ] -> t8)
    ]
-- Substitution:
    [ t4 := [ t6 < Nil : t10 | Some : t8 ]
    , t5 := t8
    , t7 := t8
    , t6 := [ t6 < Nil : t10 | Some : t8 ]
    , targ3 := t8
    , t9 := t10
    ]

11. Equality tfun2 (t8 -> [ t6 < Nil : t10 | Some : t8 ] -> t8)
    -- => tfun2 := (t8 -> [ t6 < Nil : t10 | Some : t8 ] -> t8)

-- Constraints:
    [ Equality top0 (t8 -> [ t6 < Nil : t10 | Some : t8 ] -> t8)
    ]
-- Substitution:
    [ t4 := [ t6 < Nil : t10 | Some : t8 ]
    , t5 := t8
    , t7 := t8
    , t6 := [ t6 < Nil : t10 | Some : t8 ]
    , targ3 := t8
    , t9 := t10
    , tfun2 := t8 -> [ t6 < Nil : t10 | Some : t8 ] -> t8
    ]

12. Equality top0 (t8 -> [ t6 < Nil : t10 | Some : t8 ] -> t8)
    -- => top0 := t8 -> [ t6 < Nil : t10 | Some : t8 ] -> t8

-- Constraints: []
-- Substitution:
    [ t4 := [ t6 < Nil : t10 | Some : t8 ]
    , t5 := t8
    , t7 := t8
    , t6 := [ t6 < Nil : t10 | Some : t8 ]
    , targ3 := t8
    , t9 := t10
    , tfun2 := t8 -> [ t6 < Nil : t10 | Some : t8 ] -> t8
    , top0 := t8 -> [ t6 < Nil : t10 | Some : t8 ] -> t8
    ]

Substitute

Let's substitute the type variables in our program and hide the row type variables:

    +---- t8 -> [ t6 < Nil : t10 | Some : t8 ] -> t8
    |
    |        +---- t8
    |        |
    |        |  +----- [ t6 < Nil : t10 | Some : t8 ]
    |        |  |
withDefault def x =
         +------------ [ t6 < Nil : t10 | Some : t8 ]
         |
    case x of        +---- t8
                     |
        | #Some v -> v

        | #Nil _ -> def
                     |
                     |
                     +---- t8
    end

Generalize

    +---- forall a b c. c -> [ b < Nil : a | Some : c ] -> c
    |
    |        +---- c
    |        |
    |        |  +----- [ b < Nil : a | Some : c ]
    |        |  |
withDefault def x =
         +------------ [ b < Nil : a | Some : c ]
         |
    case x of        +---- c
                     |
        | #Some v -> v

        | #Nil _ -> def
                     |
                     |
                     +---- c
    end

Second group

one = withDefault 0 (#Some 1)

Elaboration and constraints generation

 +-- t6
 |         +--- t1
 |         |
 |         |      +---- Int
 |         |      |
 |         |      |    +---- t4 -> [ t3 > Some : t4 ]
 |         |      |    |
 |         |      |    |   +--- Int
 |         |      |    |   |
one = withDefault 0 (#Some 1)
      -------------  -------
            |           |
            |           +--- t5
            |
            +------ t2

-- Constraints:

[ Equality t1 (Int -> t2)
, Equality t1 (forall a b c. c -> [b < Nil : a | Some : c] -> c)
, Equality t2 (t5 -> t6)
, Equality (t4 -> [ t3 > Some : t4 ]) (Int -> t5)
, Equality top0 t6
]

Constraint solving

-- Constraints:
    [ Equality t1 (Int -> t2)
    , Equality t1 (forall a b c. c -> [b < Nil : a | Some : c] -> c)
    , Equality t2 (t5 -> t6)
    , Equality (t4 -> [ t3 > Some : t4 ]) (Int -> t5)
    , Equality top0 t6
    ]

1. Equality t1 (Int -> t2)
    -- => t1 := Int -> t2

-- Constraints:
    [ Equality (Int -> t2) (forall a b c. c -> [b < Nil : a | Some : c] -> c)
    , Equality t2 (t5 -> t6)
    , Equality (t4 -> [ t3 > Some : t4 ]) (Int -> t5)
    , Equality top0 t6
    ]
-- Substitution:
    [ t1 := Int -> t2
    ]

2. Equality (Int -> t2) (forall a b c. c -> [b < Nil : a | Some : c] -> c)
    -- => [ Equality (Int -> t2) (ti9 -> [ ti8 < Nil : ti7 | Some : ti9 ] -> ti9) ]

-- Constraints:
    [ Equality (Int -> t2) (ti9 -> [ ti8 < Nil : ti7 | Some : ti9 ] -> ti9)
    , Equality t2 (t5 -> t6)
    , Equality (t4 -> [ t3 > Some : t4 ]) (Int -> t5)
    , Equality top0 t6
    ]
-- Substitution: unchanged

3. Equality (Int -> t2) (ti9 -> [ ti8 < Nil : ti7 | Some : ti9 ] -> ti9)
    -- => [ Equality Int ti9, Equality t2 ([ ti8 < Nil : ti7 | Some : ti9 ] -> ti9) ]

-- Constraints:
    [ Equality Int ti9
    , Equality t2 ([ ti8 < Nil : ti7 | Some : ti9 ] -> ti9)
    , Equality t2 (t5 -> t6)
    , Equality (t4 -> [ t3 > Some : t4 ]) (Int -> t5)
    , Equality top0 t6
    ]
-- Substitution: unchanged

4. Equality Int ti9
    -- => ti9 := Int

-- Constraints:
    [ Equality t2 ([ ti8 < Nil : ti7 | Some : Int ] -> Int)
    , Equality t2 (t5 -> t6)
    , Equality (t4 -> [ t3 > Some : t4 ]) (Int -> t5)
    , Equality top0 t6
    ]
-- Substitution:
    [ t1 := Int -> t2
    , ti9 := Int
    ]

5. Equality t2 ([ ti8 < Nil : ti7 | Some : Int ] -> Int)
    -- => t2 := [ ti8 < Nil : ti7 | Some : Int ] -> Int

-- Constraints:
    [ Equality ([ ti8 < Nil : ti7 | Some : Int ] -> Int) (t5 -> t6)
    , Equality (t4 -> [ t3 > Some : t4 ]) (Int -> t5)
    , Equality top0 t6
    ]
-- Substitution:
    [ t1 := Int -> [ ti8 < Nil : ti7 | Some : Int ] -> Int
    , ti9 := Int
    , t2 := [ ti8 < Nil : ti7 | Some : Int ] -> Int
    ]

6. Equality ([ ti8 < Nil : ti7 | Some : Int ] -> Int) (t5 -> t6)
    -- => [ Equality [ ti8 < Nil : ti7 | Some : Int ] t5, Equality Int t6 ]

-- Constraints:
    [ Equality [ ti8 < Nil : ti7 | Some : Int ] t5
    , Equality Int t6
    , Equality (t4 -> [ t3 > Some : t4 ]) (Int -> t5)
    , Equality top0 t6
    ]
-- Substitution: unchanged

7. Equality [ ti8 < Nil : ti7 | Some : Int ] t5
    -- => t5 := [ ti8 < Nil : ti7 | Some : Int ]

-- Constraints:
    [ Equality Int t6
    , Equality (t4 -> [ t3 > Some : t4 ]) (Int -> [ ti8 < Nil : ti7 | Some : Int ])
    , Equality top0 t6
    ]
-- Substitution:
    [ t1 := Int -> [ ti8 < Nil : ti7 | Some : Int ] -> Int
    , ti9 := Int
    , t2 := [ ti8 < Nil : ti7 | Some : Int ] -> Int
    , t5 := [ ti8 < Nil : ti7 | Some : Int ]
    ]

7. Equality Int t6
    -- => t6 := Int

-- Constraints:
    [ Equality (t4 -> [ t3 > Some : t4 ]) (Int -> [ ti8 < Nil : ti7 | Some : Int ])
    , Equality top0 Int
    ]
-- Substitution:
    [ t1 := Int -> [ ti8 < Nil : ti7 | Some : Int ] -> Int
    , ti9 := Int
    , t2 := [ ti8 < Nil : ti7 | Some : Int ] -> Int
    , t5 := [ ti8 < Nil : ti7 | Some : Int ]
    , t6 := Int
    ]

8. Equality (t4 -> [ t3 > Some : t4 ]) (Int -> [ ti8 < Nil : ti7 | Some : Int ])
    -- => [ Equality t4 Int, Equality [ t3 > Some : t4 ] [ ti8 < Nil : ti7 | Some : Int ] ]

-- Constraints:
    [ Equality t4 Int
    , Equality [ t3 > Some : t4 ] [ ti8 < Nil : ti7 | Some : Int ]
    , Equality top0 Int
    ]
-- Substitution: unchanged

9. Equality t4 Int
    -- => t4 := Int

-- Constraints:
    [ Equality [ t3 > Some : Int ] [ ti8 < Nil : ti7 | Some : Int ]
    , Equality top0 Int
    ]
-- Substitution:
    [ t1 := Int -> [ ti8 < Nil : ti7 | Some : Int ] -> Int
    , ti9 := Int
    , t2 := [ ti8 < Nil : ti7 | Some : Int ] -> Int
    , t5 := [ ti8 < Nil : ti7 | Some : Int ]
    , t6 := Int
    , t4 := Int
    ]

10. Equality [ t3 > Some : Int ] [ ti8 < Nil : ti7 | Some : Int ]
    -- => [ Equality [ t3 > Some : Int ] [ Nil : ti7 | Some : Int ], Equality ti8 [] ]
    -- LB ~ UB are solved like LB and normal variant
    -- the UB type variable should be equals to [] (the empty variant)

-- Constraints:
    [ Equality [ t3 > Some : Int ] [ Nil : ti7 | Some : Int ]
    , Equality ti8 []
    , Equality top0 Int
    ]
-- Substitution: unchanged

11. Equality [ t3 > Some : Int ] [ Nil : ti7 | Some : Int ]
    -- => [ Equality Int Int, Equality t3 [ Nil : ti7 ] ]

-- Constraints:
    [ Equality Int Int
    , Equality t3 [ Nil : ti7 ]
    , Equality ti8 []
    , Equality top0 Int
    ]
-- Substitution: unchanged

12. Equality Int Int
    -- => []

-- Constraints:
    [ Equality t3 [ Nil : ti7 ]
    , Equality ti8 []
    , Equality top0 Int
    ]
-- Substitution: unchanged

13. Equality t3 [ Nil : ti7 ]
    -- => t3 := [ Nil : ti7 ]

-- Constraints:
    [ Equality ti8 []
    , Equality top0 Int
    ]
-- Substitution:
    [ t1 := Int -> [ ti8 < Nil : ti7 | Some : Int ] -> Int
    , ti9 := Int
    , t2 := [ ti8 < Nil : ti7 | Some : Int ] -> Int
    , t5 := [ ti8 < Nil : ti7 | Some : Int ]
    , t6 := Int
    , t4 := Int
    , t3 := [ Nil : ti7 ]
    ]

15. Equality ti8 []
    -- => ti8 := []

-- Constraints:
    [ Equality top0 Int
    ]
-- Substitution:
    [ t1 := Int -> [ Nil : ti7 | Some : Int ] -> Int
    , ti9 := Int
    , t2 := [ Nil : ti7 | Some : Int ] -> Int
    , t5 := [ Nil : ti7 | Some : Int ]
    , t6 := Int
    , t4 := Int
    , t3 := [ Nil : ti7 ]
    , ti8 := Int
    ]

14. Equality top0 Int
    -- => top0 := Int

-- Constraints:
    []
-- Substitution:
    [ t1 := Int -> [ Nil : ti7 | Some : Int ] -> Int
    , ti9 := Int
    , t2 := [ Nil : ti7 | Some : Int ] -> Int
    , t5 := [ Nil : ti7 | Some : Int ]
    , t6 := Int
    , t4 := Int
    , t3 := [ Nil : ti7 ]
    , ti8 := []
    , top0 := Int
    ]

... and done.

Substitute

Let's substitute the type variables in our program and hide the row type variables:

 +-- Int
 |         +--- Int -> [ Nil : ti7 | Some : Int ] -> Int
 |         |
 |         |      +---- Int
 |         |      |
 |         |      |    +---- Int -> [ Some : Int ]
 |         |      |    |
 |         |      |    |   +--- Int
 |         |      |    |   |
one = withDefault 0 (#Some 1)
      -------------  -------
            |           |
            |           +--- [ Nil : ti7 | Some : Int ]
            |
            +------ [ Nil : ti7 | Some : Int ]

Result

    +---- forall a b c. c -> [ b < Nil : a | Some : c ] -> c
    |
    |        +---- c
    |        |
    |        |  +----- [ b < Nil : a | Some : c ]
    |        |  |
withDefault def x =
         +------------ [ b < Nil : a | Some : c ]
         |
    case x of        +---- c
                     |
        | #Some v -> v

        | #Nil _ -> def
                     |
                     |
                     +---- c
    end

 +-- Int
 |         +--- Int -> [ Nil : ti7 | Some : Int ] -> Int
 |         |
 |         |      +---- Int
 |         |      |
 |         |      |    +---- Int -> [ Some : Int ]
 |         |      |    |
 |         |      |    |   +--- Int
 |         |      |    |   |
one = withDefault 0 (#Some 1)
      -------------  -------
            |           |
            |           +--- [ Nil : ti7 | Some : Int ]
            |
            +------ [ Nil : ti7 | Some : Int ]

Phew, looks correct!

Alternative approach: simulation in userland

Another cool thing I'd like to note is that polymorphic variants could potentially be simulated in userland if you have extensible records in the language (and this is what purescript-variant) does for example).

One approach I tweeted about that also helped me reach the polymorphic variant implementation for Giml is to:

1. Make variant values functions - they take their payload and a record of functions as input, and select the label in the record that corresponds to their constructor, and pass it the payload
2. Make patterns fields in a record - the relevant label takes the expected payload and does something with it
3. Make pattern matching just applying variants with patterns. That way the variant selector will select the right pattern match from the record and apply the payload

Though in this approach we can't add a "default handler" label.

Summary

Polymorphic variants are a bit complicated and implementing them is a bit tricky, and they also have several limitations. But I believe that for some use cases they can really make a difference and it's worth having them in the language.

If you're interesting to see a video of me live coding polymorphic variants in Giml, check out Part 17 of my live streaming Giml development series.