[uryga]

...which, btw, is equivalent to Maybe/Either – they're tagged unions, i.e. pairs (tag, content). Maybe<T> is isomorphic* to

  { has_value: bool,
    val: T|nil }

* well, this representation is a bit too permissive, since you could do

  {has_value: true, val: nil} 

if you wanted to get the types water-tight, you'd need dependent types, typing it as dependent pair:

  Maybe<T> =
    sigma (has_value: bool)
      if has_value
        then T
        else ()

which can then only have values

  (false, ())

or

  (true, <actual value of type T>)