3 ms·

> I can't tell if there's anything here I should be trying to learn. Best I can tell it's choosing obtuse naming for Static and Dynamic typing. No not at all,

> I can't tell if there's anything here I should be trying to learn. Best I can tell it's choosing obtuse naming for Static and Dynamic typing. No not at all, both are static. Church style typing means all the terms are annotated with their types. In practice, languages like Haskell have some type inference, so the compiler figures out some of the annotations for you (or even all of them, in easy cases) instead of making you annotate everything, but inside the compiler every term is marked with a type (whether supplied by you or inferred by the compiler). In Curry style typing, there are no annotations at all, and the type inference algorithm has to figure everything out itself. In the most general case, this problem is Turing-complete, i.e. undecideable. Part of the challenge in projects like Liquid Haskell is to automate as much inference as possible without running up against this barrier.

karmakaze 3y ago
The way the article describes Curry style typing seems like dynamic/optional/gradual types to me. > Curry-style types is when a system of types is applied that is not part of the semantics of the language. This is what Clojure has in core.typed. The meaning of a Clojure program is not dependent on it passing the type checker---it can be run without it. The type checker simply alerts you to type errors in your code. Note that you could consider your type checker to be your own head, which, as flawed as it may be, is what most Clojure programmers use. The types could be anywhere outside of the language. I'm not familiar with Clojure/core.typed--how is it different than TypeScript (or JavaScript with the type checker in your head)? It seems that if the type check fails it does so statically, but often it doesn't fail statically but rather at runtime. I can see that is a distinction but understanding this difference doesn't offer much practical value.

karmakaze 3y ago

The way the article describes Curry style typing seems like dynamic/optional/gradual types to me. > Curry-style types is when a system of types is applied that is not part of the semantics of the language. This is what Clojure has in core.typed. The meaning of a Clojure program is not dependent on it passing the type checker---it can be run without it. The type checker simply alerts you to type errors in your code. Note that you could consider your type checker to be your own head, which, as flawed as it may be, is what most Clojure programmers use. The types could be anywhere outside of the language. I'm not familiar with Clojure/core.typed--how is it different than TypeScript (or JavaScript with the type checker in your head)? It seems that if the type check fails it does so statically, but often it doesn't fail statically but rather at runtime. I can see that is a distinction but understanding this difference doesn't offer much practical value.