# Simple SKI Combinator Calculus in Scala’s Type System

I would like to make two claims:

1. The Scala type system is turing complete.
2. This is not a bug.

The SKI combinator calculus is known to be turing equivalent:

```  trait λ { type ap[_<:λ]<:λ }
type I = λ{type ap[X<:λ] = X }
type K = λ{type ap[X<:λ] = λ{type ap[Y<:λ] = X }}
type S = λ{type ap[X<:λ] = λ{type ap[Y<:λ] = λ{type ap[Z<:λ] = X#ap[Z]#ap[Y#ap[Z]] }}}
```

And we can blow up the compiler with unbounded recursion, without resorting to circular definitions:

```type Y = S#ap[I]#ap[I]#ap[S#ap[I]#ap[I]]
```

The latter should crash the compiler with a stack overflow error.

Hat tip: Edward Kmett

# Liskov Substitution Principle is Contravariance

The Liskov Substitution Principle is a much cited result by those who believe in the myth of “object-oriented programming”. But the LSP is like many things in the OO mythos that become “invisible or simpler” when looked at from the perspective of the properties of functions (which is what programming really is about).

Let’s remind ourselves of the LSP:

Let q(x) be a property provable about objects x of type T. Then q(y) should be true for objects y of type S where S is a subtype of T.

Let `Q[A]` be a property provable about objects of type `A`. By Curry-Howard, a proof of this property is a program, and the property that it proves is a type.

So we translate “let q(x) be a property provable about objects x of type T” to just `Q[T]`. We translate “q(y) should be true for objects y of type S” to `Q[S]`.

We write `X => Y` to mean “X implies Y”, or “if X, then Y”. Let’s translate “S is a subtype of T” into these terms. It means that the set of all values in `S` is a subset of the values in `T`. So if you have a value `s` in `S`, then `s` is also in `T`. More loosely, we will say that every object `s` in `S` corresponds to exactly one object `t` in `T`. In other words, `S` implies `T`, or `S => T`. This is precisely the type of functions from S to T, and we will consider every function of this type to be a proof that `S => T`.

We’re now ready to state the Liskov Substitution Principle:

For all T, S. Q[T] => (S => T) => Q[S]

Read it as: If the property Q holds for all values of type T, then if every object of type S maps to exactly one object of type T, the property Q holds for all values of type S.

This is exactly the type of `comap` for a contravariant functor. So LSP just says “predicates are contravariant”. And what’s more, `comap` literally boils down to function composition in practise. So it’s almost completely trivial.

# A Proper Constant Function in Scala

This evening there was a discussion in #scala on Freenode about how to define a properly quantified and appropriately lazy constant function in Scala. In short, the following does not suffice for two reasons:

```def const[A,B](a: A) = (b: B) => a
```

Firstly, it’s too strict. The `B` argument is always evaluated, so this fails:

```scala> val x = const(7)(error("too strict"))
java.lang.RuntimeException: too strict
```

Secondly, it’s not properly quantified:

```scala> val x = const _
x: (Nothing) => (Any) => Nothing = <function1>
```

That type should be `[A,B](A => B => A)`. That is, the function `x` should be polymorphic in its arguments.

This exposes a shortcoming with a fundamental design decision about how functions are represented in Scala. The representation is a little bit naive, but suffices for most day-to-day coding. But, for higher-order programming (like abstracting over combinator libraries), specifically to properly encode the constant function, what’s needed is a representation similar to this:

```// The identity functor that maps every type to itself
type Id[A] = A

// A constant functor that maps every type to A
trait Const[A] { type Apply[B] = A }

// A natural transformation between functors
trait ~>[F[_],G[_]] { def apply[B](f: => F[B]): G[B] }

// A natural transformation from the identity functor to the constant functor,
// or if you like, the type of functions that return A but are
// polymorphic in their argument.
type K[A] = Id ~> Const[A]#Apply

// The non-strict, universally quantified constant function.
def const = new (Id ~> K) {
def apply[A](a: => A) = new K[A] {
def apply[B](b: => B) = a
}
}
```

This is now sufficiently lazy and properly quantified:

