Я уже давно пишу подключаемый модуль проверки типов во время выполнения для Javascript.

Я уже давно пишу подключаемый модуль проверки типов во время выполнения для Javascript. Я использую кодировку Скотта и (неявные) типы ранга 2 для выражения безопасных типов ADT в Javascript. Вот небольшой набросок рекурсивного типа List, который вы упомянули в своем посте:

import * as F from ".../ftor.js";
F.type(true);
const List = F.Adt(
  function List() {},
  "(List :: ({Cons: (a -> List<a> -> r), Nil: r} -> r) -> List<a>)"
);
const Nil = List(cases => cases.Nil);
const Cons = x => tx => List(cases => cases.Cons(x) (tx));
const uncons = F.Fun(
  "(uncons :: {Cons: (a -> List<a> -> r), Nil: r} -> List<a> -> r)",
  cases => tx => tx.run(cases)
);
const empty = uncons(
  F.Rec({
    Nil: true, Cons: F.Fun("(a -> List<a> -> Boolean)",
    x => tx => false)
  })
);
const xs = Cons("foo") (Nil),
  ys = Nil;
empty(xs); // false
empty(ys); // true
const brokenEmpty = uncons(
  F.Rec({
    Foo: true, Cons: F.Fun("(a -> List<a> -> Boolean)",
    x => tx => false)
  })
); // type error (missing Nil case)

Как видите, средство проверки типов строго оценивает типы функций и, следовательно, немедленно выдает ошибку типа.

Следует признать, что сигнатуры типов для ADT, закодированных Скоттом, немного пугают. Однако на самом деле они очень похожи для разных АТД.

Вот репо, если вы заинтересованы.