Subtype Inference by Example

https://blog.polybdenum.com/2020/07/04/subtype-inference-by-example-part-1-introducing-cubiml.html

27•azhenley•8mo ago

Comments

juancn•7mo ago

  ...but traditional static type systems require large amounts of manual annotation by programmers, making them difficult to work with...

I like to have type annotations, yeah, they can look ugly, but I much rather know what something is rather than have to infer it by myself.

Makes reading code a lot easier if you know what you're doing.

jjice•7mo ago

FWIW, I've seen many IDEs and plugins add inline type annotations so it reads as though they are there, but aren't. I think the first time I saw this was with the JetBrains IntelliJ Rust plugin in 2019.

layla5alive•7mo ago

I like being able to read code in nano or vi

exac•7mo ago

I would rather see the type annotations too. This whole essay has a flimsy premise.

mrkeen•7mo ago

Around every integer? Around every expression? On every let-bound function, on every where-bound function? Should the 'forall. a' included if 'a' is a polytype?

juancn•7mo ago

It depends on the aesthetics of the language I think. What are core concepts that you must know? (there should be few). Striking the right balance is hard.

Code is read a lot more than is written in my experience, so saving time writing it is optimizing for the wrong thing.

Languages with much inference for me REQUIRE IDEs that help you see what the code is actually doing. Forget about using a text editor or reading a diff and getting what the implications are.

afiori•7mo ago

It would be nice to have them auto-generated in the source, like a autofixable lint rule where the compiler add the annotations to your source code.

abeppu•7mo ago

I'm dimly aware that the Hindley-Milner system is closely related to System F and that System F has many notable exceptions on of the most significant of which is System F<: (System F-sub), which I thought was the subject of a number of inference papers in the 80s and 90s.

What's the difference between that work decades ago and the work from Stephen Dolan in 2016 cited in this post? Like, what's the thing that is demonstrated now that we didn't have like 30 years ago?

https://en.wikipedia.org/wiki/System_F#System_F%3C:

wittystick•7mo ago

Briefly, algebraic data types add polarity to the types so that we don't have both S <= T and T <= S, which would imply equality. Instead we have S+ <= T- and T+ <= S-. The positive types represent a value source and the negative types are a sink. For example, in a function call, the args are negative and the return type is positive. Inside the function its formal parameters become positive and its return type is negative. Variables exist in an "ambipolar" state which can be both the source or the sink, depending on whether we're using it on the rhs or lhs of an assignment.

tomp•7mo ago

I recommend anyone interested in this to check the work of Lionel Parreaux, in particular SimpleSub, which is equivalent to MLsub but substantially simpler.

As it turns out, Dolan's main contribution wasn't the algorithm (which is overly complex, as proven by Parreaux's simpler implementation), but the type language - the insight that most subtyping constraints can be removed and/or simplified to simple union and intersection types, assuming certain simplifications of the type system (namely: positive/negative types, and distributivity of union/intersection over function types).

https://lptk.github.io/programming/2020/03/26/demystifying-m...

https://dl.acm.org/doi/10.1145/3409006

Parreaux is continuing to work on this problem, and has since removed one of the assumptions/simplifications (positive/negative types) in his work on MLstruct

https://github.com/hkust-taco/mlstruct

Female Asian Elephant Calf Born at the Smithsonian National Zoo

Show HN: Zest – A hands-on simulator for Staff+ system design scenarios

Show HN: DeSync – Decentralized Economic Realm with Blockchain-Based Governance

Automatic Programming Returns

Why Are There Still So Many Jobs? The History and Future of Workplace Automation [pdf]

The Search Engine Map

Show HN: Souls.directory – SOUL.md templates for AI agent personalities

Real-Time ETL for Enterprise-Grade Data Integration

Economics Puzzle Leads to a New Understanding of a Fundamental Law of Physics

Switzerland's Extraordinary Medieval Library

A new comet was just discovered. Will it be visible in broad daylight?

ESR: Comes the news that Anthropic has vibecoded a C compiler

Frisco residents divided over H-1B visas, 'Indian takeover' at council meeting

If CNN Covered Star Wars

Show HN: I built the first tool to configure VPSs without commands

AI agents from 4 labs predicting the Super Bowl via prediction market

EU bans infinite scroll and autoplay in TikTok case

Benchmarking how well LLMs can play FizzBuzz

Why I Joined OpenAI

Octave GTM MCP Server

Show HN: Portview what's on your ports (diagnostic-first, single binary, Linux)

Voyager CEO says space data center cooling problem still needs to be solved

Boilerplate Tax – Ranking popular programming languages by density

Zen: A Browser You Can Love

My GPT-5.3-Codex Review: Full Autonomy Has Arrived

Show HN: FastLog: 1.4 GB/s text file analyzer with AVX2 SIMD

God said it (song lyrics) [pdf]

I left Linus Tech Tips [video]

Program Theory

Show HN: Local DNA analysis skill for OpenClaw