OCaml 中的 FIx 数据类型

Question

以下来自 Haskell 的数据类型如何用 OCaml 或 SML 表示？

newtype Fix f = In (f (Fix f))

Answer 1

我已经answered this question on the mailing-list （我必须说我有点不高兴你在两个不同的地方问这个问题而没有几天的延迟，因为它可能会引起重复工作），但让我们重现它在这里。

这里有一个困难，因为 OCaml 不支持更高级别的 类型变量。在此声明中，f 不是“类型”，而是“类型” 运算符”（种类 * -> *）。要在 OCaml 中执行相同操作，您可以使用 函子（不是 Haskell 函子；在 OCaml 中，“函子”一词表示 可能依赖于其他模块/函子的高阶模块）； 函子是更高种类的。

module type ParamType = sig
  type ('a, 'b) t
end

module Fix (M : ParamType) = struct
  type 'b fix = In of ('b fix, 'b) M.t
end

module List = struct
  module Param = struct
    type ('a, 'b) t = Nil | Cons of 'b * 'a
  end
  include Fix(Param)
end

open List.Param
open List

let rec to_usual_list =
  function
  | In Nil -> []
  | In (Cons (x, xs)) -> x :: to_usual_list xs

好消息是 OCaml 还支持等递归而不是 iso-recursive 类型，它允许您在以下位置删除“In”包装器 每个递归层。为此，您必须编译现有模块 （以及所有通过 接口）与“-rectypes”选项。然后你可以写：

module type ParamType = sig
  type ('a, 'b) t
end

module EqFix (M : ParamType) = struct
  type 'b fix = ('b fix, 'b) M.t
end

module EqList = struct
  module Param = struct
    type ('a, 'b) t = Nil | Cons of 'b * 'a
  end
  include EqFix(Param)
end

open EqList.Param

let rec to_usual_list =
  function
  | Nil -> []
  | (Cons (x, xs)) -> x :: to_usual_list xs

模块的语法很繁重，看起来很吓人。如果 你坚持你可以使用一流的模块来移动其中一些用途 从函子到简单的函数。我选择从“简单”开始 方法是先做。

高级变量嫉妒可能是最严重的疾病 OCaml 类型的崇拜者（或出于某些（好！）原因的 Haskellers） 来功能县的这些地方闲逛）。在实践中我们做 没有它没有太多问题，但大量使用 monad 这个函子步骤确实会使变压器变得复杂， 这是它在这里不是很流行的风格的原因之一。 你也可以通过思考不完美来分散自己的注意力 支持它们的语言中的高级变量；这 对构造函数多态性的限制，而不是任意的 类型级函数使它们的表现力不如您想要的那样。 那天我们制定出绝对完美的高阶细节 类型抽象，也许OCaml会跳转到它？

Answer 2

我不认为 OCaml 允许您对类型构造函数进行抽象。我认为，对于 Fix 的特定应用，您可以使用 -rectypes 获得类似的效果。

$ ghci
GHCi, version 7.4.2: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> newtype Fix f = In (f (Fix f))
Prelude> type L = Fix []
Prelude> let w = In [] :: L
Prelude> let x = In [x] :: L

$ ocaml -rectypes
        OCaml version 4.00.0

# type l = l list;;
type l = l list
# ([] : l);;
- : l = []
# let rec x = [x];;
val x : 'a list as 'a = [[[...]]]
# (x : l);;
- : l = [[[...]]]

我不是模块类型专家。可能有一种方法可以使用模块来比这更接近。使用模块系统似乎一切皆有可能。