Вывод типа для модели данных исчисления скала-комбинатора - PullRequest
Новая
       48

Вывод типа для модели данных исчисления скала-комбинатора

9 голосов
/ 25 декабря 2010

Я пробую очень легкое кодирование исчисления комбинаторов в scala.Сначала я просто использую комбинаторы S и K, приложения и константы.Позже я надеюсь поднять функции scala и разрешить оценку выражения как функции scala.Однако это на потом.Вот что у меня пока есть. 

/** Combinator expression */
sealed abstract class CE

/** Application: CE| (x y) <=> LC| (x:(A=>B) y:A) : B */
case class Ap[A <: CE, B <: CE, X](e1: A, e2: B) extends CE

/** A raw value with type */
case class Value[T](v: T) extends CE

/** Some combinator */
sealed abstract class Comb extends CE

/** The S combinator: CE| S x y z
 *                    LC| λx:(A=>B=>C).λy:(A=>B).λz:A.(x z (y z)) : C
 *  S : ∀A.∀B.∀C. (A => B => C) => (A => B) => A => C
 */
case object S extends Comb
/** The K combinator: CE| K x y
 *                    LC| λx:A.λy:B.x:A : A
 *  K : ∀A => ∀B => A
 */
case object K extends Comb

Теперь я хотел бы сделать какой-то вывод типа по этому поводу.Для простоты реализации сокращения малых и больших шагов модель данных не типизирована, поэтому я бы хотел, чтобы типы были внешними по отношению к этой структуре.Давайте введем кое-что для хранения информации о типе. 

trait TypeOf { type typeOf }

Тип значения прост. 

implicit def typeOfValue[T](vt: Value[T]) : TypeOf =
    new TypeOf { type typeOf = T }

Приложение немного сложнее, но в основном сводится к приложению-функции.Давайте введем тип ⊃ для приложения комбинатора, чтобы избежать путаницы с обычным приложением scala. 

/** Combinator application */
class ⊃[+S, -T]

implicit def typeOfAp[Ap[A, B], A <: CE, B <: CE], X, Y](Ap(A, B)
  (implicit aIsFXY: A#typeOf =:= (X⊃Y), bIsX: B#typeOf =:= X) : TypeOf =
      { type typeOf = Y }

Вот где я застреваю.Мне нужно представить тип комбинаторов S и K.Тем не менее, они являются универсально определенными типами.Вы не знаете их фактический тип, пока не начнете применять их.Давайте возьмем в качестве примера K. 

(K x:X y:Y) : X
(K x:X) : ∀Y.Y => X
(K) : ∀X.x => ∀Y.Y => X

Первые пару раз, когда я пытался работать с этим, я делаю K параметризованным как K [X, Y], но это (катастрофически) недостаточно полиморфно.Тип K должен ожидать тип первого аргумента, а затем следующего.Если вы применяете K только к одному значению, тогда тип следующего аргумента еще не должен быть фиксированным.Вы должны быть в состоянии взять (K x: X) и применить его к строке, или к int, или к любому другому типу, который вам нравится.

Так что моя проблема заключается в том, как написать неявное, которое генерирует typeOf для Sи K, и как правильно обрабатывать ∀-количественные типы.Возможно, я хочу что-то вроде этого? 

implicit def typeOfK(k: K.type): TypeOf = { type typeOf = ∀[X, X ⊃ (∀[Y, Y⊃X])] }

Однако я не уверен, как мне следует писать ∀-тип, чтобы выполнять сантехнику.У меня такое ощущение, что в дополнение к правильному пониманию type, у typeOfAp будет неявный второй обработчик случая A # typeOf =: = ∀ [...] в дополнение к выходу A # typeOf =: = ⊃ [...] один.

Спасибо,

Мэтью

1 Ответ

1 голос
/ 08 марта 2011

Помогает ли это? 

trait λ {
    type ap[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]]
        }
    }
}

type I = S#ap[K]#ap[K]

def ap[X<:λ,Y<:λ](x:X,y:Y): X#ap[Y]
...