NoImplicits.scala

trait Foo {
  // Represents natural numbers or expressions resulting in natural numbers.
  trait Nat {
    // The actual value (e.g. for 1 + 3 * 2, this would be 7).
    type Result <: Nat1
    // Fold.
    type Fold[K, z <: K, s[_ <: Nat] <: K] <: K
    // Catamorphism.
    type Cata[K, z <: K, s[_ <:   K] <: K] <: K
  }
  // Represents natural numbers (not expressions).
  trait Nat1 extends Nat
  
  final class Z extends Nat1 {
    type Result = Z
    type Fold[K, z <: K, s[_ <: Nat] <: K] = z
    type Cata[K, z <: K, s[_ <:   K] <: K] = z
  }
  final class S[n <: Nat] extends Nat1 {
    type Result = S[n#Result]
    type Fold[K, z <: K, s[_ <: Nat] <: K] = s[n]
    type Cata[K, z <: K, s[_ <:   K] <: K] = s[n#Cata[K, z, s]]
  }
  
  final class +[n <: Nat, m <: Nat] extends Nat {
    type Result = Cata[Nat1, Z, S]
    type Fold[K, z <: K, s[_ <: Nat] <: K] = n#Fold[K, m#Fold[K, z, s], ({type L[n1 <: Nat] = S[n1 + m]#Result#Fold[K, z, s] })#L]
    // Catamorphism builds the result bottom-up, this line says roughly the following:
    // 1. Start with m#Cata[K, z, s].
    // 2. When you see that n has an extra S layer, apply s.
    type Cata[K, z <: K, s[_ <:   K] <: K] = n#Cata[K, m#Cata[K, z, s], s]
  }
  
  final class *[n <: Nat, m <: Nat] extends Nat {
    type Result = Cata[Nat1, Z, S]
    type Fold[K, z <: K, s[_ <: Nat] <: K] = n#Cata[K, z, ({type L[x <: K] = m#Fold[K, x, s]})#L]
    // Catamorphism builds the result bottom-up, this line says roughly the following:
    // 1. Start with z
    // 2. When you see that n has an extra S layer, apply s m times.
    type Cata[K, z <: K, s[_ <:   K] <: K] = n#Cata[K, z, ({type L[x <: K] = m#Cata[K, x, s]})#L]
  }
  
  type _0 = Z
  type _1 = S[_0]
  type _2 = S[_1]
  type _3 = S[_2]
  type _4 = S[_3]
  type _5 = S[_4]
  type _6 = S[_5]
  
  // 1 : (Z + Z)#Result
  
  implicitly[(      Z)#Result           =:=    Z]
  implicitly[(      Z)#Cata[Nat, Z, S]  =:=    Z]
  implicitly[(      Z)#Fold[Nat, Z, S]  =:=    Z]
  
  implicitly[(   S[Z])#Result           =:= S[Z]]
  implicitly[(   S[Z])#Cata[Nat, Z, S]  =:= S[Z]]
  implicitly[(   S[Z])#Fold[Nat, Z, S]  =:= S[Z]]
  
  implicitly[(_0 + _0)#Result           =:=   _0]
  implicitly[(_0 + _1)#Result           =:=   _1]
  implicitly[(_1 + _0)#Result           =:=   _1]
  implicitly[(_1 + _1)#Result           =:=   _2]
  implicitly[(_0 + _0)#Cata[Nat1, Z, S] =:=   _0]
  implicitly[(_0 + _1)#Cata[Nat1, Z, S] =:=   _1]
  implicitly[(_1 + _0)#Cata[Nat1, Z, S] =:=   _1]
  implicitly[(_1 + _1)#Cata[Nat1, Z, S] =:=   _2]
  implicitly[(_0 + _0)#Fold[Nat1, Z, S] =:=   _0]
  implicitly[(_0 + _1)#Fold[Nat1, Z, S] =:=   _1]
  implicitly[(_1 + _0)#Fold[Nat1, Z, S] =:=   _1]
  implicitly[(_1 + _1)#Fold[Nat1, Z, S] =:=   _2]
  
  implicitly[(_0 * _0)#Result           =:=   _0]
  implicitly[(_0 * _1)#Result           =:=   _0]
  implicitly[(_1 * _0)#Result           =:=   _0]
  implicitly[(_1 * _1)#Result           =:=   _1]
  implicitly[(_0 * _0)#Cata[Nat1, Z, S] =:=   _0]
  implicitly[(_0 * _1)#Cata[Nat1, Z, S] =:=   _0]
  implicitly[(_1 * _0)#Cata[Nat1, Z, S] =:=   _0]
  implicitly[(_1 * _1)#Cata[Nat1, Z, S] =:=   _1]
  implicitly[(_0 * _0)#Fold[Nat1, Z, S] =:=   _0]
  implicitly[(_0 * _1)#Fold[Nat1, Z, S] =:=   _0]
  implicitly[(_1 * _0)#Fold[Nat1, Z, S] =:=   _0]
  implicitly[(_1 * _1)#Fold[Nat1, Z, S] =:=   _1]
  
  final class Times[F[_], n <: Nat] {
    type T[A] = n#Cata[Any, A, F]
  }
  implicitly[Times[Option, (_2 * _1) + _1]#T[Int] =:= Option[Option[Option[Int]]]]
  
  implicitly[(_2 * _2)#Result =:= _4]
  implicitly[((_2 * _2) + _1)#Result =:= _5]
  implicitly[((_2 * _2) + _2)#Result =:= _6]
  implicitly[(_2 * _3)#Result =:= _6]
  
  final class Lists[A] {
    trait T { self =>
      type Fold[K, nil <: K, cons[a <: A, _ <: T] <: K] <: K
      type Cata[K, nil <: K, cons[a <: A, _ <: K] <: K] <: K
    }
    
    final class Nil extends T {
      type Fold[K, nil <: K, cons[a <: A, _ <: T] <: K] = nil
      type Cata[K, nil <: K, cons[a <: A, _ <: K] <: K] = nil
    }
    
    final class ::[head <: A, tail <: T] extends T {
      type Fold[K, nil <: K, cons[a <: A, _ <: T] <: K] = cons[head, tail]
      type Cata[K, nil <: K, cons[a <: A, _ <: K] <: K] = cons[head, tail#Cata[K, nil, cons]]
    }
  }
  val natList: Lists[Nat1] = new Lists[Nat1]
  import natList._
  
  implicitly[(_3 :: _2 :: _1 :: Nil)#Cata[Nat1, Z, ({type L[a <: Nat1, b <: Nat1] = (a + b)#Result})#L] =:= _6]
  implicitly[(_3 :: _2 :: _1 :: Nil)#Cata[Nat1, _1, ({type L[a <: Nat1, b <: Nat1] = (a * b)#Result})#L] =:= _6]
  
}