Understanding purescript-variant

Question

Newbie here. I'm trying to understand some of the machinery behind purescript-variant. Basically what I mean is how to understand these 2 function: inj and on.

When I look at the type of inj, the author makes use of Cons typeclasses. From my understanding, Cons place an assertion that there's a record r2 that can be made from some other record r1 by inserting a pair of tag/value. So in a sense:

r1 + tag/value = r2

And in this case Variant is the r2.

Citing from the readme:

foo :: forall v. Variant (foo :: Int | v)
foo = inj (SProxy :: SProxy "foo") 42

bar :: forall v. Variant (bar :: Boolean | v)
bar = inj (SProxy :: SProxy "bar") true

fooToString :: forall v. Variant (foo :: Int | v) -> String
fooToString = on (SProxy :: SProxy "foo") show (\_ -> "not foo")

This is where it gets confusing for me. I can feed the bar as an argument to fooToString while from the type of bar there's no guarantee that it has a tag "foo" even if it's an open type. How is this possible?

After some more thinking. I guess this is because the type of fooToString itself doesn't restrict that the variant has to have a tag of "foo" in it. And also becaue of the open types. Is this true? — autumn322

Hjulle Hjulle · Accepted Answer · 2018-12-10T14:21:37

Both foo and bar restrict that the variant type has to contain some tag, but they don't prevent other tags from being included in the variant. The concrete types when you apply fooToString bar would be:

 bar :: Variant (bar :: Boolean, foo :: Int) -- v = (foo :: Int)
 fooToString :: Variant (foo :: Int, bar :: Boolean) -> String -- v = (bar :: Boolean)

As you can see, they are perfectly compatible.

The internals version of the types would be

bar :: forall r1 r2. RowCons "bar" Boolean r1 r2 => Variant r2
fooToString :: forall r1 r2. RowCons "foo" Int r1 r2 => Variant r2 -> String

which will specialize to

bar :: RowCons "bar" Boolean (foo :: Int) (foo :: Int, bar :: Boolean) => Variant (foo :: Int, bar :: Boolean)
fooToString :: RowCons "foo" Int (bar :: Boolean) (foo :: Int, bar :: Boolean) => Variant (foo :: Int, bar :: Boolean) -> String

Where, for bar, r1 is set to/specialized into (foo :: Int) and r2 becomes (foo :: Int, bar :: Boolean). Similarly for fooToString.

As you can see, r1 is unused outside of the constraint for both bar and fooToString, which allows them to be chosen freely to satisfy the constraints. It would be be equally valid for the compiler to add even more (unused) variants to the type, but that wouldn't change the result.

Edit:

Something that is unusual about Pruescript is that not only functions, but also values can be polymorphic. In this case, bar is a polymorphic value and fooToString is a polymorphic function. This means that the users of both bar and fooToString are free to choose any type for v (or r1/r2), as long the type contains the required variants.

Understanding purescript-variant

1 Answers

Edit: