实现和表示polyadic操作

Ytt*_*ill 5 ocaml

我不确定我是否知道如何提出这个问题.在实现编译器时,我想允许客户端指定,例如,在元组上折叠.我提供了一种方法来curry和uncurry一个函数,但这只是因为我在Ocaml中编写了一个二元运算符并将其折叠在术语和类型表示上.用户无法编写此功能.

在宏处理器中,用户可以编写此函数,因为元组是列表.

对于curried函数,用户可以轻松编写变换器,因为该术语在目标语言和术语的Ocaml表示以及键入时都是二进制的.

但他们不能为元组做这件事.这是另一个例子:用户可以轻松定义串行功能组合运算符.但用户无法定义并行组合:二进制版本:

 f1: D1 -> C1, f2: D2-> C2 --> f1 * f2: D1 * D2 -> C1 * C2
Run Code Online (Sandbox Code Playgroud)

很容易写,但不能扩展到3个术语:这里折叠会计算

 f1 * (f2 * f3)
Run Code Online (Sandbox Code Playgroud)

代替

f1 * f2 * f3
Run Code Online (Sandbox Code Playgroud)

[同构但不相等]

这个问题的概括是"我如何实现一种多语言编程语言",这里有点太多了.我试图做的是提供内置变压器:

咖喱:T1*T2*T3 ...... - > T1 - > T2 - > ......不发生:T1 - > T2 - > .. T1*T2*T3

那么用户可以用二元运算符进行折叠:

uncurry (fold user_op (uncurry term))
Run Code Online (Sandbox Code Playgroud)

但这既不够通用,也不是很好.. :)

我想Haskell的一个等价问题是:由于Haskell没有n-ary产品,n-ary元组构造函数在库中用n个函数模拟,其中每个函数必须手工写出.这显然很糟糕.这将如何解决?

[我的意思是,编写一个Python脚本来生成那些n个函数达到某个极限n是微不足道的,那么为什么在语言中以一种好的方式这么做呢?]

Mic*_*and 2

有两个组件共同导致此问题:

  • 元组不会自动展平 - 类型表达式中的括号不仅仅是分组,它们创建由更多元组连接的不同类型。这导致您的观察结果a * (b * c)同构但不等价于a * b * c
  • 类型系统不提供表达元组类型代数的方法。我的意思是,类型系统没有 cons 运算符或元组的任何等效运算符;无法表示一种类型比另一种类型具有更多或更少的元组元素。

结果是无法表达对任意长度的元组进行操作的函数的类型。

因此,简短的总结是 OCaml 类型系统缺乏表达您要编写的函数类型的机制,因此您无法编写该函数(抛开令人讨厌的游戏Obj; 您可以编写该函数,但您不能表达其类型以以类型安全的方式使用它)。

  • 是的,但这不是我的问题:我不是在问 Ocaml 的类型系统是做什么的,我是在问如何用另一种语言实现它(实际上是我的语言 Felix,其编译器是用 Ocaml 编写的)。 (2认同)