Adder generico da Idris a Scala?

Question

Type Driven Development with Idris presenta il seguente approccio vipera generico:

AdderType : (numArgs : Nat) -> Type 
AdderType Z  = Int 
AdderType (S k) = (next : Int) -> AdderType k 

adder : (n : Nat) -> (acc : Int) -> AdderType n 
adder Z acc  = acc 
adder (S k) acc = \x => (adder k (x+acc)) 

Esempio:

-- expects 3 Int's to add, with a starting value of 0 
*Work> :t (adder 3 0) 
adder 3 0 : Int -> Int -> Int -> Int 

-- 0 (initial) + 3 + 3 + 3 == 9 
*Work> (adder 3 0) 3 3 3 
9 : Int 

Sto indovinando che shapeless in grado di gestire la funzione generica sopra adder.

Come può essere scritto in Scala con o senza informi?

Answer 1

Aggiornamento: Lascio la mia implementazione originale sotto, ma ecco uno che è un po 'più diretto:

import shapeless._ 

trait AdderType[N <: Nat] extends DepFn1[Int] 

object AdderType { 
    type Aux[N <: Nat, Out0] = AdderType[N] { type Out = Out0 } 
    def apply[N <: Nat](base: Int)(implicit at: AdderType[N]): at.Out = at(base) 

    implicit val adderTypeZero: Aux[Nat._0, Int] = new AdderType[Nat._0] { 
    type Out = Int 
    def apply(x: Int): Int = x 
    } 

    implicit def adderTypeSucc[N <: Nat](implicit 
    atN: AdderType[N] 
): Aux[Succ[N], Int => atN.Out] = new AdderType[Succ[N]] { 
    type Out = Int => atN.Out 
    def apply(x: Int): Int => atN.Out = i => atN(x + i) 
    } 
} 

E poi:

scala> val at3 = AdderType[Nat._3](0) 
at3: Int => (Int => (Int => Int)) = <function1> 

scala> at3(3)(3)(3) 
res8: Int = 9 

risposta originale al di sotto.

---

Ecco un off-the-bracciale traduzione Scala:

import shapeless._ 

trait AdderType[N <: Nat] extends DepFn1[Int] { 
    protected def plus(x: Int): AdderType.Aux[N, Out] 
} 

object AdderType { 
    type Aux[N <: Nat, Out0] = AdderType[N] { type Out = Out0 } 

    def apply[N <: Nat](base: Int)(implicit at: AdderType[N]): Aux[N, at.Out] = 
    at.plus(base) 

    private[this] case class AdderTypeZero(acc: Int) extends AdderType[Nat._1] { 
    type Out = Int 
    def apply(x: Int): Int = acc + x 
    protected def plus(x: Int): Aux[Nat._1, Int] = copy(acc = acc + x) 
    } 

    private[this] case class AdderTypeSucc[N <: Nat, Out0](
    atN: Aux[N, Out0], 
    acc: Int 
) extends AdderType[Succ[N]] { 
    type Out = Aux[N, Out0] 
    def apply(x: Int): Aux[N, Out0] = atN.plus(acc + x) 
    protected def plus(x: Int): Aux[Succ[N], Aux[N, Out0]] = copy(acc = acc + x) 
    } 

    implicit val adderTypeZero: Aux[Nat._1, Int] = AdderTypeZero(0) 
    implicit def adderTypeSucc[N <: Nat](implicit 
    atN: AdderType[N] 
): Aux[Succ[N], Aux[N, atN.Out]] = AdderTypeSucc(atN, 0) 
} 

E poi:

