de orden superior constructores de tipos y funtores en Ocaml

Question

¿Pueden las siguientes funciones polimórficas

let id x = x;; 
let compose f g x = f (g x);; 
let rec fix f = f (fix f);;  (*laziness aside*) 

ser escritos para tipos/constructores de tipos o módulos/funtores? Intenté

type 'x id = Id of 'x;; 
type 'f 'g 'x compose = Compose of ('f ('g 'x));; 
type 'f fix = Fix of ('f (Fix 'f));; 

para los tipos, pero no funciona.

Aquí hay una versión para este tipo de Haskell:

data Id x = Id x 
data Compose f g x = Compose (f (g x)) 
data Fix f = Fix (f (Fix f)) 

-- examples: 
l = Compose [Just 'a'] :: Compose [] Maybe Char 

type Natural = Fix Maybe -- natural numbers are fixpoint of Maybe 
n = Fix (Just (Fix (Just (Fix Nothing)))) :: Natural -- n is 2 

-- up to isomorphism composition of identity and f is f: 
iso :: Compose Id f x -> f x 
iso (Compose (Id a)) = a 

Answer 1

Haskell permite escribir variables de tipo superior. Los dialectos ML, incluido Caml, solo permiten variables de tipo del tipo "*". Traducido en la llanura Inglés,

• En Haskell, un tipo de variable g puede corresponder a un "constructor de tipo" como Maybe o IO o listas. Por lo tanto, g x en su ejemplo de Haskell estaría bien (jerga: "bien emparejado") si, por ejemplo, g es Maybe y x es Integer.

• En ML, un tipo de variable 'g sólo puede corresponder a un "tipo de tierra" como int o string, no a un constructor de tipos como option o list. Por lo tanto, es nunca correcto para tratar de aplicar una variable de tipo a otro tipo.

Por lo que yo sé, no hay una razón profunda para esta limitación en ML. La explicación más probable es la contingencia histórica. Cuando Milner originalmente se le ocurrió su idea sobre el polimorfismo, trabajó con variables de tipo muy simples que se limitaban a los monotipos de tipo *. Las primeras versiones de Haskell hicieron lo mismo, y luego, en algún momento, Mark Jones descubrió que inferir los tipos de variables de tipo es en realidad bastante fácil. Haskell fue rápidamente revisado para permitir variables de tipo de mayor calidad, pero ML nunca se ha puesto al día.

La gente de INRIA ha realizado muchos otros cambios en ML, y estoy un poco sorprendido de que nunca hayan hecho este. Cuando estoy programando en ML, podría disfrutar de tener variables de tipo de mayor kínder. Pero no están allí, y no conozco ninguna forma de codificar el tipo de ejemplos de los que está hablando excepto mediante el uso de functors.

Answer 2

Puede hacer algo similar en OCaml, utilizando módulos en lugar de tipos, y funtores (módulos de orden superior) en lugar de tipos de orden superior. Pero parece mucho más feo y no tiene capacidad de inferencia de tipos, por lo que debe especificar manualmente muchas cosas.

module type Type = sig 
    type t 
end 

module Char = struct 
    type t = char 
end 

module List (X:Type) = struct 
    type t = X.t list 
end 

module Maybe (X:Type) = struct 
    type t = X.t option 
end 

(* In the following, I decided to omit the redundant 
    single constructors "Id of ...", "Compose of ...", since 
    they don't help in OCaml since we can't use inference *) 

module Id (X:Type) = X 

module Compose 
    (F:functor(Z:Type)->Type) 
    (G:functor(Y:Type)->Type) 
    (X:Type) = F(G(X)) 

let l : Compose(List)(Maybe)(Char).t = [Some 'a'] 

module Example2 (F:functor(Y:Type)->Type) (X:Type) = struct 
    (* unlike types, "free" module variables are not allowed, 
    so we have to put it inside another functor in order 
    to scope F and X *) 
    let iso (a:Compose(Id)(F)(X).t) : F(X).t = a 
end 

Answer 3

Bueno ... No soy un experto en los tipos de orden superior ni en la programación de Haskell. pero esto parece estar bien para F # (que es OCaml), se puede trabajar con ellos:

type 'x id = Id of 'x;; 
type 'f fix = Fix of ('f fix -> 'f);; 
type ('f,'g,'x) compose = Compose of ('f ->'g -> 'x);; 

El último que envolvió a tupla ya que no ocurre nada mejor ...

Answer 4

Puede hacerlo pero hay que hacer un poco de un truco:

newtype Fix f = In{out:: f (Fix f)} 

Puede definir Cata después:

Cata :: (Functor f) => (f a -> a) -> Fix f -> a 
Cata f = f.(fmap (cata f)).out 

que definirá una catamorphism genérico para todas las palabras funcionales, los cuales puedes usarlo para construir tus propias cosas. Ejemplo:

data ListFix a b = Nil | Cons a b 
data List a = Fix (ListFix a) 
instance functor (ListFix a) where 
fmap f Nil = Nil 
fmap f (Cons a lst) = Cons a (f lst)