L'inferenza di tipo per un modello di dati di calcolo scala combinatore

Question

Sto provando una codifica molto leggero di Combinator calcolo in scala. Inizialmente, sto solo un'attuazione delle S e combinatori K, applicazione e valori costanti. Più tardi spero di alzare le funzioni Scala di e consentire la valutazione di un'espressione come una funzione Scala. Tuttavia, questo è per dopo. Ecco quello che ho finora.

/** 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

Ora vorrei fare un certo tipo di inferenza su questo. Per semplicità di implementazione riduzione piccola e grande passo, il modello di dati non è tipizzato, quindi vorrei tipi di essere esterni a questa struttura. Introduciamo qualcosa per contenere le informazioni di tipo.

trait TypeOf { type typeOf }

Il tipo di valore è semplice.

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

L'applicazione è un po 'più complicato, ma in fondo si riduce a l'applicazione di funzioni. Introduciamo un tipo ? per l'applicazione combinatore, per evitare confusione con normale applicazione 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 }

Questo è dove mi si blocca. Ho bisogno di rappresentare il tipo dei combinatori S e K. Tuttavia, essi sono universalmente tipi quantificati. Non si conosce il loro tipo effettivo fino a quando si inizia ad applicare loro. Prendiamo K come esempio.

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

Il primo paio di volte ho provato a lavorare con questo, faccio K parametrizzato come K [X, Y], ma questo è (catastroficamente) insufficientemente polimorfico. Il tipo di K dovrebbe essere in attesa per il tipo del primo argomento, e quindi del successivo. Se si applica K a un solo valore, quindi il tipo di argomento successivo deve ancora essere risolto. Dovreste essere in grado di prendere (K x: X). E applicarlo a una stringa, o per un int o di qualsiasi tipo ti piace

Quindi il mio problema è come scrivere l'implicito che genera il TypeOf per S e K, e come gestire correttamente i tipi ?-quantificato. Forse voglio qualcosa di simile?

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

Tuttavia, non sono sicuro di come dovrei essere iscritto il tipo ? a fare l'impianto idraulico. Ho la sensazione che, oltre ad ottenere ? destra, ci sarà una seconda implicito per typeOfAp gestire la A # TypeOf =: = ? [...] caso oltre al uscendo A # TypeOf =: = ? [ ...] uno.

Grazie,

Matthew

Answer 1

Fa questo aiuto?

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]