scala> val at3 = AdderType[Nat._3](0) 
at3: AdderType[shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless._0]]]] { ... 

scala> at3(3)(3)(3) 
res0: Int = 9 

E 'più prolisso e la rappresentazione è un po' diverso per ottenere la sintassi Scala il nostro "caso base" è essenzialmente uno Int => Int invece di uno Int perché altrimenti non vedo un modo per evitare di dover scrivere apply o () ovunque, ma le idee di base sono esattamente le stesse.

Answer 2

Nel caso in cui siate in viaggio lungo e non abbiate il vostro informe sulle mani, ecco come potete farlo in puro Scala. Può essere utile per coloro che non hanno familiarità con senza forma e coloro che non lo usano per qualche motivo.

Prima di tutto, avremo bisogno di un modo per iterare sui tipi, cioè rappresentare numeri naturali nei tipi. È possibile utilizzare qualsiasi tipo nidificato o semplicemente definirne uno nuovo con alcuni alias per i numeri:

sealed trait Nat 

trait Zero extends Nat 
trait Succ[N <: Nat] extends Nat 

// enough for examples: 
type _0 = Zero 
type _1 = Succ[_0] 
type _2 = Succ[_1] 
type _3 = Succ[_2] 
type _4 = Succ[_3] 
// etc... 

Naturalmente, se si usano spesso tipi come _42 e _342923, sarebbe più conveniente prendere una esistente Tipo Nat con alcune macro-magia per la costruzione di quelle da valori, ma per i nostri esempi è sufficiente.

Ora, il tipo di funzione dipendente AdderType 'abbastanza semplice:

// first we define the type which take a Nat type argument 
trait AdderType[N <: Nat] { 

    type Out 
    def apply(i: Int): Out 
} 

// then we inductively construct its values using implicits 
case object AdderType { 

    // base case: N = _0 
    implicit def zero: 
     AdderType[_0] { type Out = Int } = 
    new AdderType[_0] { 

    type Out = Int 
    def apply(i: Int): Out = i 
    } 

    // induction step: N -> Succ[N] 
    implicit def succ[N <: Nat, NOut](
    implicit prev: AdderType[N] { type Out = NOut } 
): AdderType[Succ[N]] { type Out = Int => NOut } = 
    new AdderType[Succ[N]] { 

    type Out = Int => NOut 
    def apply(i: Int): Out = k => prev(i + k) 
    } 
} 

Ora, per costruire un'istanza di AdderType e applicarlo, si scrive una funzione che prende un N <: Nat come argomento tipo e implicitamente costruisce AdderType[N]:

def adder[N <: Nat](initial: Int)(
    implicit adderFunction: AdderType[N] 
): adderFunction.Out = adderFunction(initial) 

Questo è tutto:

scala> val add3Numbers = adder_[_3](0) 
add3Numbers: Int => (Int => (Int => Int)) = <function1> 

scala> add3Numbers(1)(2)(3) 
res0: Int = 6 

Si può vedere che la soluzione pura non è molto più grande o più complicata di quella che utilizza senza forma (sebbene quest'ultima ci fornisca i tipi pronti per l'uso Nat e DepFn).

---

Un po 'oltre: se (in qualche caso più generale) non si vuole usare adderFunction.Out, che a volte porta a problemi, ho anche una soluzione senza di essa. In questo caso particolare non è migliore, ma lo mostrerò comunque.

Il punto chiave è quello di aggiungere un altro parametro tipo per il tipo out: adder[N <: Nat, NOut], ma d'altra parte non può passare N come un tipo di adder, perché avremo bisogno di scrivere NOut, che vuole essere dedotto (in caso contrario, che cosa è il punto). Così possiamo passare un argomento valore aggiunto, che contribuirà a derivare N Tipo:

def adder[N <: Nat, NOut](n: NatVal[N])(initial: Int)(
    implicit adderFunction: AdderType[N] { type Out = NOut } 
): NOut = adderFunction(initial) 

per costruire NatVal[N] non abbiamo bisogno di creare un'istanza di ogni tipo Nat, possiamo usare un piccolo trucco:

// constructing "values" to derive its type arg 
case class NatVal[N <: Nat]() 

// just a convenience function 
def nat[N <: Nat]: NatVal[N] = NatVal[N]() 

Ora qui è come lo si utilizza:

scala> val add3Numbers = adder(nat[_3])(0) 
add3Numbers: this.Out = <function1> 

scala> add3Numbers(1)(2)(3) 
res1: this.Out = 6 

si può vedere che funziona, ma non ci mostra i tipi effettivi. Tuttavia, questo approccio può funzionare meglio nei casi in cui si hanno diversi impliciti che dipendono dai membri di tipo degli altri. Voglio dire

def foo[AOut]()(implicit 
    a: A { type Out = AOut}, 
    b: B { type In = AOut } 
) ... 

invece di

def foo()(implicit 
    a: A, 
    b: B { type In = a.Out } 
) ... 

Poiché non è possibile reffer a a.Out nella stessa lista degli argomenti.

---

È possibile trovare il codice completo nel mio repo su Github.