Конструкторы типа высшего порядка и функторы в OCaml

Question

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

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 

Answer 1

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

• В Haskell, тип переменной g может соответствовать «типа конструктора», как Maybe или IO или списки. Таким образом, g x в вашем примере Haskell будет в порядке (жаргон: «доброжелательный»), если, например, g - Maybe и x - Integer.

• В ML, тип переменной 'g может соответствовать только «основного типа» как int или string, никогда к типу конструктора, как option или list. Поэтому никогда не правильно применить переменную типа к другому типу.

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

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

Answer 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 

Answer 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);; 

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

Answer 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)