¿La "Restricción de valor" significa prácticamente que no hay una programación funcional de orden superior?

Question

¿La "Restricción de valor" significa prácticamente que no hay una programación funcional de orden superior?

Tengo el problema de que cada vez que trato de hacer un poco de HOP me atrapa un error de VR. Ejemplo:

let simple (s:string)= fun rq->1 
let oops= simple "" 

type 'a SimpleType= F of (int ->'a-> 'a) 
let get a = F(fun req -> id) 
let oops2= get "" 

y me gustaría saber si se trata de un problema de una aplicación prticular de VR o se trata de un problema general que no tiene solución en un lenguaje de tipo infered mutable que no incluye mutación en el sistema de tipo.

Answer 1

No sabía los detalles de la restricción de valor, por lo que busqué y encontré this article. Aquí está la parte relevante:

Obviamente, no vamos a escribir la expresión rev [] en un programa, por lo que no es particularmente importante que no sea polimórfico. Pero, ¿y si creamos una función usando una llamada a función? Con funciones al curry, lo hacemos todo el tiempo:

- val revlists = map rev; 

Aquí revlists deben ser polimórficos, pero la restricción de valor nos puede confundir:

- val revlists = map rev; 
stdIn:32.1-32.23 Warning: type vars not generalized because of 
    value restriction are instantiated to dummy types (X1,X2,...) 
val revlists = fn : ?.X1 list list -> ?.X1 list list 

Afortunadamente, hay un truco simple que podemos utilizar hacer revolistas polimórficos Podemos reemplazar la definición de revlists con

- val revlists = (fn xs => map rev xs); 
val revlists = fn : 'a list list -> 'a list list 

y ahora todo funciona bien, ya que (fn => xs xs mapa rev) es un valor sintáctico. (equivalente, que podría haber utilizado la sintaxis diversión más comunes:.

- fun revlists xs = map rev xs; 
val revlists = fn : 'a list list -> 'a list list 

con el mismo resultado) En la literatura, el truco de la sustitución de una expresión de función de valor e con (fn x => Ex) es conocido como expansión de eta Se ha encontrado empíricamente que la expansión eta por lo general es suficiente para hacer frente a la restricción de valor.

Para resumir, no parece que la programación de orden superior esté restringida tanto como la programación sin puntos. Esto podría explicar algunos de los problemas que tengo al traducir el código Haskell a F #.

---

Editar: En concreto, aquí es cómo fijar el primer ejemplo:

let simple (s:string)= fun rq->1 
let oops= (fun x -> simple "" x)  (* eta-expand oops *) 

type 'a SimpleType= F of (int ->'a-> 'a) 
let get a = F(fun req -> id) 
let oops2= get "" 

no he descubierto que el segundo todavía porque el constructor de tipos está recibiendo en el camino.

Answer 2

¿La "Restricción de valor" significa que no hay una programación funcional de orden superior?

Absolutely not! La restricción de valor apenas interfiere con la programación funcional de orden superior. Lo que no hacer es restringir algunas aplicaciones de polimórficos funciones — no funciones de orden superior — en el nivel superior.

---

Veamos su ejemplo. Su problema es que oops y oops2 son ambos la función de identidad y tienen tipo forall 'a . 'a -> 'a. En otras palabras, cada uno es un valor polimórfico. Pero el lado derecho no es un llamado "valor sintáctico"; es una aplicación de función. (Una aplicación de función no puede devolver un valor polimórfico porque si fuera así, podría construir una función hacky usando referencias mutables y listas que podrían subvertir el sistema de tipo; es decir, podría escribir una función de terminación tipo forall 'a 'b . 'a -> 'b.

casos Afortunadamente, en casi todos los prácticos, el valor polimórfico en cuestión es una función, y se pueden definir por ETA en expansión:

let oops x = simple "" x 

Este idioma parece que tiene algún costo en tiempo de ejecución, pero dependiendo de el inliner y el optimizador, que pueden ser eliminados por el compilador —, es solo el tipoche que tiene problemas.

El ejemplo oops2 es más problemático porque usted tiene que hacer y deshacer el valor constructor:

let oops2 = F(fun x -> let F f = get "" in f x) 

Este es un buen pero más tedioso, pero la función anónima fun x -> ... es un valor sintáctico y F es una constructor de tipo de datos, y un constructor aplicado a un valor sintáctico es también un valor sintáctico, y Bob es tu tío. El embalaje y desembalaje de F se compilará en la función de identidad, por lo que oops2 va a compilar en exactamente el mismo código de máquina que oops.

Las cosas son aún más desagradables cuando se desea que un cálculo en tiempo de ejecución devuelva un valor polimórfico como None o []. Como insinuado por Nathan Sanders, puede ir en contra de la restricción de valor con una expresión tan simple como rev []:

Standard ML of New Jersey v110.67 [built: Sun Oct 19 17:18:14 2008] 
- val l = rev []; 
stdIn:1.5-1.15 Warning: type vars not generalized because of 
    value restriction are instantiated to dummy types (X1,X2,...) 
val l = [] : ?.X1 list 
- 

Nada de orden superior no! Y sin embargo, la restricción de valor se aplica.

En la práctica la restricción de valor no presenta ninguna barrera para la definición y el uso de las funciones de orden superior; simplemente expandes eta

Answer 3

Aquí está the answer to this question en el contexto de F #. Para resumir, en F # pasar un argumento de tipo a una función genérica (= polimórfica) es una operación en tiempo de ejecución, por lo que en realidad es seguro de generalizar (como en, no se bloqueará en tiempo de ejecución). Sin embargo, el comportamiento del valor así generalizado puede ser sorprendente.

Para este ejemplo en particular en Fa #, se puede recuperar la generalización con una anotación de tipo y un parámetro de tipo explícito:

type 'a SimpleType= F of (int ->'a-> 'a) 
let get a = F(fun req -> id) 
let oops2<'T> : 'T SimpleType = get ""