可以使用 HM 类型系统键入受 Clojure 启发的传感器吗？

Posted 2023-05-08

【中文标题】可以使用 HM 类型系统键入受 Clojure 启发的传感器吗？

【英文标题】：Can clojure inspired transducers be typed with the HM type system?

【发布时间】：2021-10-05 08:23:24

【问题描述】：

我有一个纯功能的 javascript 转换器实现，支持循环融合和短路。请注意，虽然我使用的是 JS，但这并不是理解问题的必要条件。只有类型很重要。

// ((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

正如您所见，折叠有效，但不进行类型检查。揭示类型错误需要一些手动统一：

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)

这两个术语显然不能统一。

转换器是动态语言独有的概念并且无法键入，是我在统一过程中犯了错误还是我的转换器类型 (map/filtert) 完全错误？

【问题讨论】：

"我刚刚找到了我的问题的答案，但既不能撤销赏金也不能删除让我处于尴尬境地的问题。" 你可以自己回答.另一种选择是等待赏金到期然后关闭。或者也许有人同时回答。

我们更喜欢不包含赏金/投票/元评论的问题 - 理想情况下，它们应该尽可能保持对未来读者有用的状态。大多数读者并不关心超材料，因此最好将其排除在外。

【参考方案1】：

map 和 filter 的类型签名不够通用。

// 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));

acc 的类型和k 的输入类型应该相同，并且应该独立于其他类型。 k 的返回类型也应该独立于其他类型。

// 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));

请注意，Reducer 类型只是 cons 转换为延续传递样式的类型。使用此类型时，生成的程序类型会按预期进行检查。

// 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);

但是，将reducer 转换为CPS 并没有任何意义。将减速器转换为 CPS 不会给您带来任何好处，因为传感器无论如何都是用 CPS 编写的。事实上，在上述程序中，CPS 毫无意义，因为您使用的唯一延续是 id（在 foldk 函数中）。如果你不使用 CPS，那么你的程序就会变得简单得多。

// 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);

不要仅仅为了使用延续而使用延续。 99% 的时间不需要继续。

【讨论】：

我最终得到了以下更高级别的类型type Transducer a b = forall c. (a -> c -> c) -> b -> c -> c（用于非连续版本），但显然它在没有更高级别的情况下也可以工作。

你将如何有效地实现take 没有延续？顺便说一句，我的foldk 是错误的，b/c 它所基于的循环具有运行到完成语义。我目前正在实现一个堆栈安全的右关联版本，因此需要它自己的堆栈结构。

哦，我明白了，你的实现是 rank-1，b/c 你输入了减速器，而不是传感器。