Замыкания и универсальная количественная оценка

Я пытался понять, как реализовать в Scala типы данных, закодированные в формате Church. Кажется, что для этого требуются типы ранга n, поскольку вам понадобится первоклассная функция const типа forAll a. a -> (forAll b. b -> b).

Однако мне удалось закодировать пары таким образом:

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)
  }

Для списков мне удалось закодировать 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))
  }
}

Однако пустой список более проблематичен, и мне не удалось заставить компилятор Scala унифицировать типы.

Можете ли вы определить nil, чтобы с учетом приведенного выше определения компилировалось следующее?

cons(1)(cons(2)(cons(3)(nil)))

closures scala functional-programming quantifiers church-encoding
person Apocalisp    schedule 08.04.2010    source источник
comment
Вот один из вариантов использования числительных Черча в Scala: -mcbeath.blogspot.com/2008/11/   -  person Randall Schulz    schedule 08.04.2010
comment
Рэндалл: Это церковные числительные на уровне типа. То, что я делаю, не на уровне типов.   -  person Apocalisp    schedule 08.04.2010
comment
Что бы это ни стоило, методы Scala эффективно дают вам ранг n типов.   -  person Owen    schedule 14.01.2013
comment
Методы Scala не дают вам эффективно типы ранга n, но таким образом вы можете закодировать большое количество типов ранга n.   -  person Apocalisp    schedule 14.01.2013

Ответы (1)


arrow_upward
11
arrow_downward

Спасибо Марку Харра за завершение этого решения. Хитрость в том, что Function1 в стандартных библиотеках не определяется достаточно общим образом.

Моя черта «Замыкание» в вопросе на самом деле является естественным преобразованием между функторами. Это обобщение понятия «функция».

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

Тогда функция a -> b должна быть специализацией этого признака, естественным преобразованием между двумя эндофункторами в категории типов Scala.

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

Const[A] — это функтор, который отображает каждый тип в A.

И вот наш тип списка:

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

Здесь Endo — это просто псевдоним для типа функций, которые отображают тип на себя (эндофункция).

type Endo[A] = A ->: A

А Fold — это тип функций, которые могут сворачивать список:

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

И, наконец, вот наши конструкторы списков:

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
}

Одним из предостережений является необходимость явного преобразования (A ->: B) в (A => B), чтобы помочь системе типов Scala. Так что по-прежнему ужасно многословно и утомительно сворачивать список после его создания. Вот эквивалентный Haskell для сравнения:

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

Построение и свертывание списков в версии для Haskell лаконичные и бесшумные:

let xs = cons 1 (cons 2 (cons 3 nil)) in xs (+) 0
person Apocalisp    schedule 08.04.2010
comment
Это так вне моей зоны комфорта! - person Andriy Drozdyuk; 19.02.2011