Three Times: Python, Dafny & Idris

This section looks at Union Types. As we saw with Enumerations, there are times we want to represent different choices using the same type. Union types encode the idea that a type’s value can be one of many variants.

The name ‘union’ ostensibly comes from the C family of programming languages, where unions were overlapping regions of memory where it was not clear which value you had. Tagged unions (also known as variants and sum types) support discrimination of these values using tags i.e. constructor names. Intersection types on the otherhand are a special form of union.

Python

Python supports intersection types. We show this by demonstrating an example of the Option type as a raw union.

def isJust(v : str | None):
    match v:
        case str():
            print(f"Is String { v }")
        case _:
            print("Is none")

Here the bar (|) denotes the intersection. When working with these values we have to match on their constructor to discriminate between the different cases.

We can also define a type synonym to make our functions easier to read.

type MaybeStr = str | None

def isJust(v : MaybeStr):
    match v:
        case str():
            print(f"Is String { v }")
        case _:
            print("Is none")

Here type is the python keyword to declare a type alias (synonym).

Dafny

Within Dafny, we have tagged unions (aka variants). And we use the same syntax as for records, but use bar (|) to discriminate between the options.

datatype MaybeStr = Nothing | Just(value : string)

Remember that in functional programming, datatypes are actually known as: algebraic datatypes, where we can construct structured data as a sum of products. That is, a tagged union is the choice between a bunch or records which themselves can contain a bunch of sums…

Much like python we can use match to discriminate between the different choices.

function isJust(s : MaybeStr) : bool
{
  match s
  {
  case Nothing => false
  case Just(_) => true
  //        ^ Wildcard
  }
}

Wildcards can be within the constructor pattern.

We can also write this function imperatively.

method IsJust(s : MaybeStr) returns (b : bool)
{
  match s
  {
  case Nothing => return false;
  case Just(_) => return true;
  }
}

Idris

Idris like Dafny supports algebraic datatypes. Simple datatypes take an almost similar form:

data MaybeStr = Nothing | Just String

Remember that datatypes in Idris are indexed families. We can rewrite MaybeStr as:

data MaybeStr : Type where
  Nothing : MaybeStr
  Just : (value : String) -> MaybeStr

Again remember, the above definition is what the simple definition is transformed to internally!

We can then use pattern matching on function arguments to discriminate between the choices:

isJust : MaybeStr -> Bool
isJust Nothing = false
isJust (Just _) = true

Like Dafny Idris enables wildcards in constructors.

As we saw with enumerations we can also use an explicit case tree:

isJust : MaybeStr -> Bool
isJustr m
  = case m of
      Nothing => false
      (Just _) => true