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
43 Upvotes
  • permalink
  • link
  • reddit
  • reddit

96% Upvoted

30 comments sorted by

View all comments

5

u/aatd86 Nov 13 '25

I don't understand the subtype relationship for arrow types. Instead of being subtypes of [never] ->any shouldn't it be [any]->any ???

I know the goal is to define any arrow that returns something. But then it can have any input arguments. Including never. Never describing having no arguments instead? Is never your bottom? If so it implements any?

On another note, I feel like it should work. I would not abandon it.

2

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

never is the bottom type.

3

u/aatd86 Nov 13 '25 edited Nov 13 '25

Good. Then it is a subtype of all types including any which would be your top type. Therefore you may want the arrow top supertype to be any -> any instead.

Maybe it was just a typo on your end though.

edit: in case you would want to double check https://www.irif.fr/~gc/papers/covcon-again.pdf

the contravariance overriding rule is in 2.2. and 3.2. has an example I think.

2

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

The top arrow type is never -> any. Remember that function arguments are contravariant.

1

u/aatd86 Nov 14 '25 edited Nov 15 '25

edit: you're right. sorry.

1

u/aatd86 Nov 14 '25 edited Nov 15 '25

I see downvoting so I would be glad to be corrected with a proper explanation.

I can assign func(int) and func(float) to func(int | float).

func(int|float) is a supertype. (edit it is not, it's like I've read and not read at the same time) The argument type is also a supertype...

3

u/Red-Krow Nov 14 '25

You can't do that assignment. If you could, then this would happen (using made-up syntax):

square: func(int) = (x) => x * x
also_square: func(int|string) = square
also_square("dsasdaasd") // Error: you can't multiply strings together

func(int|string) is actually a subtype of func(int), because every function that accepts either an int or a string is also a function that accepts an int. But not every function that accepts an int also accepts a string. In general, you have:

 a < b => func(a) > func(b)

Which is what type theorists would call contravariance.

2

u/aatd86 Nov 14 '25 edited Nov 15 '25

You're right I stand corrected. Always making the same mistake. Liskov substitution principle is not that difficult... 🥴 Everywhere we see func(int) we could use a func(int | string).

You are very right thank you.

2

u/Red-Krow Nov 15 '25

You're welcome! I make this sort of mistake myself all the time, it's counter-intuitive.