Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Closures and universal quantification

I've been trying to work out how to implement Church-encoded data types in Scala. It seems that it requires rank-n types since you would need a first-class const function of type forAll a. a -> (forAll b. b -> b).

However, I was able to encode pairs thusly:

import scalaz._

trait Compose[F[_],G[_]] { type Apply = F[G[A]] }

trait Closure[F[_],G[_]] { def apply[B](f: F[B]): G[B] }

def pair[A,B](a: A, b: B) =
  new Closure[Compose[({type f[x] = A => x})#f,
                      ({type f[x] = B => x})#f]#Apply, Id] {
    def apply[C](f: A => B => C) = f(a)(b)
  }

For lists, I was able to encode cons:

def cons[A](x: A) = {
  type T[B] = B => (A => B => B) => B
  new Closure[T,T] {
    def apply[B](xs: T[B]) = (b: B) => (f: A => B => B) => f(x)(xs(b)(f))
  }
}

However, the empty list is more problematic and I've not been able to get the Scala compiler to unify the types.

Can you define nil, so that, given the definition above, the following compiles?

cons(1)(cons(2)(cons(3)(nil)))
like image 463
Apocalisp Avatar asked Apr 08 '10 17:04

Apocalisp


People also ask

What are the 2 types of quantification?

There are two types of quantifiers: universal quantifier and existential quantifier.

What is the difference between universal quantification and existential quantification?

The universal quantifier, meaning "for all", "for every", "for each", etc. The existential quantifier, meaning "for some", "there exists", "there is one", etc.

What is universal quantification in logic?

In mathematical logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any" or "for all". It expresses that a predicate can be satisfied by every member of a domain of discourse.

What does universal quantifier meaning?

Definition of universal quantifier : a logical quantifier that asserts all values of a given variable in a formula.


1 Answers

Thanks to Mark Harrah for completing this solution. The trick is that Function1 in the standard libraries is not defined in a general enough way.

My "Closure" trait in the question is actually a natural transformation between functors. This is a generalization of the concept of "function".

trait ~>[F[_],G[_]] { def apply[B](f: F[B]): G[B] }

A function a -> b then ought to be a specialization of this trait, a natural transformation between two endofunctors on the category of Scala types.

trait Const[A] { type Apply[B] = A }
type ->:[A,B] = Const[A]#Apply ~>: Const[B]#Apply

Const[A] is a functor that maps every type to A.

And here's our list type:

type CList[A] = ({type f[x] = Fold[A,x]})#f ~> Endo

Here, Endo is just an alias for the type of functions that map a type onto itself (an endofunction).

type Endo[A] = A ->: A

And Fold is the type of functions that can fold a list:

type Fold[A,B] = A ->: Endo[B]

And then finally, here are our list constructors:

def cons[A](x: A) = {
  new (CList[A] ->: CList[A]) {
    def apply[C](xs: CList[A]) = new CList[A] {
      def apply[B](f: Fold[A,B]) = (b: B) => f(x)(xs(f)(b))
    }
  }
}

def nil[A] = new CList[A] {
  def apply[B](f: Fold[A,B]) = (b: B) => b
}

One caveat is the need to explicitly convert (A ->: B) to (A => B) to help Scala's type system along. So it's still terribly verbose and tedious to actually fold a list once created. Here's the equivalent Haskell for comparison:

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

List construction and folding in the Haskell version is terse and noise-free:

let xs = cons 1 (cons 2 (cons 3 nil)) in xs (+) 0
like image 139
Apocalisp Avatar answered Sep 19 '22 21:09

Apocalisp