sir-wabbit

type *[A, B] = (A, B)
type +[A, B] = Either[A, B]
type Void <: Nothing

trait Functions[F[_]] {
  def unit: F[Unit]
  def void: F[Void]
  def any[A]:  F[A]

  def pure[A]:     A  => F[A]

sir-wabbit

import Abstract._

trait Abstract[A, T] {
  type Result[_]
}
private[covenant] trait L4 {
  implicit def otherwise[A, B]: Abstract.Aux[A, B, λ[X => B]] =
    new Abstract.Aux1[A, B, λ[X => B]]
}
private[covenant] trait L3 extends L4 {

sir-wabbit

type Void <: Nothing
def absurd[A](v: Void): A = v


type Id[x] = x

trait Forall[F[_]] {
  def apply[A]: F[A]
}

sir-wabbit

import scala.reflect.ClassTag

object Test {
  type Flags = Flags.Type
  trait Flags1 {
    import Flags._
    type Type <: Int with Tag$$1
  }
  object Flags extends Flags1 {
    trait Tag$$1 extends Any

sir-wabbit

package kodkod

sealed abstract class DepPair[A, F[_ <: A with Singleton]] {
  val first: A
  val second: F[first.type]
}
object DepPair {
  def apply[A, F[_ <: A with Singleton]](a: A)(fa: F[a.type]): DepPair[A, F] =
    new DepPair[A, F] {
      val first = a

sir-wabbit

type | [+A, +B] = Union.Type[A, B]
object Union {
  trait Tag extends Any
  type Base
  type Type[+A, +B] <: Base with Tag
  
  implicit def first[A]: A <:< Type[A, Nothing] = 
    implicitly[A <:< A].asInstanceOf[A <:< Type[A, Nothing]]
  implicit def second[B]: B <:< Type[Nothing, B] = 
    implicitly[B <:< B].asInstanceOf[B <:< Type[Nothing, B]]

sir-wabbit

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:

sir-wabbit

/**
  * Parametric type constructors are either constant or injective.
  * Constant type constructors satisfy `∀ a b. f a = f b`.
  * Injective type constructors satisfy `∀ a b. (f a = f b) => a = b`.
  *
  * Parametricity ≡
  *   `(∀ a b. f a = f b) ∨ (∀ a b. (f a = f b) => a = b)` ≡
  *   `∀ a b x y. (f x = f y) ∨ ¬(f a = f b) ∨ (a = b)`
  *
  * Using `A ∨ B ⊢ ¬A => B`, we get:

sir-wabbit

Preliminaries

type Void <: Nothing
type ¬[-A] = A => Void
type ¬¬[+A] = ¬[¬[A]]
type ⋁[+A, +B] = Either[A, B]
type ⋀[+A, +B] = Tuple2[A, B]

sir-wabbit

-- Everything down below is in Idris pseudocode

data EvenOrOdd : (n : Int) -> Type where
  Even : {n : Int} -> (k : Int) -> (2 * k = n)     -> EvenOrOdd n
  Odd  : {n : Int} -> (k : Int) -> (2 * k + 1 = n) -> EvenOrOdd n
  
-- let's drop all computational information
data EvenOrOdd = Even | Odd

-- let's drop all names (except type alias)