enteros de nivel de tipo en ocaml

¿Alguien podría darme sugerencias/consejos para hacer enteros de nivel de tipo en OCaml (3.12) soportando operaciones de suma y resta en ellos?enteros de nivel de tipo en ocaml

Por ejemplo, si tengo números representados así:

type zero 
type 'a succ 
type pos1 = zero succ 
type pos2 = zero succ succ 
...

necesito una manera de definir la función de los tipos de la siguiente manera:

val add: pos2 -> pos1 -> pos3

poco de historia: Estoy intentando conecte un código haskell para operaciones en dimensiones físicas y necesito la capacidad de definir operaciones en tipos de dimensión (registro de 7 entradas de nivel de tipo que representan exponentes de 7 unidades SI básicas). Necesito hacerlo de esta manera para evitar el enlace dinámico (cuando se usan objetos) y para permitir que el compilador evalúe y compruebe estáticamente todas esas expresiones.

Mi comprensión actual es que debería hacer una GADT que implemente operaciones como constructores de tipos, pero todavía estoy luchando con la idea, y cualquier sugerencia sería muy apreciada.

Fuente

2011-08-30 etaoin

También te puede interesar el artículo Many Holes in Hindley-Milner, de Sam Lindley, del Taller 2008 sobre ML.

Fuente

2011-08-31 16:15:47

Acabo de mirar estas diapositivas; la idea es muy simple y genial. Sin embargo, me parece que solo maneja la adición de nivel de tipo. No veo una manera de hacerlo funcionar para restar manteniendo la simplicidad. Si estás rastreando unidades SI, imagino que necesitas sustracción (y enteros negativos). –

@Jeffrey Me disculpo por las ideas que me llegan tan despacio, pero sabes que hay una rama "GADT" en OCaml, ¿verdad? https://sites.google.com/site/ocamlgadt/ (aparentemente, de acuerdo con esa página, los estamos obteniendo con 3.13). –

Sí, he escuchado rumores de que GADT "nativo" vendrá a OCaml en 3.13, van a ser tiempos bastante interesantes. Creo que tal vez el OP (etaion) quiere que algo funcione con la versión actual, pero tal vez la rama GADT sea aceptable. El análisis dimensional parece ser un buen caso de prueba para GADT. (Personalmente, me encantaría ver un ejemplo de código GADT que no sea un intérprete para un idioma pequeño.) Saludos, –

Su ejemplo me hace pensar que está tratando de hacer los números lógicos estilo de prólogo que sería algo así como

type fancyInt = Zero | Succ of fancyInt ;;

a continuación, añadir sería

let rec add a b = match a with Zero -> b | Succ c -> add c (Succ b);;

Sus consejos historia de fondo a una solución diferente, crea una clase que represente distancias. Almacene internamente el valor como necesite para luego proporcionar una interfaz que le permita obtener y establecer la distancia en las unidades necesarias en ese momento. O si desea permanecer con un enfoque funcional, solo cree los tipos para sus unidades y luego tenga funciones de la misma manera que Ocaml maneja tales cosas, es decir, metros_de_km.

Fuente

2011-08-30 15:51:29 stonemetal

Él quiere el tipo y la función que le das, pero al nivel * type *. Es decir, el tipo se convierte en una familia (conjunto) de tipos y sus valores Zero y Succ se convierten en tipos. Y la función agregar se convierte en una función de nivel de tipo, que en OCaml es un tipo parametrizado supongo (?). Este tipo de cosas se hace en Haskell todo el tiempo. No lo he visto en OCaml, lo que sugiere que podría no ser tan fácil. –

Gracias stonemetal, pero como dijo Jeffrey, necesito que esto suceda a nivel de tipo, de modo que el compilador pueda ejecutar esas operaciones en tiempo de compilación y escriba checker para verificar las restricciones. La idea es evitar las comprobaciones de tiempo de ejecución que pueden fallar, dependiendo de las circunstancias cuando se ejecutan (es decir, capturar operaciones semánticamente ilegales, como agregar tiempo a la longitud (no destinado a respaldar la relatividad, simplemente la vieja física newtoniana), mientras que dividir la longitud por tiempo debería ser legal y resulta en un nuevo tipo - para la velocidad). – etaoin

Lo siento, mis habilidades de programación de tipo de orden superior no son tan buenas. Probablemente recurriré a OO, construiré clases que representen los diversos tipos de cosas que necesitas. – stonemetal

Usted puede ser capaz de utilizar una de las muchas construcciones sorprendentes de Oleg: http://caml.inria.fr/pub/ml-archives/caml-list/2009/07/2984f23799f442d0579faacbf4e6e904.en.html

Jane Street tiene otra sugerencia a través de módulos de primera clase.

http://ocaml.janestreet.com/?q=node/81

exención de responsabilidad: Sobre todo admiro este tipo de programación desde lejos.

Fuente

2011-08-30 17:40:12

Gracias, oigo lo que dices, pero en Haskell todo fue tan fácil con las clases de tipo y lo que no :) Y estos enlaces que publicaste, los he estado viendo todo el tiempo, tratando de obtener la esencia de ello, pero nunca logré doblar esos módulos a mis necesidades. No entiendo las limitaciones de igualdad de tipo que implementan, ¿por qué son tan importantes y cómo usarlas exactamente para lograr funciones de "mayor nivel"? Supongo que los volveré a leer un par de veces más ... – etaoin

Respuesta

Cuestiones relacionadas