Конструкторы и функторы более высокого порядка в Ocaml

Могут ли следующие полиморфные функции

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

записывается для типов/типов конструкторов или модулей/функторов? Я попробовал

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

для типов, но он не работает.

Здесь версия 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

Ответы

Ответ 1

Haskell позволяет использовать переменные типа более высокого типа. ML-диалекты, включая Caml, допускают только переменные типа "*". Перевод на простой английский,

В Haskell переменная типа g может соответствовать "конструктору типа", подобному Maybe или IO или спискам. Таким образом, g x в вашем примере Haskell будет в порядке (жаргон: "доброжелательный" ), если, например, g есть Maybe и x is Integer.
В ML переменная типа 'g может соответствовать только "наземному типу", подобному int или string, никогда к конструктору типа, подобному option или list. Поэтому никогда не следует пытаться применить переменную типа к другому типу.

Насколько мне известно, нет серьезной причины этого ограничения в ML. Наиболее вероятным объяснением является историческая непредвиденная ситуация. Когда Мильнер изначально придумывал свои идеи о полиморфизме, он работал с очень простыми переменными типа, стоящими только для монотипов рода *. Ранние версии Haskell делали то же самое, а затем в какой-то момент Марк Джонс обнаружил, что определение типов переменных типа на самом деле довольно просто. Haskell был быстро пересмотрен, чтобы позволить переменным типа более высокого уровня, но ML никогда не догонял.

Люди из INRIA внесли много других изменений в ML, и я немного удивлен, что они никогда не делали этого. Когда я программирую в ML, мне могут нравиться переменные типа более высокого типа. Но их там нет, и я не знаю, как кодировать примеры, о которых вы говорите, кроме как с помощью functors.

Ответ 2

Вы можете сделать что-то подобное в OCaml, используя вместо модулей типы вместо типов и функторы (модули более высокого порядка) вместо типов более высокого порядка. Но он выглядит намного уродливее, и он не обладает способностью ввода-вывода, поэтому вам нужно вручную указать много вещей.

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

Ответ 3

Ну... Я не эксперт по типам более высокого порядка и программирования Haskell. Но это похоже на F # (это OCaml), вы могли бы работать с ними:

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

Последний, который я завернул в кортеж, так как я не придумал ничего лучшего...

Ответ 4

Вы можете сделать это, но вам нужно сделать несколько трюков:

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

После этого вы можете определить Cata:

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

Это определит общий катаморфизм для всех функторов, который вы можете использовать для создания собственных вещей. Пример:

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)