5 ms·

Honestly you can nearly write Haskell without specifying type signatures. GHC is very sophisticated. I feel like there have only been a few situations where I a

by foxes 7y ago

Honestly you can nearly write Haskell without specifying type signatures. GHC is very sophisticated. I feel like there have only been a few situations where I actually needed to specify the type. Really the argument shouldn't be about having strict types vs dynamic, it should be about smarter compilers etc. To me, GHC seems to be nearly perfect (also GHCi).

87zuhjkas 7y ago
I agree, GHC has the best type inference that I know of.
nestorD 7y ago
Ocaml also standout as a language in which you can omit type definitions (the only exception I ever needed was when deserializing data).
- aloisdg 7y ago
  In the same vein F# as a descendant of OCaml, opens all of this fot the .Net world.
  - nestorD 7y ago
    F# adds a [] operator to access containers (mostly arrays and dictionnaries) and unifies arithmetic operators (no more +.). While I believe those make for a more streamlined language (I do prefer F# to Ocaml), it also means that you regularly need type signature to desambiguate things where nothing was needed in Ocaml.
deleted 7y ago
[deleted]
yogthos 7y ago
HM style type inference is nice, but the root problem is that the static type system restricts you to a set of statements that it is able to verify at compile time. This necessarily leads to code that prioritizes the needs of the compiler over those of the human reader. The more things you try to encode using the type system, the more complex your code becomes because proving something correct for all cases is typically significantly more difficult than just stating it and testing for the set of cases you care about. Furthermore, there is no way to verify that your type definitions themselves are correct. When you start moving program logic into types, the compiler cannot help you ensure that it's correct. Here's a fully typed insertion sort [1] written in Idris. It's over 260 lines long, and it takes non trivial amount of effort to understand it fully, and know that what it specifies is indeed what was intended. Meanwhile, I can trivially read and understand a 10 line Python version in its entirety. Of course, you could argue that it's an extreme case, and that in practice you probably wouldn't have such an exhaustive type specification. At that point you'd be agreeing that relaxing type constraints does provide a benefit, and we'd just be arguing about our respective levels of comfort. [1] https://github.com/davidfstr/idris-insertion-sort/blob/master/InsertionSort.idr https://github.com/davidfstr/idris-insertion-sort/blob/maste...
- Drup 7y ago
  This is really an apple to oranges comparison. What you linked is not an implementation of the insertion sort. It's a an implementation coupled with proof of correctness. Try to make a mechanize proof of correctness of your python code, and it'll be as long (or longer). If you just write an implementation in statically typed languages like OCaml, F#, Haskell, Typescript (or even Idris, if you go less crazy with the typing), and you can get it down to less 10 lines easily.
  - yogthos 7y ago
    A proof of correctness is what static typing is fundamentally. The example I provided simply turns this up to 11. However, if you relax the constraint then you're losing benefits of statically checking properties at compile time. If you agree that having a 10 line version that does less checking is better than having a 260 line version that does, then you're agreeing that there is a cost associated with static checking. There are plenty of real world scenarios where static checking gets in the way even if you're not trying to encode complex properties using the type system. One problem is that static typing is at odds with modularization since type declarations are considered globally. For example, Ring HTTP abstraction in Clojure represents requests and responses as maps. Middleware functions [1] can update these maps to inject additional keys, or modify existing keys. These functions often live in separate libraries that know nothing about one another. A static type system precludes this since it would require you to provide a static declaration for every possible request and response map. [1] https://github.com/ring-clojure/ring/wiki/Middleware-Patterns https://github.com/ring-clojure/ring/wiki/Middleware-Pattern...
    - aidenn0 7y ago
      Static typing does not prevent this; the fact that static typed languages can parse freeform formats like JSON works as a simple example. If you statically prove that you check that they keys are there before using them, then the type system can be satisfied.
      - 7y ago

by foxes 7y ago

87zuhjkas 7y ago

I agree, GHC has the best type inference that I know of.

nestorD 7y ago

Ocaml also standout as a language in which you can omit type definitions (the only exception I ever needed was when deserializing data).

aloisdg 7y ago
In the same vein F# as a descendant of OCaml, opens all of this fot the .Net world.
- nestorD 7y ago
  F# adds a [] operator to access containers (mostly arrays and dictionnaries) and unifies arithmetic operators (no more +.). While I believe those make for a more streamlined language (I do prefer F# to Ocaml), it also means that you regularly need type signature to desambiguate things where nothing was needed in Ocaml.

deleted 7y ago

[deleted]

yogthos 7y ago

HM style type inference is nice, but the root problem is that the static type system restricts you to a set of statements that it is able to verify at compile time. This necessarily leads to code that prioritizes the needs of the compiler over those of the human reader. The more things you try to encode using the type system, the more complex your code becomes because proving something correct for all cases is typically significantly more difficult than just stating it and testing for the set of cases you care about. Furthermore, there is no way to verify that your type definitions themselves are correct. When you start moving program logic into types, the compiler cannot help you ensure that it's correct. Here's a fully typed insertion sort [1] written in Idris. It's over 260 lines long, and it takes non trivial amount of effort to understand it fully, and know that what it specifies is indeed what was intended. Meanwhile, I can trivially read and understand a 10 line Python version in its entirety. Of course, you could argue that it's an extreme case, and that in practice you probably wouldn't have such an exhaustive type specification. At that point you'd be agreeing that relaxing type constraints does provide a benefit, and we'd just be arguing about our respective levels of comfort. [1] https://github.com/davidfstr/idris-insertion-sort/blob/master/InsertionSort.idr https://github.com/davidfstr/idris-insertion-sort/blob/maste...

Drup 7y ago
This is really an apple to oranges comparison. What you linked is not an implementation of the insertion sort. It's a an implementation coupled with proof of correctness. Try to make a mechanize proof of correctness of your python code, and it'll be as long (or longer). If you just write an implementation in statically typed languages like OCaml, F#, Haskell, Typescript (or even Idris, if you go less crazy with the typing), and you can get it down to less 10 lines easily.
- yogthos 7y ago
  A proof of correctness is what static typing is fundamentally. The example I provided simply turns this up to 11. However, if you relax the constraint then you're losing benefits of statically checking properties at compile time. If you agree that having a 10 line version that does less checking is better than having a 260 line version that does, then you're agreeing that there is a cost associated with static checking. There are plenty of real world scenarios where static checking gets in the way even if you're not trying to encode complex properties using the type system. One problem is that static typing is at odds with modularization since type declarations are considered globally. For example, Ring HTTP abstraction in Clojure represents requests and responses as maps. Middleware functions [1] can update these maps to inject additional keys, or modify existing keys. These functions often live in separate libraries that know nothing about one another. A static type system precludes this since it would require you to provide a static declaration for every possible request and response map. [1] https://github.com/ring-clojure/ring/wiki/Middleware-Patterns https://github.com/ring-clojure/ring/wiki/Middleware-Pattern...
  - aidenn0 7y ago
    Static typing does not prevent this; the fact that static typed languages can parse freeform formats like JSON works as a simple example. If you statically prove that you check that they keys are there before using them, then the type system can be satisfied.
    - 7y ago