Sunday 1 August 2021

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

I just found an answer to my question but can neither revoke the bounty nor delete the question which leaves me in a sort of awkward position.

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?



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

No comments:

Post a Comment