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. > Summary: Static

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. > Summary: Static vs dynamic typing debates often flounder because the debators see from two different perspectives without knowing it. Learning to identify the two perspectives can calm the discussion. The tension between the two perspectives has led to Gradual Typing and other technologies. I'm not buying this. The best pragmatic answer for myself is that static types is better in large or across teams. Dynamic typing is good for solo or early development by a small team. Gradual typing is the best you can get when a product developed with dynamic typing grows to be developed by many.

awkward 3y ago
It's comparing static typing as exists in Haskell or OCaml to static typing as exists in C++ or Typescript. To dynamically type a program in the first group, you would have to manually make a giant type that includes everything and use that everywhere. In the second, you can program dynamically by turning the safety off.
- deleted 3y ago
  [deleted]
- hardlianotion 3y ago
  Are you sure you meant C++ in the second group? In Typescript you can program dynamically, perhaps. In C++, you'd have to cast everything brutally, which I don't think most would call programming dynamically, or do what you propose for OCaml.
  - awkward 3y ago
    Casting at all really solidly puts it in that group. The idea that there’s a program and a type system and you tell the type system when it’s diverged from the program doesn’t really work in the other group of languages.
    - hardlianotion 3y ago
      (Complete rewrite) I think this may be true in theory but not a practical way to think about c++, as the language fights you if you try to use in that way.
beders 3y ago
The ability to reason about code, to split it into modules that can be developed independently etc. is not dependent on having a static type system. It is dependent on having a specification. "Types" is just one form of, in many languages quite limited, specs.
- nyssos 3y ago
  > "Types" is just one form of, in many languages quite limited, specs. That's the "Curry types" perspective described in the article, yes. "Church types" are syntax, not specification. In Haskell, for example main = print (5 + "foo") isn't a program that fails to conform to its spec, it's just not a program. It has no meaning and no behavior, not wrong behavior. You can (but should never) `unsafeCoerce` `5` to `String` or `"foo"` to `Int` and get something broken out - but they'll be different broken things, and neither will in any sense be the compiled form of the `main` function above.
ltr_ 3y ago
I agree with your sentiment and resonate with some of my opinions on languages (been reading about TT and abstract math in general for a while as a hobby) my opinions so far (subject to change as i read more): dynamic typing = just one type [0]. yes, good to test ideas quick, to develop quick gigs that i don't care about and tiny snippets/scripts, i use js for that. gradual typing = guaranteed mess evolving large code bases, I guess the gradual typing thing in practice never happen and when it happens your IDE becomes red and your compiler errors explode, i don't recall where i read about that but it made sense to me, i used groovy to take advantage of the optional typing but i was the only dev in that project. sound type system + parametric polymorphism = the best thing around, although i prefer to have explicit type annotations. no formal math object behind a language = the language does not exist, just , absurd rules ,idioms and syntactic mess that you have to remember and tied to specific monkey patched implementations to compensate incoherent foundations, sadly unavoidable, as most, if not all popular languages do not exist,. Yes, I've been reading Harper a lot. [0] https://existentialtype.wordpress.com/2011/03/19/dynamic-languages-are-static-languages https://existentialtype.wordpress.com/2011/03/19/dynamic-lan... edit: formatting
throwaway81523 3y ago
> 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.

awkward 3y ago

It's comparing static typing as exists in Haskell or OCaml to static typing as exists in C++ or Typescript. To dynamically type a program in the first group, you would have to manually make a giant type that includes everything and use that everywhere. In the second, you can program dynamically by turning the safety off.

deleted 3y ago
[deleted]
hardlianotion 3y ago
Are you sure you meant C++ in the second group? In Typescript you can program dynamically, perhaps. In C++, you'd have to cast everything brutally, which I don't think most would call programming dynamically, or do what you propose for OCaml.
- awkward 3y ago
  Casting at all really solidly puts it in that group. The idea that there’s a program and a type system and you tell the type system when it’s diverged from the program doesn’t really work in the other group of languages.
  - hardlianotion 3y ago
    (Complete rewrite) I think this may be true in theory but not a practical way to think about c++, as the language fights you if you try to use in that way.

beders 3y ago

The ability to reason about code, to split it into modules that can be developed independently etc. is not dependent on having a static type system. It is dependent on having a specification. "Types" is just one form of, in many languages quite limited, specs.

nyssos 3y ago
> "Types" is just one form of, in many languages quite limited, specs. That's the "Curry types" perspective described in the article, yes. "Church types" are syntax, not specification. In Haskell, for example main = print (5 + "foo") isn't a program that fails to conform to its spec, it's just not a program. It has no meaning and no behavior, not wrong behavior. You can (but should never) `unsafeCoerce` `5` to `String` or `"foo"` to `Int` and get something broken out - but they'll be different broken things, and neither will in any sense be the compiled form of the `main` function above.

ltr_ 3y ago

I agree with your sentiment and resonate with some of my opinions on languages (been reading about TT and abstract math in general for a while as a hobby) my opinions so far (subject to change as i read more): dynamic typing = just one type [0]. yes, good to test ideas quick, to develop quick gigs that i don't care about and tiny snippets/scripts, i use js for that. gradual typing = guaranteed mess evolving large code bases, I guess the gradual typing thing in practice never happen and when it happens your IDE becomes red and your compiler errors explode, i don't recall where i read about that but it made sense to me, i used groovy to take advantage of the optional typing but i was the only dev in that project. sound type system + parametric polymorphism = the best thing around, although i prefer to have explicit type annotations. no formal math object behind a language = the language does not exist, just , absurd rules ,idioms and syntactic mess that you have to remember and tied to specific monkey patched implementations to compensate incoherent foundations, sadly unavoidable, as most, if not all popular languages do not exist,. Yes, I've been reading Harper a lot. [0] https://existentialtype.wordpress.com/2011/03/19/dynamic-languages-are-static-languages https://existentialtype.wordpress.com/2011/03/19/dynamic-lan... edit: formatting

throwaway81523 3y ago

> 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.