Can clojure inspired transducers be typed with the HM type system?

Question

I have a purely functional transducer implementation in Javascript that supports loop-fusion and short circuiting. Please note that although I am using JS it is not a requirement for understanding the question. Only the types matter.

// ((a -> r) -> r) -> Cont r a
const Cont = k => ({run: k});

// (a -> b -> Cont b b) -> b -> [a] -> b
const foldk = f => init => xs => {
  let acc = init;

  for (let i = xs.length - 1; i >= 0; i--)
    acc = f(xs[i]) (acc).run(id);

  return acc;
};

// (a -> b) -> (b -> t b -> Cont (t b) (t b)) -> a -> t b -> Cont (t b) (t b)
const map = f => cons => x => acc =>
  Cont(k => cons(f(x)) (acc).run(k));

// (a -> Bool) -> (a -> t a -> Cont (t a) (t a)) -> a -> t a -> Cont (t a) (t a)
const filter = p => cons => x => acc =>
  Cont(k =>
    p(x)
      ? cons(x) (acc).run(k)
      : k(acc));

// (b -> c) -> (a -> b) -> a -> c
const comp = f => g => x => f(g(x));

const liftCont2 = f => x => y => Cont(k => k(f(x) (y)));
const unshift = x => xs => (xs.unshift(x), xs);
const includes = sub => s => s.includes(sub);
const len = arrayLike => arrayLike.length;
const id = x => x;

// (String -> t String -> Cont (t String) (t String))
//   -> String -> t String -> Cont (t String) (t String)
const filterO = filter(includes("o"));

// (Number -> t Number -> Cont (t Number) (t Number))
//    -> String -> t Number -> Cont (t Number) (t Number)
const mapLen = map(len);

// type error
const transducer = comp(filterO) (mapLen);

const reducer =  transducer(liftCont2(unshift));

const main = foldk(reducer) ([]) (["f", "fo", "foo", "fooo"]);

console.log(main); // [2, 3, 4] with only a single traversal

As you can see the fold works but doesn't type check. Revealing the type error requires some manual unification:

unify `comp(filterO)`:
(b -> c) -> (a -> b) -> a -> c
(String -> t String -> Cont (t String) (t String))
  -> String -> t String -> Cont (t String) (t String)

yields

(a -> String -> t String -> Cont (t String) (t String))
  -> a -> String -> t<String> -> Cont (t String) (t String)

unify result of `comp(filterO)` with `mapLen` (contravariant):
a -> String -> t String -> Cont (t String) (t String)
(Number -> t Number -> Cont (t Number) (t Number))
  -> String -> t Number -> Cont (t Number) (t Number)

substitutes

a ~ Number -> t Number -> Cont (t Number) (t Number)

unify (covariant):
String -> t String -> Cont (t String) (t String)
String -> t Number -> Cont (t Number) (t Number)

Both terms clearly cannot be unified.

Are transducers a concept exclusive for dynamic languages and cannot be typed, did I make a mistake during unification or are my transducer types (map/filtert) just plain wrong?

Answer 1

Your type signatures for map and filter aren't generic enough.

// map :: (a -> b) -> (b -> t b -> Cont (t b) (t b)) -> a -> t b -> Cont (t b) (t b)
const map = f => cons => x => acc => Cont(k => cons(f(x))(acc).run(k));

// filter :: (a -> Bool) -> (a -> t a -> Cont (t a) (t a)) -> a -> t a -> Cont (t a) (t a)
const filter = p => cons => x => acc => Cont(k => p(x) ? cons(x)(acc).run(k) : k(acc));

The type of acc and the input type of k should be the same, and they should be independent of other types. The return type of k should also be independent of other types.

// type Reducer r a b = a -> b -> Cont r b

// map :: (a -> b) -> Reducer r b c -> Reducer r a c
const map = f => cons => x => acc => Cont(k => cons(f(x))(acc).run(k));

