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

问题描述

可以使用以下多态函数：

  let id x = x ;; 
让compose f g x = f（g x）;; 
让rec修复f = f（修复f）;; （* laziness aside *）
  

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

  type'x id ='x; 
 type'f'g'x compose =（'f（'g'x））;;的构成
 type'f fix =（'f（Fix'f））;; 
  

表示类型，但不起作用。

这里有一个Haskell版本的类型：

  data Id x = Id x 
 data Compose fgx = Compose f（gx））
 data修复f =修复（f（Fix f））
 
  - 例子：
l =撰写[Just'a'] :: Compose []也许Char 
 
类型Natural = Fix也许 - 自然数是Maybe 
n = Fix的固定点（Just（Fix（Just（Fix Nothing））））:: Natural  -  n is 2 
 
  - 同构组合的同一性和f是f：
 iso :: Compose Id fx  - > fx 
 iso（Compose（Id a））= a 
  

解决方案

Haskell允许更高类型的类型变量。 ML方言，包括Caml，只允许类型*的类型变量。翻译成简单的英文，

• 在Haskell中，一个类型变量 g 可以对应类型构造函数，如 Maybe 或 IO 或列表。因此，如果例如 g 是Haskell示例中的 gx ，那么它就是OK（行话：well-kinded） 也许和 x 是整数。




• 在ML中，类型变量'g 只能对应于地面类型，如 int 或 string ，永远不会是像选项或列表。因此，试图将一个类型变量应用到另一个类型是不正确的。

据我所知，这种ML限制没有深刻的理由。最可能的解释是历史偶然性。当米尔纳最初提出他关于多态性的想法时，他使用了非常简单的类型变量，仅仅为类型单变量*。 Haskell的早期版本也做了同样的事情，然后马克琼斯发现推断各种类型变量其实很简单。 Haskell很快被修改为允许更高类型的变量，但ML从未赶上。

INRIA的人对ML做了很多其他修改，而我有点惊讶他们从未做过这件事。当我在ML编程时，我可能会喜欢拥有更高级的类型变量。但他们不在那里，我不知道任何方式来编码你正在谈论的例子，除非使用函子。

Can the following polymorphic functions

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.

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 allows type variables of higher kind. ML dialects, including Caml, allow type variables of kind "*" only. Translated into plain English,

• 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.

• 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.

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.

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屋！