Uninhabited.blk

Auto.

# We won't need anything above type(2).
type(2) : type(3).
type(1) : type(2).

# Subtyping lattice:
any  : type(1).
void : type(1).
# Reflexivity:
[t]         (t  : type(1)) -> (void << t) & (t << t) & (t << any).
# Transitivity:
[t1, t2, t3] (t1 : type(1)) & (t2 : type(1)) & (t3 : type(1)) & (t1 << t2) & (t2 << t3) -> (t1 << t3).
# (Sub)typing judgement.
[t1, t2, x] (t1 : type(1)) & (t2 : type(1)) & (x : t1) & (t1 << t2) -> (x : t2).

[t1, t2] (t1 : type(1)) & (t2 : type(1)) -> (union(t1, t2) : type(1)).
[t1, t2] t1 << union(t1, t2).
[t1, t2] t2 << union(t1, t2).
[t1, t2] (t1 << t2) -> (union(t1, t2) = t2).
[t1, t2] union(t1, t2) = union(t2, t1).

[t1, t2] (t1 : type(1)) & (t2 : type(1)) -> (int(t1, t2) : type(1)).
[t1, t2] int(t1, t2) << t1.
[t1, t2] int(t1, t2) << t2.
[t1, t2] (t1 << t2) -> (int(t1, t2) = t1).
[t1, t2] int(t1, t2) = int(t2, t1).

# Singletons
[x] (x : t) -> (x : singleton(x)) & (singleton(x) << t).

# Functions.
[k, t1, t2] (t1 : type(1)) & (t2 : type(1)) -> (func(t1, t2) : type(1)).
[x1, x2, t1, t2] ((x1 : t1) -> (x2 : t2)) -> <f> f: func(t1, t2).
[t1, t2, x, f] (x : t1) & (f : func(t1, t2)) -> app(f, x) : t2.

# Void is empty.
! (<x> x : void).

# Unit.
unit : type(1).
u : unit.

# Natural numbers.
z : nat.
[n] (n : nat) -> (s(n) : nat).

# Option.
[t] option(t) : type(1).
[t1, t2] (t1 << t2) -> (option(t1) << option(t2)).
[t] none : option(t).
[t, x] (x : t) -> (some(x) : option(t)).

# Tuple.
[t1, t2] product(t1, t2) : type(1).
[t1, t11, t2] (t1 << t11) -> (product(t1, t2) << product(t11, t2)).
[t1, t1, t21] (t1 << t21) -> (product(t1, t2) << product(t1, t21)).
[t1, t2, x1, x2] (x1 : t1) & (x2 : t2) -> tuple(x1, x2) : product(t1, t2).
[t1, t2, x] (x : product(t1, t2)) -> fst(x) : t1.
[t1, t2, x] (x : product(t1, t2)) -> snd(x) : t2.

# # trait Foo { def f[A]: A => Nothing }
# foo : type(1).
# [x] (x : foo) -> [a] (a : type(1)) -> foo_f(x, a) : func(a, void).
# <x> x : foo.

# # type Foo = (A, A => Nothing)
# <x> x : product(a, func(a, void)).

# # trait Foo[B <: Nothing] { def f[A]: A => B }
# [b] ((b : type(1)) & (b << void)) <-> foo(b) : type(1).
# [x, b] (x : foo(b)) -> [a] (a : type(1)) -> foo_f(x, a) : func(a, b).
# <x, b> x : foo(b).

# # [A] Option[A] => (A, A)
# [x, t] (x : option(t)) -> <x> x : product(t, t).
# [t] <f> f : func(option(t), t).

# # type Foo = (Foo => A, B => Nothing)
# # A <: B
# foo : type(1).
# bar : type(1).
# baz : type(1).
# bar << baz.
# [x] (x : foo) -> foo_value(x) : product(func(foo, bar), func(baz, void)).
# <x> x : foo.