[k_bx]

What you cannot do is compile-time safety guarantees, and in languages like Rust type system isn't strong enough to do some advanced compile-time guarantees (via types). So no, you cannot do this in basically any language (unless you turn it into Haskell).

[pkolaczk]

Rust (and Scala) type systems are somewhat stronger and more expressive in some areas than Haskell. Weaker in some other. But it’s not a clear cut that Haskell type system offers more safety guarantees.

[thesz]

  > But it’s not a clear cut that Haskell type system offers more safety guarantees.

You can log operands in your implementation of Rust's Add trait, or compute running sum of one of the operands. In Haskell it is not possible unless you use unsafePerformIO from System.IO.Unsafe.

Haskell's type system controls effects available to the code. This can be used to implement programs adhering to specific formulas of Linear Temporal Logic or implementing a protocol specification, where operations on any given phase and side are restricted by type system.

I used Haskell's type system to prevent crossing of clock domains in the hardware description eDSL. Also, it was of great help in the CPU simulator description, fixing available commands and resources for different CPU models.

Even the logic of Rust's borrow checker was expressible in Haskell as early as February 2009 - there was HList, there was ParameterizedMonad and that's about what one needs for implementation of borrow checker.

[josephg]

Can you give some examples? What is Haskell’s type system capable of that you can’t express in rust?

[IggleSniggle]

Caveat emptor, I'm not a Haskeller, just an admirer. But Haskell let's you run functions over the type system itself very elegantly, so you can have a type that is derived from a type that composes three types that are derived from several functions' declared runtime behavior. This kind of type inference can provide arbitrarily rich information about anything in the entire program, letting you encode more than just range-types etc at compile time.

This comes with some design drawbacks. I think Rust's borrow checker would be implementable but unreasonable in Haskell: Haskell already does lazy-evaluation on types to enable its arbitrary depth of type expressivity. But the borrow checker also wouldn't really make sense for Haskell because the default programming model uses a GC. I think Linear Haskell might be a kind of Rust-in-Haskell, though.

Again, caveat emptor.

[k_bx]

I've spent long time writing Haskell and now write Rust professionally, so let me tell you something. The stuff where you really want to "program in types" lives beyond Haskell, in languages like Agda, Idris, some HoTT stuff etc. anyways.

In principle the more developed the type system is – the closer it to not distinct between types and values. Caviat is that its "type inference" gets worse.

So, in those more developed languages, you could have type-level proofs (guarantees) that your calculator produces correct results, as a proof, as theorems. That 2+3 will be 5, not as runtime test assertion, but as a theorem, that no other result is possible no matter what happens. Or that your parser will never fail on valid JSON etc. but nobody guarantees it's going to be a pleasant thing to write, maintain, and debug. And compile times will probably be terrible.

[uecker]

What the parents describe can be done with almost any language.

[thrawa8387336]

No you cannot

[uecker]

They described the use of abstract data types. One can certainly use those in most languages - for sure in C.

[k_bx]

> runST :: (forall s. ST s a) -> a

> The rank-2 type (that is, the type s is scoped within the parenthesis and can't escape) of runST ensures that the mutable references created inside the computation cannot escape due to being tagged with the type s. Internally, all sorts of imperative nonsense may occur. Externally, the function is pure. The world outside the boundary gets none of the mutation, only the result.

C does not have parametric polymorphism, nor rank-2 quantifications, so no, this cannot be done in C.

[uecker]

This was not the original claim in the thread I responded to which as "even with a dynamically typed language, you can keep escaped strings as an Escaped class, with escape(str)->Escaped and dangerouslyAssumeEscaped(str)->Escaped functions (or static methods)." so this was about abstract data types and not polymorphism.

Regardless, you can also have some limited parametric polymorphism in C with macros. This is very poor, but parametric polymorphism in Rust is based on monomorphization so it is also quite poor. You can also have higher-order polymorphism in C but then you need to use subtype polymorphism.