It struck me quite recently that a fundamental divide exists between ML-like languages which can basically infer all types for you and languages with powerful type-systems which can’t (Haskell, Rust, etc…).

I wonder which type of language is easier to teach?

For those which teach, do you go via the write the type declarations route or everything is automatically inferred for you?

Uh, should clarify for Haskell I mean the subset of Haskell + extensions which people typically use.

Even though your type system fully supports type inference, you probably want to write type annotations anyway, at the very least at the top-level declarations. Two reasons:

1. It serves as a documentation
2. It serves as a ground truth.

Definitely for anything which is exported between boundaries; I’d also add a third, which is related to 2. which is that with languages with powerful compile-time dispatch it can help guard against “spooky” action at a distance.

But it definitely feels like there’s a ton of busywork, esp. where you require annotations for anything apart from variables within a function body.

I’ve written a hefty amount of SML, and even in that you occasionally need type annotations to compile. I’ve never taught it, but I tend to code/experiment as “leave off the types” and then make a pass later when things are more set to add annotations back.

I don’t understand what the distinction you’re making is. Haskell and SML do basically the same amount of inference, and Rust is also similar but syntactically restricts inference to force you to write more annotations that it could theoretically infer.

@samth I meant distinction in terms of culture/development loop. In ML it doesn’t seem that you write the type signatures out during development like @ben.knoble alludes to. But in Haskell, many of the libraries mean you pretty much have to write out the top-level signatures since it doesn’t infer them - especially when dealing with some of the more hairy encodings which rely on universal quantification.

I think modern OCaml culture writes similar amounts of signatures to modern Haskell

Maybe it’s just because I’m looking though the intro materials to F sharp/Bucklescript/Elm then.

Oh and ofc, at the extreme end you have Agda and Idris which you use the types to generate the code.

Though I think you’re right @samth, I’m significantly more familiar with one than another, so it’s not right for me to make a sweeping statement.