¿Cómo implementar un "pliegue generalizado eficiente" en F#?

nested polymorphism

Question

En el artículo de Martin et al. Leí sobre pliegues generalizados eficientes para los tipos de datos de nestet. El periódico habla sobre Haskell y quiero probarlo en F #.

Hasta ahora he logrado seguir el ejemplo de Nest incluida la implementación de gfold .

type Pair<''a> = ''a * ''a
type Nest<''a> = Nil | Cons of ''a * Nest<Pair<''a>>
let example =
Cons(1,
Cons((2, 3),
Cons(((4, 5), (6, 7)),
Nil
)
)
)
let pair (f:''a -> ''b) ((a, b):Pair<''a>) : Pair<''b> = f a, f b
let rec nest<''a, ''r> (f:''a -> ''r) : Nest<''a> -> Nest<''r> = function
| Nil -> Nil
| Cons(x, xs) -> Cons(f x, nest (pair f) xs)
//val gfold : e:''r -> f:(''a * ''r -> ''r) -> g:(Pair<''a> -> ''a) -> _arg1:Nest<''a> -> ''r
let rec gfold e f g : Nest<''a> -> ''r = function
| Nil -> e
| Cons(x, xs) ->
f(x, gfold e f g (nest g xs))
let uncurry f (a, b) = f a b
let up = uncurry (+)
let sum = example |> gfold 0 up up

Desafortunadamente, gfold parece tener una complejidad cuadrática y es por eso que los autores se acercaron con el efold . Como probablemente puedas adivinar, ese es el que no pude poner en práctica. Después de jugar con muchas anotaciones tipo, se me ocurrió esta versión que solo tiene un pequeño garabato:

let rec efold<''a, ''b, ''r> (e:''r) (f:''a * ''r -> ''r) (g:(Pair<''a> -> Pair<''a>) -> ''a -> ''a) (h:_) (nest:Nest<''a>) : ''r =
match nest with
| Nil -> e
| Cons(x, xs) -> f(h x, efold e f g ((g << pair) h) xs)
^^

El único tipo no especificado restante es el de h . El compilador infiere val h : (''a -> ''a) pero creo que debe haber diferentes tipos.

El mensaje de error proporcionado dice

