AVL trees, intrinsically and extrinsically typed. Scala examples of exercises from CM 500 Logical Frameworks (see https://github.com/julianpeeters/hello-twelf/tree/main)

avl.scala

// AVL trees, intrinsically and extrinsically typed

/* "extrinsically typed" AVL trees
 *
 * avlTree : tree -> type.
 * avlTree/leaf : avlTree leaf.
 * avlTree/node-1: avlTree (node L R)
 *   <- height L (s H)
 *   <- height R H.
 * avlTree/node0: avlTree (node L R)
 *   <- height L H
 *   <- height R H.
 * avlTree/node+1: avlTree (node L R)
 *   <- height L H
 *   <- height R (s H).
 */
type Avl[T] = T match
  case Leaf.type => Close[Zero.type, Leaf.type]
  case Node[l, r] => Close[Difference[Height[Avl[l]], Height[Avl[r]]], Node[l, r]]
  
type Close[N, T] = N match
  case Zero.type => T
  case Successor[Max[Successor[Max[Zero.type, Zero.type]], Zero.type]] => T
  case Successor[Max[Zero.type, Successor[Max[Zero.type, Zero.type]]]] => T
  case Successor[Max[Zero.type, Zero.type]] => T
  case Successor[Zero.type] => T
  
val mm: Avl[Leaf.type] = Leaf
val nn: Avl[Node[Leaf.type, Leaf.type]] = Node(Leaf, Leaf)
val oo: Avl[Node[Leaf.type, Node[Leaf.type, Leaf.type]]] = Node(Leaf, Node(Leaf, Leaf))
val pp: Avl[Node[Node[Leaf.type, Leaf.type], Leaf.type]] = Node(Node(Leaf, Leaf), Leaf)
val qq: Avl[Node[Node[Leaf.type, Leaf.type], Node[Leaf.type, Leaf.type]]] = Node(Node(Leaf, Leaf), Node(Leaf, Leaf))
val rr: Avl[Node[Node[Node[Leaf.type, Leaf.type], Leaf.type], Node[Leaf.type, Node[Leaf.type, Leaf.type]]]] = Node(Node(Node(Leaf, Leaf), Leaf), Node(Leaf, Node(Leaf, Leaf)))
val ss: Avl[Node[Node[Node[Node[Leaf.type, Leaf.type], Leaf.type], Leaf.type], Node[Leaf.type, Node[Leaf.type, Leaf.type]]]] = Node(Node(Node(Node(Leaf, Leaf), Leaf), Leaf), Node(Leaf, Node(Leaf, Leaf)))
// correctly does not compile
// val tt: Avl[Node[Node[Node[Node[Node[Leaf.type, Leaf.type], Leaf.type], Leaf.type], Leaf.type], Node[Leaf.type, Node[Leaf.type, Leaf.type]]]] = Node(Node(Node(Node(Node(Leaf, Leaf), Leaf), Leaf), Leaf), Node(Leaf, Node(Leaf, Leaf)))
val uu: Avl[Node[Node[Node[Node[Leaf.type, Leaf.type], Leaf.type], Leaf.type], Node[Node[Leaf.type, Node[Leaf.type, Leaf.type]], Node[Node[Node[Leaf.type, Leaf.type], Node[Leaf.type, Leaf.type]], Node[Leaf.type, Leaf.type]]]]] = Node(Node(Node(Node(Leaf, Leaf), Leaf), Leaf), Node(Node(Leaf, Node(Leaf, Leaf)), Node(Node(Node(Leaf, Leaf), Node(Leaf, Leaf)), Node(Leaf, Leaf))))



/* "intrinsically typed" avl tree:
 *
 * avl : nat -> type.
 * avl/leaf : avl z.
 * avl/node-1: avl (s N) -> avl N -> avl (s (s N)).
 * avl/node0 : avl N -> avl N -> avl (s N).
 * avl/node+1: avl (s (s N)) -> avl N -> avl (s N).
 */
sealed trait AVL[T]

case object ALeaf extends AVL[Zero.type]

case class `ANode-1`[
  N <: Nat,
  L <: AVL[Successor[N]],
  R <: AVL[N]
](l: L, r: R) extends AVL[Successor[Successor[N]]]

case class ANode0[
  N <: Nat,
  L <: AVL[N],
  R <: AVL[N]
](l: L, r: R) extends AVL[Successor[N]]

case class `ANode+1`[
  N <: Nat,
  L <: AVL[N],
  R <: AVL[Successor[N]]
](l: L, r: R) extends AVL[Successor[Successor[N]]]

val ff: AVL[Successor[Zero.type]] = ANode0(ALeaf, ALeaf)
val gg: AVL[Successor[Successor[Zero.type]]] = `ANode-1`(ANode0(ALeaf, ALeaf), ALeaf)
val hh: AVL[Successor[Successor[Zero.type]]] = `ANode+1`(ALeaf, ANode0(ALeaf, ALeaf))
val ii: AVL[Successor[Successor[Zero.type]]] = ANode0(ANode0(ALeaf, ALeaf), ANode0(ALeaf, ALeaf))