Ocaml 中的高阶类型构造函数和函子 [英] Higher-order type constructors and functors in Ocaml

问题描述

可以下面的多态函数

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

是为类型/类型构造函数还是模块/函子编写的?我试过了

be written for types/type constructors or modules/functors? I tried

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

对于类型，但它不起作用.

for types but it doesn't work.

这是一个 Haskell 版本的类型:

Here's a Haskell version for types:

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

推荐答案

Haskell 允许更高级的类型变量.ML 方言，包括 Caml，仅允许类型为*"的类型变量.翻译成简单的英语，

Haskell allows type variables of higher kind. ML dialects, including Caml, allow type variables of kind "*" only. Translated into plain English,

• 在 Haskell 中，类型变量 g 可以对应于类型构造函数"，如 Maybe 或 IO 或列表.因此，如果例如 g 是 Maybe 和 x 是 Integer.

• In Haskell, a type variable g can correspond to a "type constructor" like Maybe or IO or lists. So the g x in your Haskell example would be OK (jargon: "well-kinded") if for example g is Maybe and x is Integer.

在 ML 中，类型变量 'g 只能对应于基础类型"，例如 int 或 string，从不到像 option 或 list 这样的类型构造函数.因此，尝试将类型变量应用于另一种类型永远是不正确的.

In ML, a type variable 'g can correspond only to a "ground type" like int or string, never to a type constructor like option or list. It is therefore never correct to try to apply a type variable to another type.

据我所知，ML 中的这种限制没有深层原因.最可能的解释是历史偶然性.当米尔纳最初提出他关于多态的想法时，他使用非常简单的类型变量，这些变量仅代表种类 * 的单类型.早期版本的 Haskell 也是这样做的，然后在某个时候 Mark Jones 发现推断类型变量的种类实际上非常容易.Haskell 很快被修改以允许更高种类的类型变量，但 ML 始终没有赶上.

As far as I'm aware, there's no deep reason for this limitation in ML. The most likely explanation is historical contingency. When Milner originally came up with his ideas about polymorphism, he worked with very simple type variables standing only for monotypes of kind *. Early versions of Haskell did the same, and then at some point Mark Jones discovered that inferring the kinds of type variables is actually quite easy. Haskell was quickly revised to allow type variables of higher kind, but ML has never caught up.

INRIA 的人对机器学习做了很多其他的改变，我有点惊讶他们从来没有做过这个.当我在 ML 中编程时，我可能喜欢拥有更高级的类型变量.但是它们不在那里，我不知道有什么方法可以对您正在谈论的示例进行编码，除非使用 函子.

The people at INRIA have made a lot of other changes to ML, and I'm a bit surprised they've never made this one. When I'm programming in ML, I might enjoy having higher-kinded type variables. But they aren't there, and I don't know any way to encode the kind of examples you are talking about except by using functors.

这篇关于Ocaml 中的高阶类型构造函数和函子的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！