Tipo de error no coincide. Esperando un
Nest <''a>
pero dado un
Nest <Pair <''a >>
El tipo resultante sería infinito al unir '''' a ''y'' Pair <''a>''

Con el tipo correcto de h el error debería desaparecer. Pero no entiendo lo suficiente a Haskell para traducirlo a F #.

Ver también esta discusión sobre un posible error tipográfico en el documento.

Actualización: Esto es lo que entiendo de la respuesta de kvb :

Entonces h transforma un tipo de entrada en un tipo intermedio, como en un doblez regular donde el acumulador puede ser de tipo diferente. g se usa luego para reducir dos valores tipeados intermedios a uno, mientras que f obtiene un tipo intermedio y un tipo de entrada para producir los valores tipados de salida. Por supuesto, e también es de ese tipo de salida.

h hecho se aplica directamente a los valores encontrados durante la recursión. g por otro lado, solo se usa para hacer que h sea aplicable a tipos progresivamente más profundos.

Simplemente mirando los primeros ejemplos, por sí solo no parece hacer mucho trabajo aparte de aplicar h y alimentar la recursión. Pero en el enfoque sofisticado puedo ver que es el más importante de todos. lo que sale, es decir, es el caballo de batalla.

¿Es eso correcto?

Answer 1

La definición correcta de efold en Haskell es algo así como:

efold :: forall n m b.
(forall a. n a)->
(forall a.(m a, n (Pair a)) -> n a)->
(forall a.Pair (m a) -> m (Pair a))->
(forall a.(a -> m b) -> Nest a -> n b)
efold e f g h Nil = e
efold e f g h (Cons (x,xs)) = f (h x, efold e f g (g . pair h) xs

Esto no se puede traducir a F # en generalidad completa porque n y m son "tipos de alto grado" - son constructores de tipos que crean un tipo cuando se les da un argumento - que no son compatibles con F # (y no tienen una representación limpia en .RED).

Interpretación

Su actualización le pregunta cómo interpretar los argumentos al doblez. Tal vez la forma más fácil de ver cómo funciona el doblez es expandir lo que sucede cuando aplica el doblez a su ejemplo. Obtendrías algo como esto:

efold e f g h example ≡
f (h 1, f ((g << pair h) (2, 3), f ((g << pair (g << pair h)) ((4,5), (6,7)), e)))

Entonces h mapea los valores en el tipo que puede servir como el primer agumento de f. g se usa para aplicar h a pares anidados más profundamente (para que podamos pasar de usar h como una función de tipo a -> mb a Pair a -> m (Pair b) para Pair (Pair a) -> m (Pair (Pair b)) etc.), f se aplica repetidamente en el lomo para combinar los resultados de h con los resultados de las llamadas anidadas a f . Finalmente, e se usa exactamente una vez, para servir como la semilla de la llamada más anidada a f .

Creo que esta explicación está más de acuerdo con lo que has deducido. f es ciertamente crítico para combinar los resultados de las diferentes capas. Pero también es importante, ya que te dice cómo combinar las piezas dentro de una capa (por ejemplo, al sumar los nodos, debe sumar las sumas anidadas izquierda y derecha, si querías usar un pliegue para construir un nuevo nido donde el los valores en cada nivel se invierten de los de la entrada, se usaría una g que se parece más o menos a la fun (a,b) -> b,a ).

Enfoque simple

Una opción es crear implementaciones especializadas de efold para cada par de n , m te interesen. Por ejemplo, si queremos sumar las longitudes de las listas contenidas en un Nest , n _ y m _ serán ambos int . Podemos generalizar ligeramente, al caso donde n _ y m _ no dependen de sus argumentos:

let rec efold<''n,''m,''a> (e:''n) (f:''m*''n->''n) (g:Pair<''m> -> ''m) (h:''a->''m) : Nest<''a> -> ''n = function
| Nil -> e
| Cons(x,xs) -> f (h x, efold e f g (g << (pair h)) xs)
let total = efold 0 up up id example

Por otro lado, si n y m usan sus argumentos, entonces necesitarías definir una especialización separada (además, puedes necesitar crear nuevos tipos para cada argumento polimórfico, ya que la codificación de tipos de rango superior de F # es incómoda) . Por ejemplo, para recopilar los valores de un nido en una lista, quiere n ''a = list<''a> y m ''b = ''b . Entonces, en lugar de definir nuevos tipos para el tipo de argumento de e podemos observar que el único valor de tipo forall ''a.list<''a> es [] , por lo que podemos escribir:

type ListIdF =
abstract Apply : ''a * list<Pair<''a>> -> list<''a>
type ListIdG =
abstract Apply : Pair<''a> -> Pair<''a>
let rec efold<''a,''b> (f:ListIdF) (g:ListIdG) (h:''a -> ''b) : Nest<''a> -> list<''b> = function
| Nil -> []
| Cons(x,xs) -> f.Apply(h x, efold f g (pair h >> g.Apply) xs)
let toList n = efold { new ListIdF with member __.Apply(a,l) = a::(List.collect (fun (x,y) -> [x;y]) l) } { new ListIdG with member __.Apply(p) = p } id n

Enfoque sofisticado

Mientras que F # no admite directamente tipos de mayor nivel, resulta que es posible simularlos de una manera un tanto fiel. Este es el enfoque adoptado por la biblioteca superior . Así es como se vería una versión mínima de eso.

Creamos un tipo de App<''T,''a> que representará algún tipo de aplicación T<''a> , pero donde crearemos un tipo de acompañante ficticio que puede servir como primer argumento de tipo para la App<_,_> :

type App<''F, ''T>(token : ''F, value : obj) =
do
if obj.ReferenceEquals(token, Unchecked.defaultof<''F>) then
raise <| new System.InvalidOperationException("Invalid token")
// Apply the secret token to have access to the encapsulated value
member self.Apply(token'' : ''F) : obj =
if not (obj.ReferenceEquals(token, token'')) then
raise <| new System.InvalidOperationException("Invalid token")
value 

Ahora podemos definir algunos tipos complementarios para los constructores de tipos que nos importan (y estos generalmente pueden vivir en alguna biblioteca compartida):

// App<Const<''a>, ''b> represents a value of type ''a (that is, ignores ''b)
type Const<''a> private () =
static let token = Const ()
static member Inj (value : ''a) =
App<Const<''a>, ''b>(token, value)
static member Prj (app : App<Const<''a>, ''b>) : ''a =
app.Apply(token) :?> _
// App<List, ''a> represents list<''a>
type List private () =
static let token = List()
static member Inj (value : ''a list) =
App<List, ''a>(token, value)
static member Prj (app : App<List, ''a>) : ''a list =
app.Apply(token) :?> _
// App<Id, ''a> represents just a plain ''a
type Id private () =
static let token = Id()
static member Inj (value : ''a) =
App<Id, ''a>(token, value)
static member Prj (app : App<Id, ''a>) : ''a =
app.Apply(token) :?> _
// App<Nest, ''a> represents a Nest<''a>
type Nest private () =
static let token = Nest()
static member Inj (value : Nest<''a>) =
App<Nest, ''a>(token, value)
static member Prj (app : App<Nest, ''a>) : Nest<''a> =
app.Apply(token) :?> _

Ahora podemos definir los tipos de rango superior para los argumentos del fold eficiente de una vez por todas:

// forall a. n a
type E<''N> =
abstract Apply<''a> : unit -> App<''N,''a>
// forall a.(m a, n (Pair a)) -> n a)
type F<''M,''N> =
abstract Apply<''a> : App<''M,''a> * App<''N,''a*''a> -> App<''N,''a>
// forall a.Pair (m a) -> m (Pair a))
type G<''M> =
abstract Apply<''a> : App<''M,''a> * App<''M,''a> -> App<''M,''a*''a>

para que el doblez sea justo:

let rec efold<''N,''M,''a,''b> (e:E<''N>) (f:F<''M,''N>) (g:G<''M>) (h:''a -> App<''M,''b>) : Nest<''a> -> App<''N,''b> = function
| Nil -> e.Apply()
| Cons(x,xs) -> f.Apply(h x, efold e f g (g.Apply << pair h) xs)

Ahora, para llamar a " efold " necesitamos rociar en algunas llamadas a los diversos métodos Inj y Prj , pero de lo contrario todo se ve mucho como esperábamos:

let toList n =
efold { new E<_> with member __.Apply() = List.Inj [] }
{ new F<_,_> with member __.Apply(m,n) = Id.Prj m :: (n |> List.Prj |> List.collect (fun (x,y) -> [x;y])) |> List.Inj }
{ new G<_> with member __.Apply(m1,m2) = (Id.Prj m1, Id.Prj m2) |> Id.Inj }
Id.Inj
n
|> List.Prj
let sumElements n =
efold { new E<_> with member __.Apply() = Const.Inj 0 }
{ new F<_,_> with member __.Apply(m,n) = Const.Prj m + Const.Prj n |> Const.Inj }
{ new G<_> with member __.Apply(m1,m2) = Const.Prj m1 + Const.Prj m2 |> Const.Inj }
Const.Inj
n
|> Const.Prj
let reverse n =
efold { new E<_> with member __.Apply() = Nest.Inj Nil }
{ new F<_,_> with member __.Apply(m,n) = Cons(Id.Prj m, Nest.Prj n) |> Nest.Inj }
{ new G<_> with member __.Apply(m1,m2) = (Id.Prj 2, Id.Prj m1) |> Id.Inj }
Id.Inj
n
|> Nest.Prj

Esperemos que el patrón aquí sea claro: en cada expresión de objeto, el método de aplicación proyecta cada argumento, opera sobre ellos y luego inyecta el resultado en un tipo de App<_,_> . Con un poco inline magia en inline , podemos hacer que este aspecto sea aún más uniforme (a costa de algunas anotaciones de tipo):

let inline (|Prj|) (app:App< ^T, ''a>) = (^T : (static member Prj : App< ^T, ''a> -> ''b) app)
let inline prj (Prj x) = x
let inline inj x = (^T : (static member Inj : ''b -> App< ^T, ''a>) x)
let toList n =
efold { new E<List> with member __.Apply() = inj [] }
{ new F<Id,_> with member __.Apply(Prj m, Prj n) = m :: (n |> List.collect (fun (x,y) -> [x;y])) |> inj }
{ new G<_> with member __.Apply(Prj m1,Prj m2) = (m1, m2) |> inj }
inj
n
|> prj
let sumElements n =
efold { new E<Const<_>> with member __.Apply() = inj 0 }
{ new F<Const<_>,_> with member __.Apply(Prj m, Prj n) = m + n |> inj }
{ new G<_> with member __.Apply(Prj m1,Prj m2) = m1 + m2 |> inj }
inj
n
|> prj
let reverse n =
efold { new E<_> with member __.Apply() = Nest.Inj Nil }
{ new F<Id,_> with member __.Apply(Prj m,Prj n) = Cons(m, n) |> inj }
{ new G<_> with member __.Apply(Prj m1,Prj m2) = (m2, m1) |> inj }
inj
n
|> prj