scala - 关于点菜数据类型的问题

Question

我正在阅读 the original paper about data types a la carte并决定尝试在 Scala 中实现这个想法(我知道它已经在许多函数库中实现了)。不幸的是，我发现原始论文很难理解，而且我一开始就卡在了某个地方。然后我找到了another paper这更容易理解，我设法将论文中的 Haskell 代码重写为 Scala，你可以找到它 here .但是，我仍然难以理解片刻:

引用第二篇论文

原创 Expr数据类型

data Expr = Val Int | Add Expr Expr

新类型签名:

data Arith e = Val Int | Add e e

For any functor f, its induced recursive datatype, Fix f, is defined as the least fixpoint of f, implemented as follows:

data Fix f = In (f (Fix f))

Now that we have tied the recursive knot of a signature, Fix Arith is a language equivalent to the original Expr datatype which allowed integer values and addition.

“我们已经绑定(bind)了签名的递归结”到底是什么意思？它是什么意思 Fix Arith是一种等同于原始 Expr 的语言?
In 的实际类型是 In :: f (Fix f) -> Fix f如果我们尝试使用 In 构造一个值构造和 Val 1变量我们将得到以下结果:

> :t  In(Val 1)
> In(Val 1) :: Fix Arith

相同数据类型的 Scala 编码:

  sealed trait Arith[A]
  case class Val[A](x: Int) extends Arith[A]
  case class Add[A](a: A, b: A) extends Arith[A]

  trait Fix[F[_]]
  case class In[F[_]](exp: F[Fix[F]]) extends Fix[F]

fold功能fold函数具有以下签名和实现

haskell :

fold :: Functor f => (f a -> a) -> Fix f -> a
fold f (In t) = f (fmap (fold f) t)

我想出的Scala变体

  def fold[F[_] : Functor, A](f: F[A] => A): Fix[F] => A = {
    case In(t) =>
      val g: F[Fix[F]] => F[A] = implicitly[Functor[F]].lift(fold(f))
      f(g(t))
  }

我很好奇的是，在我的 Scala 版本函数中 g具有以下类型 F[Fix[F]] => F[A]但是变量的类型 t模式匹配后是 LaCarte$Add有值 Add(In(Val(1)),In(Val(2))) ，如何应用函数 g 是有效的至 LaCarte$Add ?另外，如果您能帮助我理解 fold，我将不胜感激。功能 ？

引用论文:

The first argument of fold is an f-algebra, which provides the behavior of each constructor associated with a given signature f.

Answer 1

What does it mean exactly “we have tied the ‘recursive knot’ of a signature”?

原文 Expr数据类型是递归的，在它自己的定义中引用它自己:

data Expr = Val Int | Add Expr Expr

Arith通过用参数替换递归调用，键入“分解”递归:

data Arith e = Val Int | Add e e

原文 Expr type 可以有任意深度的嵌套，我们希望通过 Arith 来支持。也是，但最大深度取决于我们为 e 选择的类型:

Arith Void不能嵌套:它只能是文字值(Val n)，因为我们不能构造 Add ，因为我们无法获得 Void 类型的值(它没有构造函数)

Arith (Arith Void)可以有一层嵌套:外部构造函数可以是 Add , 但内部构造函数只能是 Lit .

Arith (Arith (Arith Void))可以有两个级别

等等

什么 Fix Arith给我们的是一种谈论不动点的方法 Arith (Arith (Arith …))深度没有限制。

这就像我们如何用非递归函数替换递归函数并使用定点组合器恢复递归:

factorial' :: (Integer -> Integer) -> Integer -> Integer
factorial' recur n = if n <= 1 then 1 else n * recur (n - 1)

factorial :: Integer -> Integer
factorial = fix factorial'

factorial 5 == 120

What does it mean Fix Arith is a language equivalent to the original Expr?

Fix Arith 的语言(语法)表示相当于 Expr 的语言代表;也就是说，它们是同构的:您可以编写一对总函数 Fix Arith -> Expr和 Expr -> Fix Arith .

How it happens that it’s valid to apply function g to LaCarte$Add?

我对 Scala 不是很熟悉，但它看起来像 Add是 Arith 的子类型，所以 g的参数类型 F[Fix[F]]可以用 Arith[Fix[Arith]] 类型的值填充您可以通过匹配 In构造函数来“展开”一层递归。