List coalgebra translating code from Haskell to SML

Question

I'm trying to translate this piece of code in Haskell that describes List anamorphism but can't quite get it to work.

The final three lines are supposed to generate a function count which given an int will produce an int list [n, n-1, ..., 1]

Haskell code:

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)

What I have so far:

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

I get the following error:

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)

Not sure how to fix this as I am not super proficient in SML.

Answer 1

As you mentioned in the comments, the type parameters got mixed up. With a bit of renaming for comparison:

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

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

which leads to a mismatch after pattern-matching on the pair:

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

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