Перечислить коалгебру, переводящую код из Haskell в SML - PullRequest
0 голосов
/ 07 мая 2020

Я пытаюсь перевести этот фрагмент кода в Haskell, который описывает анаморфизм списка, но не могу заставить его работать.

Предполагается, что последние три строки генерируют количество функций, которое 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.

1 Ответ

0 голосов
/ 07 мая 2020

Как вы упомянули в комментариях, параметры типа перепутались. С небольшим переименованием для сравнения:

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 *)
...