Previously: Structural wrapper subtyping

Only 5 real types

As we already know from the previous chapter:

There are only 5 real types in Я: Void, Unit, Sum, Product and Arrow. That’s it! The rest is on newtype wrappers.

In this chapter we are going to talk about mostly about Sum and Product. You may find those in majority of modern programming languages as well. However, the devil is in the details!

Elements of row polymorphism

Let’s say we have a Product type, structurally it contains two elements - and type declaration reflects this fact:

x = (12345 `lu` False Unit): Integer `P` Boolean

Using at method we can get access to a field in that record:

x `yi` at `ho` this @Integer ===> 12345
x `yi` at `ho` this @Boolean ===> False Unit

Exactly the same code could be applied for record where these fields are defined in reverse order:

x = (False Unit `lu` 12345): Boolean `P` Integer
x `yi` at `ho` this @Integer ===> 12345
x `yi` at `ho` this @Boolean ===> False Unit

You also can replace exact field with a new one:

x `yi` at @Integer `ho` that `li` 54321 ===> False Unit `lu` 54321
x `yi` at @Boolean `ho` that `li` by True ===> True Unit `lu` 12345

Alternatively you can use this/that methods that give you an access to left/right objects of a tuple accordingly:

x `yi` this @Boolean ===> False Unit
x `yi` that @Integer ===> 12345

I think using types instead of field names is better since you don’t have to come up with names and you have less boilerplate.

But what if we have a tuple of elements of the same type?

x = (12345 `lu` 12345): Integer `P` Integer

at is not going to work here anymore since it cannot decide which field it should get access to based on provided type information… In this case you can tag your fields:

x = (Tag 12345 `lu` Tag 6789): (Minutes # Integer) `P` (Seconds # Integer)

So this way we can use at method on distinguishable types:

x `yi` at @(Minutes # Integer) `ho` this ===> Tag 12345
x `yi` at @(Seconds # Integer) `ho` this ===> Tag 6789

But these values are still tagged! To get rid of this Tag we can use unwrap, but we have to specify subtyping morphism - it’s Arrow in this case:

x `yi` at @(Minutes # Integer) `ho` this `ho` unwrap @(AR) ===> 12345
x `yi` at @(Seconds # Integer) `ho` this `ho` unwrap @(AR) ===> 6789

Here is a better way - if we use he operator next to ho, type of morphism is just going to be the same as for this method:

x `yi` at @(Minutes # Integer) `ho` this `ho'he` is ===> 12345
x `yi` at @(Seconds # Integer) `ho` this `ho'he` is ===> 6789

Snippet with demonstration of record fields manipulations is located here.

Untagged unions

It’s time to look at its counterpart - Sums.

x = (This 12345): Integer `S` Boolean

Current x value holds Integer which means that we can change only Integer part of this union:

x `yoi` (+ 6789) ==> This 19134
x `yio` wrap `ha` not ==> This 19134

At some point you need to resolve it, let’s say we want to decide how many bits should we allocate for these types:

We can use explicit pattern matching for that:

case x of
 This _ -> 32
 That _ -> 1

However, explicit pattern matching in Я is not very welcoming since it’s monstrous and doesn’t compose well. Use la operator instead:

is @Integer `hu` 32 `la` is @Boolean `hu` 1

It’s more compact and you don’t use lambdas.

Tagged unions

As we have seen with records, it would be nice to have something similar - ability to pick a member of a union without knowing its structure. So here you go:

on: entire `AR_` entire `M` target `S` target

This operator is saying: give me an entire structure and I either find a target you are asking for (target) or I give you this structure back without that target (entire - target).

But this operator works only with tagged unions in order to avoid ambiguity:

x = (This `hv` Tag 12345): (Unit # Integer) `S` (Unit # Boolean)
 
x `yi` on @Integer ===> That `hv` 12345
x `yi` on @Boolean ===> This `hv` Tag 12345

There is a good demonstration how to work with on method in this tutorial chapter.

Just follow your types

As you can see, working with tagged Products and Sums is easy with types instead of defining getting/setters. With this approach we use compiler’s help rather than creating bloated boilerplate (doesn’t matter if it’s generated by Template Haskell or you do it manually).