```scala> val x = const
x: java.lang.Object with ~>[Id,K] = \$anon\$1@8f84a7

scala> val y = x(7)
y: K[Int] = \$anon\$1\$\$anon\$2@1eb89ca

scala> val z = y(error("too strict"))
z: Int = 7
```

We can implicitly convert various applications of `~>` to regular old `Function1`. For example:

```implicit def kToFn[A,B](f: K[A]) = (b: B) => f(b): A
```

Which lets us now use our universally quantified nonstrict constant function in the usual manner:

```scala> val x = List(1,2,3) map const(7)
x: List[Int] = List(7, 7, 7)
```

# Scala, Folds, and Universal Quantification

Church encoding of data types is a fun exercise. Something that blew my mind while learning functional programming was that a data structure is completely defined by its catamorphism. So for example, foldr is not just another function over lists. The list data type is the foldr function.

For example, in Haskell, we can encode pairs as this function:

```pair x y f = f x y
```

A pair is then a higher-order function. It takes a function with two arguments and yields the result of applying that function to the two elements with which we constructed the pair.

Doing this in Scala is not quite as pretty. Here’s an attempt:

```def pair[A,B,C](a: A, b: B) = (f: (A,B) => C) => f(a,b)
```

Seems to work:

```scala> pair(10,20)(_ + _)
res1: Int = 30
```

However, that C type parameter is going to give us problems if we try this:

```scala> val x = pair(10,20)
x: ((Int, Int) => Nothing) => Nothing = <function>

scala> x(_ + _)
<console>:12: error: type mismatch;
found   : Int
required: Nothing
x(_ + _)
^
```

Oops. It looks like Scala needs all of the type parameters to a function up front. In other words, it seems like its type system is unable to unify the types (∀ a. a -> (∀ b. b -> b)) and (∀ a b. a -> b -> b). Is this accurate? If you know the answer, please comment below.

However, we can be saved with anonymous type syntax (which, I’m told, unfortunately makes use of reflection):

```def pair[A,B](a: A, b: B) = new { def apply[C](f: (A,B) => C) = f(a,b) }
```

Now this works as expected:

```scala> val x = pair(1,2)
x: java.lang.Object{def apply[C]((Int, Int) => C): C} = \$anon\$1@ad8dbc

scala> x(_ + _)
res13: Int = 3
```

Sweet! Let’s do this for lists. Here’s the Haskell.

```nil p z = z
cons x xs p z = p x (xs p z)
```

Testing this in GHCi:

```Prelude> let xs = cons 1 (cons 2 (cons 3 nil))
Prelude> xs (+) 0
6
```

No sweat. Now, let’s do this in Scala. This is the best I’ve come up with:

```def nil =
new { def apply[A](a: A) =
new { def apply[B](b: B) = b }}
def cons[A](x: A) =
new { def apply[B](xs: ((A => B => B) => B => B)) =
(f: A => B => B) => (b:B) => f(x)(xs(f)(b)) }
```

This doesn’t completely work:

```scala> val xs = cons(1)(cons(2)(cons(3)(nil)))
<console>:20: error: type mismatch;
found   : java.lang.Object{def apply[A](A): java.lang.Object{def apply[B](B): B}}
required: ((Int) => (?) => ?) => (?) => ?
val xs = cons(1)(cons(2)(cons(3)(nil)))
^
```

Scala is not able to unify those two types. Let’s help it along:

```def objToFun[A,B](o: {def apply[A](a: A): {def apply[B](b: B): B}}) = (a: A) => (b: B) => o(a)(b)
def nilp[A,B] = objToFun[A => B => B, B](nil)
```

With a little annotation, we can now create a list that has the right type:

```scala> cons(3)(cons(2)(cons(1)(nilp[Int,Int])))
xs: ((Int) => (Int) => Int) => (Int) => Int = <function>

scala> xs(x => y => x + y)(0)
res44: Int = 6
```

Not terrible, but can we do better? Can this be done without the anonymous type syntax? Is using that syntax necessarily bad? Why? Could we modify Scala to get a nicer notation for anonymous function types? Is rank-2 polymorphism required for that, or can we convince the compiler to move universal quantifiers to the left of a single arrow?