Constructores y funtores de tipo de orden superior en Ocaml


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 escrito para tipos / constructores de tipos o módulos / funtores? He intentado

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 tipos pero no funciona.

Aquí hay una versión de Haskell para los tipos:

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
Author: sdcvvc, 2009-12-31

4 answers

Haskell permite variables de tipo superior. Los dialectos ML, incluyendo Caml, solo permiten variables de tipo"*". Traducido al inglés,

  • En Haskell, una variable de tipo g puede corresponder a un "constructor de tipo" como Maybe o IO o listas. Así que el g x en tu ejemplo de Haskell estaría bien (jerga: "bien kinded") si por ejemplo g es Maybe y x es Integer.

  • En ML, una variable de tipo 'g solo puede corresponder a una " tierra escriba " como int o string, nunca a un constructor de tipo como option o list. Por lo tanto, nunca es correcto intentar aplicar una variable de tipo a otro tipo.

Por lo que 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ó sus ideas sobre el polimorfismo, trabajó con variables de tipo muy simples de pie solo para monotipos de tipo *. Primeras versiones de Haskell hizo 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 revisado rápidamente para permitir variables de tipo de tipo superior, pero ML nunca ha alcanzado.

La gente de INRIA ha hecho 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 kinded. Pero no están allí, y no se ninguna manera de codificar el tipo de ejemplos de los que estás hablando excepto usando funtores.

 30
Author: Norman Ramsey,
Warning: date(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/agent_stack/data/www/ajaxhispano.com/template/agent.layouts/content.php on line 61
2011-11-01 03:47:11

Puede hacer algo similar en OCaml, usando módulos en lugar de tipos, y funtores (módulos de orden superior) en lugar de tipos de orden superior. Pero se ve mucho más feo y no tiene la capacidad de inferencia de tipo, por lo que tiene que especificar manualmente un montón de 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
 19
Author: newacct,
Warning: date(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/agent_stack/data/www/ajaxhispano.com/template/agent.layouts/content.php on line 61
2010-03-18 04:56:50

Bueno... No soy un experto en tipos de orden superior ni en la programación de Haskell. Pero esto parece estar bien para F# (que es OCaml), podrías trabajar con estos:

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 lo envolví en tupla ya que no se me ocurrió nada mejor...

 0
Author: Tuomas Hietanen,
Warning: date(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/agent_stack/data/www/ajaxhispano.com/template/agent.layouts/content.php on line 61
2011-06-02 11:17:35

Puedes hacerlo pero necesitas hacer un pequeño 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

Eso definirá un catamorfismo genérico para todos los funtores, que puedes usar 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)
 -1
Author: Bruno Figares,
Warning: date(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/agent_stack/data/www/ajaxhispano.com/template/agent.layouts/content.php on line 61
2017-02-11 07:52:27