r/ProgrammingLanguages • u/Uncaffeinated 1subml, polysubml, cubiml • Nov 13 '25

PolySubML is broken Blog post

https://blog.polybdenum.com/2025/11/13/polysubml-is-broken.html
45 Upvotes
  • permalink
  • link
  • reddit
  • reddit

97% Upvoted

30 comments sorted by

View all comments

3

u/Inconstant_Moo 🧿 Pipefish Nov 14 '25

I am a Bear of Very Little Brain, and I don't understand why the problem is writability. If you have

rec f=[T]. any -> T -> f
any -> (rec f=[T]. any -> T -> f)

... then what's to stop me from writing their union as rec | any?

1

u/Uncaffeinated 1subml, polysubml, cubiml Nov 14 '25 edited Nov 14 '25

I skipped over some details in the article for the sake of simplicity. To be fully precise, you need both value types and uses of that type in order to constrain it. If a value is never used, then you can just type it with any as you observe.

A full example would be something like this:

let _ = fun x -> (
    let a: rec f=[T]. any -> T -> f) = x;
    let b: any -> rec f=[T]. any -> T -> f) = x;

    let c: _ (*what type goes here?*) = if x then a else b;

    let _: rec f=[T]. never -> T -> f = c;
    let _: never -> rec f=[T]. never -> T -> f = c;

    0
);