// filter :: (a -> Bool) -> Reducer r a b -> Reducer r a b
const filter = p => cons => x => acc => Cont(k => p(x) ? cons(x)(acc).run(k) : k(acc));

Notice that the type Reducer is just the type of cons converted to continuation-passing style. When using this type, the resulting program type checks as expected.

// data Cont r a = Cont { run :: (a -> r) -> r }
const Cont = run => ({ run });

// type Reducer r a b = a -> b -> Cont r b

// foldk :: Reducer b a b -> b -> [a] -> b
const foldk = f => init => xs => xs.reduceRight((acc, x) => f(x)(acc).run(id), init);

// map :: (a -> b) -> Reducer r b c -> Reducer r a c
const map = f => cons => x => acc => Cont(k => cons(f(x))(acc).run(k));

// filter :: (a -> Bool) -> Reducer r a b -> Reducer r a b
const filter = p => cons => x => acc => Cont(k => p(x) ? cons(x)(acc).run(k) : k(acc));

// comp :: (b -> c) -> (a -> b) -> a -> c
const comp = f => g => x => f(g(x));

// liftCont2 :: (a -> b -> c) -> a -> b -> Cont r c
const liftCont2 = f => x => y => Cont(k => k(f(x)(y)));

// unshift :: a -> [a] -> [a]
const unshift = x => xs => [x, ...xs];

// includes :: String -> String -> Bool
const includes = sub => s => s.includes(sub);

// len :: ArrayLike t => t a -> Number
const len = arrayLike => arrayLike.length;

// id :: a -> a
const id = x => x;

// filterO :: Reducer r String a -> Reducer r String a
const filterO = filter(includes("o"));

// mapLen :: ArrayLike t => Reducer r Number b -> Reducer r (t a) b
const mapLen = map(len);

// transducer :: Reducer r Number a -> Reducer r String a
const transducer = comp(filterO)(mapLen);

// reducer :: Reducer r String [Number]
const reducer = transducer(liftCont2(unshift));

// main :: [Number]
const main = foldk(reducer)([])(["f", "fo", "foo", "fooo"]);

// [2, 3, 4]
console.log(main);

However, it doesn't really make any sense to convert the reducer to CPS. Converting the reducer to CPS doesn't buy you anything because transducers are written in CPS anyway. In fact, in the above program CPS is pointless because the only continuation you're using is id (in the foldk function). If you don't use CPS, then your program becomes much simpler.

// type Reducer a b = a -> b -> b

// foldr :: Reducer a b -> b -> [a] -> b
const foldr = f => init => xs => xs.reduceRight((acc, x) => f(x)(acc), init);

// map :: (a -> b) -> Reducer b c -> Reducer a c
const map = f => cons => x => cons(f(x));

// filter :: (a -> Bool) -> Reducer a b -> Reducer a b
const filter = p => cons => x => p(x) ? cons(x) : id;

// comp :: (b -> c) -> (a -> b) -> a -> c
const comp = f => g => x => f(g(x));

// unshift :: a -> [a] -> [a]
const unshift = x => xs => [x, ...xs];

// includes :: String -> String -> Bool
const includes = sub => s => s.includes(sub);

// len :: ArrayLike t => t a -> Number
const len = arrayLike => arrayLike.length;

// id :: a -> a
const id = x => x;

// filterO :: Reducer String a -> Reducer String a
const filterO = filter(includes("o"));

// mapLen :: ArrayLike t => Reducer Number b -> Reducer (t a) b
const mapLen = map(len);

// transducer :: Reducer Number a -> Reducer String a
const transducer = comp(filterO)(mapLen);

// reducer :: Reducer String [Number]
const reducer = transducer(unshift);

// main :: [Number]
const main = foldr(reducer)([])(["f", "fo", "foo", "fooo"]);

// [2, 3, 4]
console.log(main);

Don't use continuations just for the sake of using continuations. 99% of the time you don't need continuations.