列出从 Haskell 到 SML 的 colgebra 转换代码答案

【问题标题】：List coalgebra translating code from Haskell to SML列出从 Haskell 到 SML 的 colgebra 转换代码
【发布时间】：2020-08-23 02:39:29
【问题描述】：

我正在尝试在 Haskell 中翻译这段描述 List anamorphism 但无法完全正常工作的代码。

最后三行应该生成一个函数 count 给定一个 int 将生成一个 int 列表 [n, n-1, ..., 1]

Haskell 代码：

data Either a b = Left a | Right b

type List_coalg u x = u -> Either () (x, u)

list ana :: List_coalg u x -> u -> [x]
list_ana a = ana where
  ana u = case a u of 
    Left _ -> []
    Right (x, l) -> x : ana l

count = list_ana destruct_count
destruct_count 0 = Left ()
destruct_count n = Right (n, n-1)

到目前为止我所拥有的：

type ('a, 'b) List_coalg = 'a -> (unit, 'a*'b) Either

fun list_ana (f : ('a, 'b) List_coalg) : 'a -> 'b list = 
  let
    fun ana a : 'b list = 
      case f a of
        Left () => []
      | Right (x, l) => x :: ana l
  in
    ana
  end

fun destruct_count 0 = Left ()
  | destruct_count n = Right (n, n-1)

val count = list_ana destruct_count

我收到以下错误：

catamorphism.sml:22.7-24.35 Error: case object and rules do not agree [UBOUND match]
  rule domain: (unit,'b * 'a) Either
  object: (unit,'a * 'b) Either
  in expression:
    (case (f a)
      of Left () => nil
       | Right (x,l) => x :: ana l)

不知道如何解决这个问题，因为我对 SML 不是很精通。

【问题讨论】：

我通过简单地将行 type ('a, 'b) List_coalg = 'a -> (unit, 'a*'b) Either 更改为 type ('a, 'b) List_coalg = 'a -> (unit, 'b*'a) Either 来修复错误，但我不确定它为什么有效？我试图从一篇论文中理解这一点，但我通常不确定这种类型行是如何工作的
我的意思是，Haskell 版本有type List_coalg u x = u -> Either () (x, u) - 显然元组中的类型参数与类型声明的类型参数的顺序相反。因此，如果您希望类型以相同的方式排列，则需要在 ML 中执行相同的操作。
@amalloy 颠倒参数顺序有什么意义？我不太明白
在这种情况下，我认为颠倒这些论点没有意义。通常，当您想要部分应用类型构造函数时会这样做，例如定义一个仿函数实例，但这里不需要。（尽管从技术上讲，对于某个函子 F，余代数是 u->F u。但我们在这里不需要知道这一点。）

标签： haskell functional-programming sml category-theory unfold

【解决方案1】：

正如您在 cmets 中提到的，类型参数混淆了。稍微重命名以进行比较：

type List_coalg a b = a -> Either () (b, a)            --  (b, a)

type ('a, 'b) List_coalg = 'a -> (unit, 'a*'b) Either  (*  ('a * 'b)  *)

这会导致在该对上进行模式匹配后不匹配：

    Right (x, l) -> x : ana l
    -- x :: b
    -- l :: a

    Right (x, l) => x :: ana l
    (* x : 'a *)
    (* l : 'b *)

【讨论】：