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在你的哈斯克尔例子是OK(行话:"很好kinded"),举例来说,如果g是Maybe和x是Integer.

• 在ML,一个类型变量'g可以仅对应于"接地类型"喜欢int或string,从未类型构造像option或list.因此,尝试将类型变量应用于另一种类型永远不正确.

据我所知,ML的这种限制没有深刻的理由.最可能的解释是历史偶然性.当米尔纳最初提出他关于多态性的观点时,他使用了非常简单的类型变量,只代表了类型的单型*.早期版本的Haskell也做了同样的事情,然后在某些时候,Mark Jones发现推断类型变量的种类实际上非常容易.Haskell很快被修改为允许更高类型的变量,但ML从未赶上.

INRIA的人们对ML做了很多其他的改变,我有点惊讶他们从来没有做过这个.当我用ML编程时,我可能喜欢使用更高级的变量.但它们不在那里,除了使用仿函数之外,我不知道如何编码你正在谈论的那种例子.

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