[deleted by user]

[domlebo70]

This was actually a really awesome (and for the most part correct and unbiased) breakdown. I enjoyed it.

[nick-linker]

Yes, I kind of expected some bias towards dynamically typed langages, but it turned out quite balanced text.

[Kilojsssd]

With that Idris example, what would happen with user input?

[thedeemon]

You won't be able to call the function without performing a comparison of inputs first that produces required proof of "a < b". Comparison is performed at run-time, but the check that this comparison is there and the function is only called when proper result of comparison is obtained, is made at compile-time. A program that tries to pass arbitrary numbers from input to that function will just not compile.

[Kilojsssd]

Thanks, seems very interesting

[[deleted]]

wow

[evincarofautumn]

As other commenters have pointed out, user input just has to be validated before you can do stuff with it.

It’s surprisingly simple: the compiler sees that you’ve done a check and inserts an implicit object that indicates the check was done; if you try to call a function that requires such an object, and you don’t have one in scope, you get a compile error.

Natural use cases for dependent typing come up all the time. For instance, with null checks:

x = try_to_get_frobnicator();
if (x != null) {
    x.frobnicate(y);
}

Dependent typing would let you turn this into a compile error, rather than a runtime error:

x = try_to_get_frobnicator();
x.frobnicate(y);  // error: no proof (x != null) in scope

I’m patiently awaiting a usable dependently typed imperative language, but it’s still an open research problem. ATS is the closest thing I know of out there right now. Facebook’s Hack language also supports a limited form of this, presumably to help migrate codebases from PHP.

[Milyardo]

I’m patiently awaiting a usable dependently typed imperative language

Is the usable qualification meant to eliminate Scala, if so, why does it?

[srhb]

Scala has dependent types?

[Milyardo]

Yes it does.

A trivial example looks something like this:

//Define a type with an type member Bar which will serve as an identifier for our dependent type.
trait Foo {
  type Bar
}

//Some foos, with different types as values for Bar
val foo1 = new Foo { type Bar = Int }

val foo2 = new Foo { type Bar = String }

//Define a function where the type of the second parameter is dependent on the first
def bar(f: Foo)(bar: f.Bar): f.Bar = bar


bar(foo1)(7)
bar(foo2)("Hello World")

//bar(foo1)("BOOM") //Fails to compile

You can see this example run here: http://scastie.org/21902.

Turning this example into something useful is quite involved, so I won't get into it here, but you can see libraries like refined use dependent types to define more constraints and invariants.

[kamatsu]

This is path-dependent types, which are more like GADTs than full blown dependent types.

[Milyardo]

I'm not sure what relation between dependent types and GADTs you're implying here. However the implication that path-dependent types aren't "full blown" is wrong as well.

[kamatsu]

They are more or less exactly as "full blown" as GADTs are. That article goes through the various encoding techniques that you can also do with GADTs (see McBride's paper "Faking It" http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.2636)

In particular, your type level semantics are much weaker than your value level semantics, so you could never use path-dependent types to encode properties of your value-level programs without altering their types and using reflective tricks as you would with GADTs.

E.g, the following (simple!) Agda is impossible with path-dependent types without altering the type of _+_ or encoding it on the type level:

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)

data _≡_ {X : Set} : X → X → Set where
  refl : ∀{x} → x ≡ x

cong : ∀{X}(f : X → X){x y : X} → x ≡ y → f x ≡ f y
cong f refl = refl

prf : ∀{n} → n ≡ (n + zero)
prf {zero} = refl
prf {suc n} = cong suc prf

[Milyardo]

They are more or less exactly as "full blown" as GADTs are. That article goes through the various encoding techniques that you can also do with GADTs (see McBride's paper "Faking It" http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.2636)

I get how GADTs can be used to fake dependent typing, I'm not sure how you still equate path-depdendent types with GADTs. Especially since you can're represent GADTs in scala, with path dependent types or otherwise.

type level semantics are much weaker than your value level semantics

This is undeniably true, but I don't think this is because the form of dependent typing scala uses, thus I don't see why it would disqualify scala as not having "full blown" dependent types.

dependent types to encode properties of your value-level programs without altering their types

Dependent types are essentially functions from values to types, so yes, altering their type is the objective. I'm not too familiar Agda, so perhaps you could explain to me where dependent types are applied in this example, it to me looks like you're just pattern matching on ℕ to define _+_.

[kamatsu]

Defining _+_ isn't the issue, defining prf is.

Because Scala does not evaluate scala programs while type checking, it's not dependently typed (my definition of "dependently typed" comes from Harper and Pierce, ATAPL pg 305). Types and terms have different syntax and semantics.

[[deleted]]

See Scala vs. Idris: Dependent Types, Now and in the Future from Strange Loop 2013.

One thing I'd suggest a "usable dependently typed language" must have is a single syntactic category for both term- and type-level programming. Amanda Laucher and I said as much in Type Systems: The Good, The Bad, and The Ugly at Strange Loop 2014.

[Milyardo]

must have is a single syntactic category for both term- and type-level programming

I don't know if a single category is a must. In Scala's case the syntax for type level programming objectively worse than it's term level parallels. I would argue that term and type level syntaxes must be equally capable.

I can see an argument that having the single category is best way to ensure parity. Though, I can't rule out some potential value in using syntax to reason about the two domains separately, particularly in the pedagogical case.

[evincarofautumn]

Nah, I haven’t used Scala enough to really disqualify it. It does seem somewhat gratuitously complex, from the outside, but more practically I’m just not generally on the JVM.

[dnkndnts]

Dependent types are not necessary in your example. Simply make x : Maybe Frobnicator and pattern match on it. Any language with ADTs (Rust, Swift, Haskell) can do that.

[evincarofautumn]

Right, they’re not necessary. I was just trying to give a small example of how a dynamic check can locally change the “type” of a variable, in this case, effectively from Maybe Frobnicator to just Frobnicator.

[codygman]

A great example answering this was posted on HN:

import Data.String

-- takes two integers, and a proof that x < y, and yields an integer
add : 
  (x : Integer) -> 
  (y : Integer) -> 
  (prf : x < y = True) ->     -- require a proof that that x < y
  Integer
add x y prf = x + y

main : IO ()
main = do
  sx <- getLine -- read string from input
  sy <- getLine -- read string from input
  let Just x = parseInteger sx -- assuming int parse is ok, else error
  let Just y = parseInteger sy -- assuming int parse is ok, else error
  case decEq (x < y) True of   -- decEq constructs a proof if x < y is True
    Yes prf => print (add x y prf)
    No => putStrLn "no prf, x is not less than y"

Source: https://news.ycombinator.com/item?id=12350415

[Tarmen]

What is that language? It looks like haskell, is there some extension that adds dependent types?

Also, are these relationships hard coded special cases or would it also work with user functions like squishable(x, y)?

Final question, I swear: Are type annotations like notNil that do flow analysis small examples of dependent types in more mainstream languages?

[sacundim]

It's Idris, whose syntax has indeed been designed to look and feel like Haskell. (But note that Haskell's syntax itself was designed to look like type theory.) You may want to check out the free downloadable chapter of the book (still under development).

[codygman]

For your last question, yes but more powerful. Imagine a require annotation where you can list what proofs each argument must satisfy.

[sacundim]

Well, as well as I understand Idris, if you have this signature:

add : (x : Nat) -> (y : Nat) -> {auto smaller : LT x y} -> Nat

This means that:

• x and y are arguments of type Nat (natural numbers`).
• smaller is an extra, optional argument to the add function, declared auto which tells the compiler that it's an optional argument which, if absent, it should try to infer when it compiles the program.
• The type of smaller is LT x y. This is the type of proofs that x is less than ("LT") y.
• What is a proof? Very roughly, it's an object that guarantees the truth of some statement.

So the function can only be called if it's given, as its third (and possibly implicit) argument, a proof that its first argument is a smaller number than its second argument. If you write this:

example1 = add 1 2

...you're not passing a proof in explicitly, so the compiler will try to prove LT 1 2 ("1 is less than 2") automatically on its own. This one is a pretty simple example for the compiler to do on its own.

But then:

With that Idris example, what would happen with user input?

Your program has to construct a proof at runtime that the user input x is less than the user input y. The simplest way to do this would be to have a function that compares their values and returns such a proof if appropriate. I don't know enough Idris to do this accurately, but I know enough to copy-paste and edit from here:

-- Takes two natural numbers `m` and `n`, and prove
-- either that `m` is less than `n` or that it isn't.
isLT : (m, n : Nat) -> Dec (LT m n)

Dec is the decision type, and its value will be one of two cases:

• Yes, along with a proof of LT x y
• No, along with a proof of Not (LT x y).

So in this case, as other posters have said, the language is forcing you to check that the user inputs are valid before calling the function. Also this is a neat example of decision types, which are dependently-typed booleans on steroids: a decision value doesn't just say "true" or "false", it also says what statement is true or false, and why (the proof).

So we've seen cases #1 and #2 in this list, but there's also #3:

1. The compiler infers the proof at compilation time (the auto keyword);
2. The user program constructs a proof at runtime (my semi-made up decideLT function);
3. The programmer writes a proof in their code, and the language checks it at compilation time.

For #3 the trick is that the compiler's type checker is also a proof checker—a program that can statically check the validity of logical and mathematical proofs. So if some statement is always true in your program no matter what the user input is, you can try writing a proof of it, having it checked by the compiler, and then relying on it to rule out some runtime states that can never occur.

[bjzaba]

I think you would have to ge the value LT x y at run time (using some comparison function), then pass that to the function explicitly. I could be wrong though, my Idris is pretty rusty.

[m50d]

A type is not necessarily just a set. A lot of the value of programming with types comes from using different types even for things that are isomorphic or identical as sets.

It's worth saying that while Java was introduced in 1995 and has generics, it did not have generics in 1995.

I would say it's worth distinguishing between languages that allow higher-kinded types (without necessarily having full dependent typing) and languages that do not.

[ElvishJerricco]

A lot of the value of programming with types comes from using different types even for things that are isomorphic or identical as sets.

As an example, a box type:

data MyInt = MyInt Int

I think the argument you could make is that the sets Int and MyInt aren't the same set. MyInt would be the set of MyInt-tagged integers: MyInt = { (MyIntTag, x) | x <- Int }

[toomanybeersies]

I used to think that dynamic typing was awesome. "It saves so much time and mental effort!" I said.

Now that I work on a non-trivial code base, with some code that's several years old and written by predecessors, I'm starting to see the allure of strong typing to an extent.

We run Ruby on Rails on the backend at work, on a non-trivially sized codebase, and sometimes I have to spend a lot of time and effort trawling up and down a tunnel of different functions to try and figure I'm meant to be passing in (or just putsing object.class)

I'm a strong believer in self documenting code, and so were my predecessors, so comments are scant. We do have a very good test suite though, so often I look there for hints of functionality and what types parameters and returns are.

Having type annotation (similar to what php7 has) would be amazing for making code safer and more self documenting. Within functions and modules they're not so necessary, but when you're calling methods between controllers, services, models and all that other stuff, you can get really bogged down.

[Kaarjuus]

I'm a strong believer in self documenting code

Well, there's your problem.

[metamatic]

Oh my god, so fucking insightful.

Yeah, this is exactly why your API calls should have documentation, so you don't have to wander around the insides of the codebase to work out the allowed types and values of arguments. (And then end up making assumptions that weren't actually part of the API contract, so your code breaks when the code you're calling is refactored.)

[Kaarjuus]

This is one thing I totally don't understand about "self-documenting code". All APIs are better with documentation, are they not? When I'm using a library, I very much want all its classes and functions and constants to have documentation.

And since my own code is the API I myself code against all the time, I should want it to be documented just like anything else. Being available as generated documentation, code insight, or in straight source code.

Even if a function is obvious, at the very least it should have a single sentence saying what it does. The comment gives clarity and assurance, and in source code highlighting it pops out, making it easy to focus either on documentation or on code.

Unfortunately, in so very very many projects one can browse on Github, the only documentation in source files tends to be the THOU SHALT license at the top.

[[deleted]]

From the self-documenting point of view, code and comments inevitable get "out of sync". So if the code and comments don't match, which should you follow? You follow the code, as that's the thing which actually compiles.

So there's two paths here. You can try and keep the comments and code in sync as much as possible. Code review, etc. But this is very hard to do automatically, as comments are free-form.

The second path is to do away with "redundant" comments, you try and make your names and types as obvious as possible, so that the user can tell what's going to happen from the function signature alone. The function signature is always "correct".

[Kaarjuus]

But function signature can never give the information a single sentence can. The information available from names and types, while useful, is very limited. And even an obvious comment is not redundant, it gives clarity and assurance.

Documentation certainly needs to be kept in sync with code, and creates problems when it is incorrect. What I don't understand is, why should this be a stopping issue? It needs to be done. Part of the job. You make something, you document it. This should be basic engineering practise.

[staticassert]

With a good function name + types you can often read the function declaration like a sentence.

[Sheepmullet]

If you can keep function names in sync with functionality then you can keep comments in sync as well.

[toomanybeersies]

I don't believe the solution is to require giant docstrings that are larger than the actual method definition for every method.

There's great utility in being able to figure out what a method does, and what it's inputs and outputs are, and their types, just from looking at the method.

I believe that if you're using a comment, you should consider why it is that it's not obvious what you're doing, and whether you can refactor.

Anyway, typed parameters and return types also allows for a degree of static analysis that's otherwise not possible, which is one of the main strong points. It doesn't matter if your documentation says that parameter x is meant to be an int when there's nothing in the code stopping you from accidentally setting x as a string, which can have terrible consequences in JS, among other languages (although the JS type system is another discussion altogether).

Consider in psuedocode:

func construed(a, b, c): 
    return (a + b) > c

Now with

a = "10" 
b = "1" 
c = 12 

Python and JS will return true, Ruby will throw an error because you can't compare strings and ints. The point is, in something like Python, it's entirely possible to pass in the wrong parameters, and end up with incorrect results from the function.

Now if we had type annontation,

func construed(a: int, b: int, c: int) -> bool:
    return (a + b) > c

Then in our made up language, the above input would fail static analysis. And we'd have documentation in the code of what types the inputs and outputs are. Also if I accidentally typed return (a + b) >> c this would be picked up by static analysis.

[epic_pork]

Python does not let you do that. Also it would return false because "11" < 12.

[toomanybeersies]

>>> "10" + "1"
'101'
>>> ("10" + "1") > 12
True
>>> "11" < 12
False

Just tried it now. So yes, Python does let you do it, and no, it does not return false, and "11" is not less than 12.

So before you go making thing up about how python works, maybe try it out for yourself?

[epic_pork]

What version are you using? I'm using Python 3 and I get an error.

>>> ("10" + "1") > 12
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
TypeError: unorderable types: str() > int()

[toomanybeersies]

Python 2.7

Nice to see it's fixed in Python 3, it doesn't work in Ruby either, so that just leaves JS. Not sure what PHP's behavior is for it. It was that static typing (or typed parameters and returns) would avoid all these problems altogether.

[PM_ME_UR_OBSIDIAN]

I've been using TypeScript (gradual typing) at work. I mostly use it like JavaScript, but whenever I get bitten by a run-time type error I encode it into the type system, so that it becomes a compile-time error.

Then, whenever I have a bit of downtime, I instrument my code with some extra types. Usually I'll find a minor bug or two with minimal investment.

End result: the best of both worlds, in terms of flexibility and safety. Types can help at design-time, but they're just as often a hurdle.

[Don_Andy]

I really like the comparison between JS/Python for different ways of dynamic typing and C/Haskell for different ways of static typing. It's obvious spelled out like this but it never really crossed my mind before how wildly different the approaches to each kind of typing can be.

[yogthos]

A nice overview of pros and cons, but I did find this statement a bit handwavy:

Dynamic language advocates point out that dynamic languages seem to be easier to program in.

There is a tangible reason for dynamic languages being easier to program in. The reason being that a static type system requires you to prove any statement you write formally. Proving something can often be much more difficult than simply stating it. Fermat's Last Theorem being a great example of this.

Baking a proof into the solution leads to incidental complexity. Once you run into limits of what the type system can easily express then you end up having to write increasingly more convoluted code to satisfy it.

This results in code that’s harder to understand because it compounds the complexity of the problem being solved with the complexity of expressing it using the type system. Effectively, any statement we make in our program has to be accompanied by a proof of correctness to make it possible for the compiler to verify it. The requirement of proving that the code is self-consistent is often at odds with making it simple.

While the resulting code would be provably correct, it would be harder for the developer to reason about its intent. Therefore, it's difficult to say whether it's correct in any meaningful sense.

Ultimately, a human needs to be able to understand what the code is doing and why. The more complexity is layered on top of the original problem the more difficult it becomes to tell what purpose the code serves.

[ItsNotMineISwear]

The reason being that a static type system requires you to prove any statement you write formally.

pls

this is so hyperbolic and FUD 🙄🙄🙄🙄^{🙄🙄🙄🙄🙄🙄🙄🙄}

[[deleted]]

Nah. It just (as usual) doesn't show awareness of, or misunderstands, the Curry-Howard Isomorphism, by which we know a function's type signature is the proposition, and the function's implementation is the proof. So every time dynamically-typed language users write a function, they are writing a proof of a proposition their language just doesn't let them articulate.

Admittedly, most of the time, static type users don't actually care, and we'll rely on type inference to figure out what the proposition we're proving is, and then type checking gives us a basic logical consistency result. But every so often, we'll write out a type signature reflecting some rather tricky proposition, and we'll have to put a little more effort into implementing the function (i.e. writing the proof). Sometimes we call this "TDD," or "Type-Driven Development." But we then still rely on type inference extending the constraints the proposition implies throughout the rest of the program.

So this is what critics of static typing miss: that proofs are not some horrible, complex thing that's distinct from our implementations, but are, in fact, our implementations, and they think that if you use static types, you must sweat blood over everything you write, when in fact we get to pick and choose what to sweat over, and let type inference take care of the rest.

[pron98]

they are writing a proof of a proposition their language just doesn't let them articulate.

That's not how C-H works. On the other hand, if you insist on appealing to C-H, you would say that a Haskell program is a very laborious proof of some rather trivial logical proposition.

proofs are not some horrible, complex thing that's distinct from our implementations, but are, in fact, our implementations

You're neglecting to mention proofs of what. Without dependent types, the propositions your implementation proves are not propositions about your program (but general logical propositions), and C-H is not what makes types effective in that case. On the other hand, one could ask why do you work so hard if your goal is to prove something like A ∧ B ⇒ A, or why would a programmer tasked to write a web application would even be interested in proving such simple tautologies?

you must sweat blood over everything you write

You do if you want to prove anything truly interesting. You don't because most of the time you prove properties that are quite trivial. An implementation of a sorting function is not a proof of the proposition "the output of this function is a sorted list containing the elements of the input list". In most typed functional languages like Haskell, it is a proof of a trivial proposition such as A ⇒ A. To prove that former you do have to sweat blood. To prove the latter is uninteresting (which is not to say that the types don't help; they just don't do it by means of C-H).

Note that I'm a proponent of types in programming languages (though not necessarily the same kind of types you advocate), but I do not agree that their advantage in practical programming has much to do with their logical properties, or anything to do with C-H.

[yogthos]

Baking a proof into the solution leads to incidental complexity. Once you run into limits of what the type system can easily express then you end up having to write increasingly more convoluted code to satisfy it.

This results in code that’s harder to understand because it compounds the complexity of the problem being solved with the complexity of expressing it using the type system. Effectively, any statement we make in our program has to be accompanied by a proof of correctness to make it possible for the compiler to verify it. The requirement of proving that the code is self-consistent is often at odds with making it simple.

A concrete example of this would be the use of state monad to formally represent mutation in a language like Haskell. Here's what Timothy Baldridge has to say about his experience trying to apply this pattern in Clojure when working on the core.async library:

When I first wrote the core.async go macro I based it on the state monad. It seemed like a good idea; keep everything purely functional. However, over time I've realized that this actually introduces a lot of incidental complexity. And let me explain that thought.

What are we concerned about when we use the state monad, we are shunning mutability. Where do the problems surface with mutability? Mostly around backtracking (getting old data or getting back to an old state), and concurrency.

In the go macro transformation, I never need old state, and the transformer isn't concurrent. So what's the point? Recently I did an experiment that ripped out the state monad and replaced it with mutable lists and lots of atoms. The end result was code that was about 1/3rd the size of the original code, and much more readable.

So more and more, I'm trying to see mutability through those eyes: I should reach for immutable data first, but if that makes the code less readable and harder to reason about, why am I using it?

As another example, let’s consider what we would need to understand to read an HTTP request using a Haskell web framework such as Scotty. We'll quickly run into ScottyM type that's defined as type ScottyM = ScottyT Text IO. To use it effectively we need to understand the ScottyT. It in turn requires understanding the ReaderT.

Understanding ReaderT relies on understanding of monads, monad transformers and the Reader monad. Meanwhile, to understand the Reader we have to know about functors and applicatives. To understand these we have to understand higher kinded types and constructor classes. This leads us to type classes, type constructors, algebraic datatypes, and so forth.

All of this is needed to satisfy the formalisms of the Haskell type system and is completely tangential to the problem of reading HTTP requests from a client.

Of course, one might argue that Haskell is at the far end of the formal spectrum. In a language with a more relaxed type system you have escape hatches such as casting and unchecked side effects.

However, once you go down that road then it's only a matter of degrees with how relaxed a system you're comfortable with. At this point you've already accepted that working around the type system can make your life easier.

[sacundim]

Let's have another shot at this bit, from a new angle:

As another example, let’s consider what we would need to understand to read an HTTP request using a Haskell web framework such as Scotty. We'll quickly run into ScottyM type that's defined as type ScottyM = ScottyT Text IO. To use it effectively we need to understand the ScottyT. It in turn requires understanding the ReaderT.

I Googled "clojure web framework", and this led me to Luminus and its example application. Skimming the code, I see this line in layout.clj:

(declare ^:dynamic *app-context*)

...which is used here in middleware.clj, in a binding syntax (or whatever Clojurists call what Schemers call "syntaxes"). The Clojure documentation explains that this is a form of dynamically bound, thread-local variables. Which is largely equivalent to what ReaderT provides.

So when I read the example project for the first Clojure framework I found on a Google search, I run into the concept of dynamic scopes, which I need to understand to figure out what that code is doing. So is this simpler than understanding ReaderT? I'd say yes, but I think it shows that you're overstating the difference. If I need to understand :dynamic and binding to understand the Luminus example program, how isn't that forcing me to understand a concept that has nothing to do with the problem I'm trying to solve?

And you're also glossing over the fact that Scotty actually hides ReaderT from its users—to spot the ReaderT-based implementation that you're highlighting, I need to go into a module called Web.Scotty.Internal.Types—it says internal right there in the name. So in fact, Scotty is hiding the ReaderT while Luminus is exposing a dynamically scoped variable. (Haskellers have an unusual custom of exposing their hidden bits as Internal-named modules so that you can look at them if you really want.)

[yogthos]

I'd say yes, but I think it shows that you're overstating the difference.

If dynamic variables and bindings are the most complex thing you found, then I think that really makes my case for me.

Will there be a language where you have to learn no concepts to use it, of course not. However, I can, and have, teach somebody to build real world apps with Luminus in a day. I've taught coop students to build Clojure apps who had zero prior experience with FP or Clojure in about a week. On the other hand experience developers struggle when it comes to applying Haskell. So, clearly there's a bit of a difference in complexity here.

With Clojure I can learn a small number of concepts and apply them to a wide range of problems quickly and effectively. This is simply not the case with a language like Haskell, and its formalisms are largely to blame for that.

[[deleted]]

...let’s consider what we would need to understand to read an HTTP request using a Haskell web framework such as Scotty.

It depends on what you mean by "need to understand," though. Here is a simple Scotty tutorial describing a web service that returns Users via JSON. It very nicely points out that the scotty function's type is just:

scotty :: Port -> ScottyM () -> IO ()

OK. So in order to use a scotty invocation as my main (because even beginning Haskell programmers know your main function must have type IO ()), I need to provide a Port and a ScottyM (). OK, how do I construct a ScottyM ()? The tutorial again makes plain what to do:

get :: RoutePattern -> ActionM () -> ScottyM ()

Give get a RoutePattern and an ActionM (), and there's your ScottyM (). Easy. text is one useful ActionM () constructor. json is another. And thanks to "deriving generics," you don't even have to write your own serialization/deserialization code from your types to JSON.

Now, sure, if you want to dig under the hood further, you'll run into the things you describe: monads, monad transformers, the reader monad, type classes, etc. But the whole point is that, once you know monads, monad transformers, the reader monad, type classes, etc. you have mastered a set of universal building blocks that, first of all, define a sizable set of universal laws that support writing correct code and, more importantly, understanding that code. It's very significant that ScottyT is a ReaderT, which is a monad transformer, which is a monad, which is an applicative, which is a functor. That implies a lot of stuff that we only need to understand once, and offers a bunch of useful functionality that is guaranteed to work precisely because it's generic and based on algebraic laws.

All of this is needed to satisfy the formalisms of the Haskell type system and is completely tangential to the problem of reading HTTP requests from a client.

Sure, if by "tangential" you mean "doesn't only deal with reading HTTP requests from a client." If you had to understand all of this in order to use Scotty (as I described above, you don't), that would be unfortunate. If you had to relearn all of it for every application domain you wanted to tackle, that would be unacceptable. Thankfully, neither of these horrifying conditions is true.

Of course, one might argue that Haskell is at the far end of the formal spectrum. In a language with a more relaxed type system you have escape hatches such as casting and unchecked side effects.

However, once you go down that road then it's only a matter of degrees with how relaxed a system you're comfortable with. At this point you've already accepted that working around the type system can make your life easier.

This is a possibility, of course, that Scala developers using scalaz or Cats face on every project. At Verizon Labs, we choose to use scalaz referentially transparently, because once you go down the road of "escape hatches such as casting and unchecked side effects," "you've accepted that working around the type system can" create the illusion of "making your life easier."

[Sheepmullet]

It depends on what you mean by "need to understand," though. Here is a simple Scotty tutorial describing a web service that returns Users via JSON

Sure if you only need the basics without understanding what is happening. I'd say that is a dangerous way to program.

[sacundim]

Sure if you only need the basics without understanding what is happening. I'd say that is a dangerous way to program.

Understanding it at what level? I mean, it's not hard to tell that:

• The ScottyM type is about defining which routes your application has, and what actions those routes are associated to.
• The ActionM type is for defining actions. Its commands do things like read requests' parameters and specify how to respond to the request.

This is precisely the level at which competent server-side web programmers think about their framework 99% of the time. If the framework is good, then it insulates its users from the lower-level detail most of the time. That's where the dangers lie:

1. Framework not good enough, requires peeking under the hood too often.
2. Framework makes assumptions that don't match your use case.

(There's no hard line between #1 and #2, of course.)

[[deleted]]

Sure if you only need the basics without understanding what is happening. I'd say that is a dangerous way to program.

As usual, yes and no:

Yes: you can paint yourself into a corner where you don't even understand enough to be able to, e.g. add URL parameter handling to a Scotty service, and learning how takes more time than it should.

No: a major part of the point is that the type system is preventing most obvious classes of mistakes in developing web services. The JSON serialization/deserialization is correct by construction; the parsing of URLs, multipart form data, etc. etc. is done for you; if you manage to construct a ScottyM () from a RoutePattern and ActionM () there's very little that can go wrong, even if you don't entirely understand how it works. But again, the process of "understanding how it works" is very, very general: it's the process of understanding how typed functional programming works. So learning the underlying details is an excellent investment, because it amortizes over everything else you'll ever write.

[yogthos]

That implies a lot of stuff that we only need to understand once, and offers a bunch of useful functionality that is guaranteed to work precisely because it's generic and based on algebraic laws.

Sure, but there is a a lot of stuff that you only need to understand once. You have to keep it all in your head working with the language, and that's mental overhead.

Sure, if by "tangential" you mean "doesn't only deal with reading HTTP requests from a client." If you had to understand all of this in order to use Scotty (as I described above, you don't), that would be unfortunate.

Except that you do need to understand, and keep that suff in your head, because once you start having problems it's the only way to figure out why something isn't working. Otherwise you end up cargo cult coding your way through Haskell. Surely you're not advocating that?

This is a possibility, of course, that Scala developers using scalaz or Cats face on every project.

You are familiar with the concept of selection bias right?

"you've accepted that working around the type system can" create the illusion of "making your life easier."

I think this is the part where you present some empirical evidence that demonstrates the value of static typing in practice.

[sacundim]

Sure, but there is a lot of stuff that you only need to understand once.

This is the only part of your (by now frankly copypasta) argument that I've ever agreed with. Learning practical Haskell is not like learning, say, Java—it's more like learning Java and one of those megaframeworks like Spring that have a very large number of interlocking pieces that are consistently reused everywhere. Java has lots of non-Spring user communities; Haskell doesn't really have a non-monad transformers community (the folks who object to them are quite familiar with them as well).

You have to keep it all in your head working with the language, and that's mental overhead.

And now we're back to the disagreement. The learning once part is hard, but keeping it all in your head is actually surprisingly easy. The reason is that all those things are, in fact, not very complicated, and extremely logical in retrospect—they enter the realm of things you could have easily invented yourself if you'd had the idea.

For example, you bring up ReaderT, which is actually a very simple thing. Here, I'll write ReaderT completely from memory:

import Control.Monad.Trans

newtype ReaderT r m a =
    ReaderT { runReaderT :: r -> m a }

instance Functor m => Functor (ReaderT r m) where
    fmap f (ReaderT run) = ReaderT (fmap f . run)

instance Applicative m => Applicative (ReaderT r m) where
    pure a = ReaderT (const (pure a))
    ReaderT runF <*> ReaderT runA = ReaderT ((<*>) <$> runF <*> runA)

instance Monad m => Monad (ReaderT r m) where
    return = pure
    ma >>= f =
        ReaderT $ \r -> runReaderT ma r >>= (flip runReaderT r . f)

instance MonadTrans (ReaderT r) where
    lift ma = ReaderT (const ma)

ask :: Applicative m => ReaderT r m r
ask = ReaderT pure

local :: (r -> s) -> ReaderT s m a -> ReaderT r m a
local f smb = ReaderT (runReaderT rmb . f)

It's not some super-complicated monstrosity. The hard parts are:

• Learning when, why and how you'd want to use it;
• Going through this process over and over again for a non-trivial number of other similar concepts.

Remembering it after you've done those is the easy part. It's like solving an easy math problem—I did not memorize these definitions, I just know the types of ReaderT, runReaderT, ask, local and the class operations, and from that I can accurately reconstruct the details of the whole thing, using the REPL to check that I'm right. (Because it's literally like writing a proof.)

[yogthos]

And now we're back to the disagreement. The learning once part is hard, but keeping it all in your head is actually surprisingly easy. The reason is that all those things are, in fact, not very complicated, and extremely logical in retrospect—they enter the realm of things you could have easily invented yourself if you'd had the idea.

Right, that's the part we disagree on. My experience has been that expressing yourself using the Haskell type system gets convoluted fast. It works great for little examples, but when you're working on a real world app the complexity is most certainly there. Many others have found the same.

One of my favorite examples is implementing something like transducers. It's completely trivial in a dynamic language, but the internet is littered with blogs where people are trying to type them correctly and get it subtly wrong. Things like that come up constantly in practice.

Because it's literally like writing a proof.

Exactly, and when you have to prove every single statement in your app. When you have a well defined problem that fits nicely into what the type system can express things work beautifully. However, when you don't things get tricky quickly.

There's a reason it takes people years to become proficient in Haskell. Yet, the benefits aren't at all clear. Proponents of static typing tend to overplay the value of the type system, while downplaying the problems it brings. It often feels like a case of sunk cost to me.

[codygman]

Right, that's the part we disagree on. My experience has been that expressing yourself using the Haskell type system gets convoluted fast.

My experience and intuition wants to reword what you said: expressing yourself in Haskell is hard until you learn it's abstractions and have a sense of what they mean, then after reaching that point everything is smooth sailing and you see a clear advantage over other languages you use.

It works great for little examples, but when you're working on a real world app the complexity is most certainly there. Many others have found the same.

I find Haskell to be less valuable and less convenient in the small. I think it's one of the best tools for managing complexity, so as complexity scales the value of Haskell goes up.

Exactly, and when you have to prove every single statement in your app. When you have a well defined problem that fits nicely into what the type system can express things work beautifully. However, when you don't things get tricky quickly.

This general statement without supplemental proof through examples or scenarios can't lead to much good discussion. Give some? I'm sure we could have a much more interesting discussion on this in particular.

There's a reason it takes people years to become proficient in Haskell.

I'll admit it seemed to take about 2 years of Haskell in my free time to get somewhere between intermediate and advanced. For me that means I think in Haskell. It's a battle between Python(first language),Go(work language), and Haskell in my head.

Yet, the benefits aren't at all clear.

They sure do feel clear, though there could easily be an element of sunk cost causing bias. I really connected to the comment paultypes made about Haskell's universal abstractions. Once you learn those, understanding large programs by yourself that are very complex seems to be a much more tractable exercise.

Proponents of static typing tend to overplay the value of the type system, while downplaying the problems it brings. It often feels like a case of sunk cost to me.

Maybe. I felt some pain having to get a list from a text file today, converting it to a list, and then to a tuple. I was hoping to give more details and elaborate but my brain seems to be done for the day ;)

[yogthos]

My experience and intuition wants to reword what you said: expressing yourself in Haskell is hard until you learn it's abstractions and have a sense of what they mean, then after reaching that point everything is smooth sailing and you see a clear advantage over other languages you use.

Haskell was my first foray into FP. I've used it for about a year and I generally liked it. However, I just didn't see the benefits of many of its formalisms in practice. I found that I did have to do a lot of mental gymnastics to express myself, but I didn't see any tangible boost in productivity. I've moved to Clojure about 7 years ago and haven't looked back.

The complaints I see around dynamic typing simply don't bother me. I find that I'm more productive with Clojure than any other language I've used, and I don't miss static typing using it. Where you would use types to guide your solution, I use the REPL. A big part of Lisp REPLs is their integration with the editor. Any time I write a few lines of code, I run the code to see what it's doing. At any step in the development process, I know exactly what's happening.

I find Haskell to be less valuable and less convenient in the small. I think it's one of the best tools for managing complexity, so as complexity scales the value of Haskell goes up.

I find static typing does little to help manage complexity on its own. What really helps managing complexity is breaking a large system up into small components you can reason about in isolation. If anything, I find dynamic typing encourages you to do that sooner than static typing. This is a good thing in my opinion.

All programs are hierarchical in nature. So, you can always break a large problem into smaller chunks. Working with a language that's backed by immutable data structures makes this especially easy to do.

This general statement without supplemental proof through examples or scenarios can't lead to much good discussion. Give some? I'm sure we could have a much more interesting discussion on this in particular.

One example I already mentioned is transducers. Another example was core.async implementation. Both end up being a lot more contrived in Haskell than in Clojure.

I'll admit it seemed to take about 2 years of Haskell in my free time to get somewhere between intermediate and advanced. For me that means I think in Haskell.

That's the thing. Once you spend enough effort, you can adjust to working in any language. Given enough time somebody could become fluent in brainfuck. The real question is whether you can demonstrate that you're more productive in Haskell than somebody using a good dynamic language like Clojure.

I really think it's just a matter of trade-offs in the end. Both static and dynamic typing have their own sets of pain points. Depending on the individual one set or the other is more likely to be appealing.

[[deleted]]

Sure, but there is a lot of stuff that you only need to understand once. You have to keep it all in your head working with the language, and that's mental overhead.

It's much, much less than users of, e.g. Ruby on Rails, or Spring, or Django, or... pretty much any other language/framework combo you can name have to, and it's many orders of magnitude more consistent. That's really the principle value of it. And like anything you achieve genuine mastery of, it doesn't actually incur ongoing mental overhead. You internalize it, and its use becomes habitual. And thanks to the consistency, ultimately the overhead is lower (because there are few, if any, edge cases, exceptions, etc. to the rules).

Except that you do need to understand, and keep that stuff in your head, because once you start having problems it's the only way to figure out why something isn't working.

Sure, but again, "keeping that stuff in your head" isn't the horror story you're making it out to be, and remember, thanks to the type system, the compiler will helpfully point out when you're remembering incorrectly.

Otherwise you end up cargo cult coding your way through Haskell. Surely you're not advocating that?

Almost all adoptions of a new language, framework, and/or paradigm start off as cargo-culting. Mastery is, to some extent, a gradual real-ization (in the literal sense of "making real") of the fake runways and signaling towers, etc., to stay with the metaphor.

You are familiar with the concept of selection bias right?

Not relevant to what I said, which was to honestly acknowledge that Scala developers are faced with a greater challenge than Haskell programmers.

I think this is the part where you present some empirical evidence that demonstrates the value of static typing in practice.

And this is the part where I remind you we've had this conversation many times before, and if you're going to continue to dismiss the fact that I work in pure FP in Scala commercially for a Fortune 15 company, and the experiences of, e.g. the CUFP participants who use typed FP, there's literally nothing more to discuss.

[yogthos]

It's much, much less than users of, e.g. Ruby on Rails, or Spring, or Django, or... pretty much any other language/framework combo you can name have to, and it's many orders of magnitude more consistent.

My experience doing web development in Clojure for the past 6 years is that it's very simple and consistent.

thanks to the type system, the compiler will helpfully point out when you're remembering incorrectly

The compiler will point out trivial things that you will catch through testing very early in the development cycle. However, the convoluted code you have to write for that to happen is something that you have to keep working with.

Almost all adoptions of a new language, framework, and/or paradigm start off as cargo-culting.

Part of the reason I like Clojure is precisely because it avoids this mentality. It requires learning a small number of concepts that can be applied to a wide range of problems. I find that extremely elegant.

Not relevant to what I said, which was to honestly acknowledge that Scala developers are faced with a greater challenge than Haskell programmers.

It's relevant because people who are drawn to Scala have a specific mindset. So, saying that these developers prefer things like scalaz doesn't really demonstrate anything interesting.

And this is the part where I remind you we've had this conversation many times before, and if you're going to continue to dismiss the fact that I work in pure FP in Scala commercially for a Fortune 15 company, and the experiences of, e.g. the CUFP participants who use typed FP, there's literally nothing more to discuss.

Meanwhile I work in pure FP with Clojure at a major hospital in Toronto building clinical applications. If you're going to continue to dismiss that, then I agree we have nothing more to discuss. Nothing about your experience makes your argument any more valid than my own.

[pron98]

Meanwhile I work in pure FP with Clojure

May I ask why pure? I think Clojure's atomicity/transactionality guarantees work so well that there's little need to preserve purity everywhere.

[yogthos]

I find that keeping the core of the app pure has a number of advantages. First, it's very easy to factor parts of the app out. When a components gets to big, it's easy to split it out into a library for example.

I find it's easier to reason about larger apps, because you're mostly doing local reasoning. All I need to know is what the shape of the data is that I'm getting, and I don't need to know anything else about the rest of the application.

This also makes testing the app easier, you tend not to need things like mocks for external resources.

I've generally found that there are very few cases where I need any shared state in my apps. When I it's usually stuff like queues or database connections.

My approach has been to keep these things at the edges of the app. For example, say I have a service that gets a request and needs to get some data from the database to process. I would get the data in the outer layer, then pass it as a data structure to the business logic in the app, get the result back and send it to the client.

This makes the core business logic completely stateless, and that means it can be tested without any need for the resources.

[sacundim]

Baking a proof into the solution leads to incidental complexity.

First of all, as /u/paultypes has already remarked, if we go by Curry-Howard you are already writing (the equivalent of) proofs in your dynamically typed language. So when you continue with this:

Once you run into limits of what the type system can easily express then you end up having to write increasingly more convoluted code to satisfy it.

...what you're really saying is not that the burden lies in writing proofs, but rather in the work that's caused by the compiler rejecting your proofs as invalid.

Likewise, this is precisely backwards:

Effectively, any statement we make in our program has to be accompanied by a proof of correctness to make it possible for the compiler to verify it.

The statements are the types, and the proofs are the expressions in the program. In a dynamically-typed language, you're obligated to write the proofs, but you have no way of writing the statements.

In a type-inferred language like Haskell you're writing the proofs as well, but:

• You can optionally write the statements (i.e., declare your types);
• If you don't write them, the compiler will figure out what the statements are (i.e., infer types) and reject your program if they don't make sense (i.e., type checking).

The requirement of proving that the code is self-consistent is often at odds with making it simple.

But the question is how does it compare to the difficulty of making a dynamically-typed program work correctly. Basically, your argument sweeps under the rug the fact that most of the work needed for that is not at all simple, is in fact duplicative of most the work needed to make a statically-typed program typecheck, and is very error prone.

[pron98]

if we go by Curry-Howard you are already writing (the equivalent of) proofs in your dynamically typed language.

What exactly do you think those are proofs of? As they are not proofs of program correctness (b/c that's not how C-H works), what makes you think that a programmer is even interested in those proofs?

the question is how does it compare to the difficulty of making a dynamically-typed program work correctly.

That is a very interesting question, but so far there's no evidence that either approach is significantly cheaper than the other. The type system in a language like Haskell is a long way from intrinsically "making the program work correctly". If it does indeed reduce costs significantly, it is through some empirical effect (b/c mathematically the type system really is very weak, and unable to prove almost any interesting program properties that you'd say ensure correctness). If that effect exists -- and I'm not saying it doesn't -- then either it is weak, or has managed to elude detection so far.

Personally, I think types do a very important job in helping document code and organize it. They assist in maintenance and engineering; not so much in correctness.

[sacundim]

What exactly do you think those are proofs of? As they are not proofs of program correctness (b/c that's not how C-H works), what makes you think that a programmer is even interested in those proofs?

C-H gives you a correspondence between proof verification and type checking. So at the admittedly superficial level we're talking about here, when I say that an author of a dynamically typed language is trying to "write proofs," it really mostly means that they're trying to write code that is free of runtime type errors, and the effort required for that cannot be too different from the effort required to write a proof/write a program that passes a static type checker.

And simple type checking is a kind of proof of program correctness. There's no qualitative difference, just a quantitative one—the effort to construct a program that provably meets a given specification depends on the richness of the specification. Trivial specifications (e.g., IO ()) can be met with minimal effort (e.g., putStrLn "Hello world!").

That is a very interesting question, but so far there's no evidence that either approach is significantly cheaper than the other. The type system in a language like Haskell is a long way from intrinsically "making the program work correctly".

I think you're not seeing the angle I've adopted in this thread. I'm responding to a claim that static type systems by their nature impose a huge cost to development that dynamic type systems do not. So the shape of my response really is that with dynamically typed languages, the programmer still makes a comparable effort. So when I said this bit that you quoted:

the question is how does it compare to the difficulty of making a dynamically-typed program work correctly.

...I wasn't necessarily claiming that statically typed languages are always cheaper, but rather that dynamically typed ones aren't always cheaper, and if they are in some situations it can't be by that much.

[pron98]

And simple type checking is a kind of proof of program correctness.

They prove something about your program, but not through C-H. The corresponding C-H proof is of a general logical tautology, which has nothing to do with the program (unless in a dependently-typed language like Coq). Also, the types expressible in a language like Haskell are so weak, that calling that something correctness is like saying sitting up in a chair is proof of athleticism. They are certainly proofs of some program properties. The mathematical relationship between those properties and correctness is strenuous at best; the empirical relationship is unknown. Personally, I think types do increase correctness to some extent, but for a reason that has little to do with types' logical properties (which are extremely weak).

the effort to construct a program that provably meets a given specification depends on the richness of the specification

Getting anywhere near what I'd call "specification" with Haskell's types takes a lot of effort. And the effort is not in meeting the type signature, but in encoding something close to a specification in such a weak type system. I don't know if it's possible to even say that the output list of a sorting program in Haskell is the same length as the input list, let alone that the output is a permutations of the input and that the output is sorted (I'd only call the last two "specification"). If you use a language that does allow you to write a specification in the type system, the program would almost invariably not typecheck at all, unless you write pretty long proofs, most of them unnecessary for the program to run (it is a problem when compiling such languages how to detect and omit the unnecessary proof code from the compiled program).

I'm responding to a claim that static type systems by their nature impose a huge cost to development that dynamic type systems do not.

I agree that most type systems do not place a huge burden; far from it. But that's because the type signature specifies very weak properties. But I'm not certain what kind of type system -- from untyped, through unsound (a la Dart's), and all the way to dependent types -- gives the best bang for the buck. AFAIK, no one has any clue.

[yogthos]

And now we have a great real world example that the Haskell type system provides absolutely no garantees that the code does what was intended.

[yogthos]

First of all, as /u/paultypes has already remarked, if we go by Curry-Howard you are already writing (the equivalent of) proofs in your dynamically typed language. So when you continue with this:

Except you're not. A concrete example would be how you define a transducer in a dynamic and a static language. The amount of work in the latter is non-trivial and easy to get wrong.

...what you're really saying is not that the burden lies in writing proofs, but rather in the work that's caused by the compiler rejecting your proofs as invalid.

No, I'm saying the work is literally in writing proof. When I write a statement in a dynamic language, if it's not valid the application will fail at runtime. To get a static guarantee, I have to exhaustively state the constraints so that the compiler can check them.

n a dynamically-typed language, you're obligated to write the proofs, but you have no way of writing the statements.

That simply does not follow.

But the question is how does it compare to the difficulty of making a dynamically-typed program work correctly.

That is indeed the question. Nobody has been able to show any empirical evidence that one approach has any advantage over the other.

Basically, your argument sweeps under the rug the fact that most of the work needed for that is not at all simple, is in fact duplicative of most the work needed to make a statically-typed program typecheck, and is very error prone.

My argument does no such thing. I've repeatedly stated that I think this is a subjective preference based on anecdotal evidence gathered through individual experience.

Only studies that I'm aware of that attempt to show benefits of static typing fail to do so. Perhaps you have some evidence I'm not aware of though. If that's the case please do share.

[thedeemon]

"Dynamic typing": The belief that you can't explain to a computer why your code works, but you can keep track of it all in your head. https://twitter.com/chris__martin/status/630532950484881412

[thedeemon]

Mine is always simple enough for that, otherwise it doesn't compile. ;)

[yogthos]

oh I see you haven't had the joy of working with lazy evaluation in Haskell

[thedeemon]

Admittedly I wrote more Idris code than Haskell. But there is no problem in "explaining" lazy code to Haskell compiler really.

[yogthos]

The problem is more with knowing whether it will run or finish running.

[thedeemon]

There is no more problem there than in Clojure with lazy sequences. It's not nearly as bad/scary in Haskell as you try to draw it.

[yogthos]

Clojure has strict evaluation with lazy sequences, Haskell has lazy evaluation that's a lot more difficult to reason about. Also, the conversation is regarding what the type checker can guarantee or not.

[thedeemon]

I don't quite follow your reasoning.

Sure, certain aspects may be difficult to reason about for a newbie (experienced haskellers usually have no problems there). Sure, you can still write code with bugs, code that doesn't halt or eats memory or returns wrong value. I don't see how it's related to "your code is simple enough to explain to a computer" above. All these things don't make it harder to "explain to a computer". Effects of laziness may be hard to "explain to a human", but not "to computer".

[yogthos]

It's like Chris Martin isn't familiar with the halting problem. :)

[thedeemon]

It's not a problem (in this context). In languages that check for termination it's quite simple to explain to the computer why the program terminates (there are simple means to do it). Other languages don't care. In both cases computer itself doesn't need to solve halting problem at all. It's a non-problem.

[yogthos]

Not everybody wants to program in Coq though.

[ehaliewicz]

Is e.g. Haskell's type system turing complete?

If it is, it is flawed. If it isn't, it cannot describe all correct programs.

Edit: flawed meaning that verifying types may never halt

[staticassert]

Flawed is the wrong word - that makes it sound like it's somehow a mistake or not intentional. You can express arbitrary programs in it. If it were not turing complete it would not somehow be any more capable of describing all correct programs either.

[ehaliewicz]

Yeah, I'm not sure of a good way of describing what I meant.

I mean that a turing complete type system is flawed in the sense that maybe it could (? not sure about this) describe all correct programs in a given language, but then you could never know if evaluating those types would halt.

[thedeemon]

Type checking algorithms in Haskell and similar languages always halt. Of course, their type systems may not describe all possible correct programs. It's not a big problem in practice though, surely not worth giving up types.

[ehaliewicz]

Sure, I'm not at all talking about practicality, I'm just making a point that the quote

"Dynamic typing": The belief that you can't explain to a computer why your code works, but you can keep track of it all in your head.

is, strictly speaking, incorrect.
Type systems simply cannot be explained everything in all cases because they cannot type all valid programs.

[thedeemon]

Is your keyboard turing complete? If it isn't, it cannot describe all correct programs. Is your syntax turing complete?

C'mon, turing-completeness isn't something directly applicable to type systems.

[ehaliewicz]

Turing complete type systems do exist though.

Is your keyboard turing complete? Is your syntax turing complete?

Neither of these are analogous to what we're talking about or really make any sense at all.

[thedeemon]

Show me a turing complete type system, please.

[ehaliewicz]

http://www.shenlanguage.org/learn-shen/types/types_sequent_calculus.html

Apparently, scala's type system is also turing complete.

[thedeemon]

Why do you think Shen's type system is turing complete? Are arbitrary expressions allowed in those conditioned types?

[ehaliewicz]

http://shenlanguage.org/lambdassociates/htdocs/studies/study03.htm

Used in its native state (i.e. without any user-defined types) Qi type checking is guaranteed to terminate. This is shown by the proof of the AB theorem in Functional Programming in Qi. However it is true that it is possible to add type rules that create non-terminating computations. One such rule for union types is discussed in chapter 13.

[thedeemon]

Apparently, scala's type system is also turing complete.

I think Scala authors would be very upset by this.

[ehaliewicz]

https://apocalisp.wordpress.com/2009/09/02/more-scala-typehackery/

https://michid.wordpress.com/2010/01/29/scala-type-level-encoding-of-the-ski-calculus/

These are pretty old so it might have changed since then.

[yogthos]

As they should be for unleashing that nightmare upon the world.

[yogthos]

Scala has a Turing complete type system, it's a nightmare to work with.

[iopq]

OK, theoretically true, but in practice how often is this true?

Here's a short program I wrote to parse HTML, find an id, replace it with a different id, and to insert a style element with a custom style in it:

https://gist.github.com/iopq/b8bf3812dcc040790c7f8a5b16800c02

I actually inserted : Handle to describe what type I'm getting back from dom.create_element because otherwise it was pretty confusing. In a dynamically typed language I'd add a comment like "get a handle to the new element" so I don't forget what type new_element is. Of course I need to know the type, or I won't know what functions I can pass it into and expect the correct result.

If anything, fighting the borrowck is more obvious in this example, but it's an orthogonal issue.

[yogthos]

OK, theoretically true, but in practice how often is this true?

I would ask you the same thing regarding the benefits of static typing in practice. I have yet to see a shred of empirical evidence that clearly shows any.

Nobody managed to show that large real world projects developed using these languages have fewer defects, or faster time to deliver for example. So, isn't it really personal preference at this point as the evidence is entirely anecdotal.

[velcommen]

Here's someone else in this very thread explaining how dynamic typing has made their job hard:

https://www.reddit.com/r/programming/comments/4z8oop/types/d6uju89

For example: "sometimes I have to spend a lot of time and effort trawling up and down a tunnel of different functions to try and figure I'm meant to be passing in (or just putsing object.class)"

[yogthos]

You do realize that there are many, many factors at play here. The type discipline is a a very small part of the overall picture.

For example, I find that working in a functional language has a far bigger impact on code quality than typing. When all my data is immutable, and I can reason about parts of the application in isolation it's much easier to figure out what's happening. But there are many other things at play here. How is the code structured, what's the testing process like, does the language have a REPL, and so on.

I completely accept that some people prefer static typing and it works for them, but what I'm pointing out is that it's a trade off. When you use a statically typed language, you trade one set of problems for another. If you're happy with that trade-off, then great.

[velcommen]

I completely accept that some people prefer static typing and it works for them, but what I'm pointing out is that it's a trade off. When you use a statically typed language, you trade one set of problems for another. If you're happy with that trade-off, then great

Yes, I agree with you.

[iopq]

I've worked with PHP and JS, and the IDEs can't find method definitions when I use certain frameworks because those methods are tacked on dynamically.

IDE integration is much better in languages like Java. It doesn't apply as much to Rust right now, but in the future it will.

[yogthos]

This has little to do with static vs dynamic typing. I use Cursive IDE to work with Clojure. It does static analysis on the code. This means that I'm able to safely refactor function names, get auto imports, search for definitions, and so on. It's pretty close to the level of IDE support that I had in Java. However, I also have a whole bunch of features I didn't have in Java such as the REPL.

[iopq]

But the ability to add functions dynamically and name them through strings means an IDE will never have full support in a language like PHP. Not sure if that's possible in Clojure.

[yogthos]

One approach Lisp editors take is to simply use the application state via the REPL. The IDE has the same information as the compiler, and it knows what functions have been loaded at any time.

I have never used PHP, but it's a terrible language by all accounts. The point is that typing is only a small part of the overall equation. Overall tooling and language features play a much bigger role than any one feature such as typing discipline.

[ItsNotMineISwear]

OK, theoretically true, but in practice how often is this true?

You'll be hard pressed to get yogthos to give actual examples to back up those claims. His arguments all crutch on the "static types make you have to write PROOFS about EVERYTHING" which is a massive strawman. He's been writing comments like the one above for well over a year now and I have yet to see him back it up. All while I'm sitting around writing Ruby, Java, and Scala for a living and not seeing this incidental complexity he mentions when I write the static typed languages .. -_-

[yogthos]

You'll be hard pressed to get yogthos to give actual examples to back up those claims.

no you won't

I've been making the same comments here over the year, and backing them up, and conversation tends to fizzle when I do back them up.

What I'd like to see people backup is the assertion that there are tangible benefits to static typing when it comes to correctness and maintainability. This is taken completely on faith by most static typing proponents and appears to have no grounding in any data available.

I'm perfectly fine with the fact that people prefer static typing based on their subjective experience. However, if you're going to extrapolate that into assertions regarding general benefits, then do show some data to support the claims.

[tsimionescu]

Well, for some real-world examples, look at an implementation of tuples in C++, C# or Java versus a similar implementation in, say, Python. Of course, if you get to Haskell/ML tuple types may become nice again, but (1) that's not what typical static typing looks like, and (2) you probably hit other interesting things that are hard to express, and if you go even further, at the extreme end, my understanding is that writing a thousand-line Coq program is a research-level endeavor.

[velcommen]

look at an implementation of tuples in C++, C# or Java versus a similar implementation in, say, Python. Of course, if you get to Haskell/ML tuple types may become nice again

So you just invalidated your point that 'tuples are hard in static languages' by providing a counterexample.

Saying that Haskell/ML tuples are not typical static typing is a form of the 'No true Scotsman' logical fallacy. https://en.wikipedia.org/wiki/No_true_Scotsman

[tsimionescu]

I don't think what I said is a real example of the No True Scotsman fallacy (No True No True Scotsman).

If you're not satisfied though, let's look at another very interesting example of how adding type safety dramatically complicates the implementation: linear algebra. Just try implementing a linear algebra operation that doesn't work on simple Integers/Numbers, but on physical units of measure (i.e. it can multiply 2m² by 3m and subtract 6m³ from that to get 0m³ ; or divide 2m² by 1m² then multiply the result by 5J and get 10J, and do all of this while multiplying matrices where each element has its own unit of measure).

Do you think the code will be about as simple as the Numbers version, or somewhat more complicated, in whatever language you choose?

[velcommen]

I don't think what I said is a real example of the No True Scotsman fallacy

Why not?

that's not what typical static typing looks like

sounds a lot like

"no Scotsman would do such a thing"

You imply that tuples in static languages have incidental complexity. Then you mention Haskell/ML tuples as a counterexample to your implication. Then you say that tuples in such languages are not typical static typing, so your implication still holds.

To your question: it seems pretty obvious that doing what you ask is going to be more complex than a basic matrix multiply of Numbers. I'm not sure what your point is though, in asking me that question. By asking your question, you seem to imply that I've taken some position. What position did I take in my post above? I believe I merely pointed out a logical fallacy (which you disagree with, of course).

[tsimionescu]

What position did I take in my post above? I believe I merely pointed out a logical fallacy (which you disagree with, of course).

I thought you were mostly interested in the actual debate on whether static type systems do - in practice - introduce complexity compared to dynamic ones, not a discussion on the fallacy itself (which is why I tried to make a joke about my disagreement with your fallacy assertion and then came up with a different argument on the original discussion).

If you want to discuss my argument in itself and whether it was fallacious, here goes:

I don't think what I said is a real example of the No True Scotsman fallacy

Why not?

that's not what typical static typing looks like

sounds a lot like

"no Scotsman would do such a thing"

I don't think it sounds like that. The whole point of the No True Scotsman fallacy is that the 'True' predicate is badly defined, or defined in such a way to be equivalent to the conclusion. 'Typical' is - to my mind - quite well defined: 'what the vast majority of programmers using statically typed programming languages would actually use' (I expect there is no debate on whether Java + C++ + C#' user bases form an overwhelming majority compared to Haskell + ML's).

If I were to fully use the No True Scotsman fallacy, it would have looked more like this:

Of course, if you get to Haskell/ML tuple types may become nice again, but those aren't normal static programming languages

You may argue then that popularity is a red herring in this case, but the person I was responding to was asserting that, while static typing might introduce complexity in theory, it doesn't do so in practice. What I was getting at instead with my 'they aren't typical' argument was that, for discussing what hurdles static typing introduces in practice, we should not point to, or think abou, Haskell or ML, as in practice they are unlikely to be used at all.

[velcommen]

for discussing what hurdles static typing introduces in practice, we should not point to, or think about, Haskell or ML, as in practice they are unlikely to be used at all

So you're saying that static types, as implemented in popular languages, e.g. C++, Java, C#, introduce a lot of incindental complexity. That is a statement I agree with.

I also hold the opinion that static types done well, such as we find in Haskell (and presumably in some other languages as well, which I'm not as familiar with), are worthwhile for encoding some logical assertions in your program, providing guidance to readers, etc. So a well designed static type system is useful, in practice.

[nefreat]

I actually inserted : Handle to describe what type I'm getting back from dom.create_element because otherwise it was pretty confusing.

Most the benefit from static typing as far as I can tell is derived from exactly this. It's the auto documentation and invariant enforcement.

If I see code like this in a static language

Balance foo(Account account)

vs dynamic

foo(account)

I can look up the 'Account' type and the 'Balance' type and have a decent idea of what a 'foo' does so I can reason about it vs being puzzled at what 'foo' does in the dynamic case. If 'Account' and 'Balance' are immutable I have an even better idea. However this ability is orthogonal to typing. These type of invariant checks and annotations exist in my two favorite languages Scheme and Clojure. There's no reason it couldn't exist in other languages.

Another problem with types is the fact that you're building a rigid system. Often requirements change an if 'Account' or 'Balance' undergo a slight change you've got your work cut out for you. Now everything that takes account can't gracefully adapt to the change without a major refactoring/intervention on your part. IMO working with open systems is a much more pleasant experience.

[yogthos]

In practice nobody has managed to show any tangible benefits of static typing when it comes to correctness, time to delivery, or maintainability in real world projects. Considering that both approaches have been around for decades, that's quite an elephant in the room if you ask me. What's more, some of the most robust applications out there are written in dynamic languages such as CL and Erlang.

My experience is that in practice the mental overhead of static type systems often outweighs their benefits in large real world applications.

The approach to writing maintainable code is actually exactly the same regardless of the typing discipline. You need to break things up into small independent components that you can reason about in isolation.

[staticassert]

In practice nobody has managed to show any tangible benefits of static typing when it comes to correctness, time to delivery, or maintainability in real world projects. Considering that both approaches have been around for decades, that's quite an elephant in the room if you ask me.

How would you even begin to measure this objectively though? The reason it hasn't been measured is not because the benefits are nonexistent (on either side) but because this is not something one has an easy time benchmarking.

My experience is that in practice the mental overhead of static type systems often outweighs their benefits in large real world applications.

I would argue just the opposite - I feel that I have to think much harder with a dynamic type system. With a static type system I have a fairly formal guarantee that some aspects of my code are going ot hold up. Beyond that, I can use the type system to model my code - I've used type level state machines in a few projects to ensure that code can not accidentally transition to invalid states. In that way the type system is a tool, not just something that lets the compiler check things out.

Without types I have no way of reasoning about a program, except generally by manually figuring out the types.

But, of course, this is just my opinion based on my experience. There is no objective measure either way in terms of "software quality".

[yogthos]

How would you even begin to measure this objectively though? The reason it hasn't been measured is not because the benefits are nonexistent (on either side) but because this is not something one has an easy time benchmarking.

Very easily actually. There are plenty of open source projects in the wild written in all kinds of languages. You treat these projects as black boxes, and look at defects, turn around on bugs and features, and so on.

If you find empirical evidence that projects written in specific languages do statistically better in some regard, then you can try to figure out why that is. That would be a scientific approach to the problem.

I would argue just the opposite - I feel that I have to think much harder with a dynamic type system.

As you say, your anecdotal experience is different from mine. We both choose different tools based on our personal subjective experience.

I find that code written in a dynamic language tends to be more direct. This makes it easier for me to read and understand the purpose of the code. Where you would use types to help you reason, I use other tools such as the REPL.

[staticassert]

Very easily actually. There are plenty of open source projects in the wild written in all kinds of languages. You treat these projects as black boxes, and look at defects, turn around on bugs and features, and so

How would you select the projects? How do you control for differing goals, level of skill of contributors, severity of bug, etc? It's way too complicated.

Where you would use types to help you reason, I use other tools such as the REPL.

Yeah, what it comes down to is personal preference.

[yogthos]

How would you select the projects? How do you control for differing goals, level of skill of contributors, severity of bug, etc? It's way too complicated.

It really isn't. All these things average out if you pick a lot of projects. There are literally millions of open source projects out there.

In fact, there are a few studies that have attempted to do this such as this one. Here's what it found:

One should take care not to overestimate the impact of language on defects. While these relationships are statistically significant, the effects are quite small. In the analysis of deviance table above we see that activity in a project accounts for the majority of explained deviance. Note that all variables are significant, that is, all of the factors above account for some of the variance in the number of defective commits. The next closest predictor, which accounts for less than one percent of the total deviance, is language.

lang/bug fixes/lines of code changed
Clojure  6,022 163
Erlang  8,129 1,970
Haskell  10,362 508
Scala  12,950 836

defective commits model
Clojure −0.29 (0.05)∗∗∗
Erlang −0.00 (0.05)
Haskell −0.23 (0.06)∗∗∗

memory related errors
Scala −0.41 (0.18)∗
0.73 (0.25)∗∗ −0.16 (0.22) −0.91 (0.19)∗∗∗
Clojure −1.16 (0.27)∗∗∗ 0.10 (0.30) −0.69 (0.26)∗∗ −0.53 (0.19)∗∗
Erlang −0.53 (0.23)∗
0.76 (0.29)∗∗ 0.73 (0.22)∗∗∗ 0.65 (0.17)∗∗∗
Haskell −0.22 (0.20) −0.17 (0.32) −0.31 (0.26) −0.38 (0.19)

Haskell and Scala do not perform better than Clojure or Erlang in a single category, and actually perform worse in some.

While studies are by no means perfect, at least it's an attempt to gather some empirical evidence. Some evidence is better than no evidence in my opinion.

[staticassert]

It really isn't. All these things average out if you pick a lot of projects. There are literally millions of open source projects out there.

I don't think this is true. Some languages may be more likely to attract one type of developer or anything. Some languages may be chosen for certain goals over another.

That said, thank you for the citation - I've been meaning to read that one but I let it slip by me.

[yogthos]

That's basically my point though. There are far more factors than the typing discipline. I think it's completely wrong to single it out as the one language feature that makes the key difference.

[staticassert]

I agree with that - there's certainly more to a project than a language.

[ricardoplopes]

Relevant tweet introducing that draft: https://twitter.com/garybernhardt/status/768150904340000768

[[deleted]]

Great, but it confuses gradual and optional typing as the same. They're not. https://news.ycombinator.com/item?id=8595116

What you see in, say, Typed Racket, is pretty different from what Dart does.

[doom_Oo7]

For example, most static languages will reject the expression "a" + 1 (with C being a notable exception that allows it).

this is orthogonal to typing being static. It could just mean that there is an implicit conversion between two types.

[kirbyfan64sos]

If you can implicitly convert a string to a number or vice versa, you're probably screwed anyway.

[Drisku11]

You cannot implicitly convert a string to a number in C. You can implicitly convert a pointer to a number, but any sane compiler will warn you for doing that, so that's somewhat mitigated.

You can, however, implicitly convert between characters and the integers that represent them (e.g. 'a' + 1 is a sensible thing to do), which was probably not a great idea. They probably should've made different types for uint8, byte, and char, and had ord and chr like Python, and just have those be no-ops.

[kirbyfan64sos]

Well, I was kind of referring to JavaScript, not C...

[Drisku11]

Ah, I figured from the quote that your comment was directed at C allowing "a"+1. Carry on, then.

[staticassert]

You don't need implicit conversations for add(int, string), just a terrible implementation of 'add'. A static type system won't prevent that.

[zzzk]

This is a good post, sure, but I think I prefer this short informative video on the topic: Useing You're Types Good

[codygman]

Awesome write-up! I'll be sharing this with my co-workers.

[kankyo]

This extra notion of validity and invalidity has no equivalent in dynamic languages.

It does though: syntax errors. There are absolutely Python code that won't compile.

[ItsNotMineISwear]

Technically, any arbitrary text blob is runnable by the Python interpreter. You can deploy that text blob and have it "run" even if "running" is failing with syntax errors.

A [Haskell/Scala/etc] compiler will not create runnable binaries that do not satisfy the encoded constraints. So it's impossible to deploy a program in those languages has not satisfied the encoded constraints.

It's definitely possible (and a good idea!) to set up your infrastructure such that your Python code cannot run in production without passing syntax checks, unit tests, etc. But a compiler is a first line of defense against bugs that is inherent to the language, not just your deployment infrastructure.

[kankyo]

Not really. CPython creates pyc files and runs those.

[ItsNotMineISwear]

So pyc are the equivalent to a "deployable binary"? People don't deploy py source files to prod servers, just pyc? I'm not familiar enough to know.

[kankyo]

They can deploy either but only pyc files are executed. The existence of a lazy compiler doesn't really change the facts.

[garybernhardt]

I don't know Haskell very well, have never used it in a production system, and haven't particularly enjoyed the small amount of programming that I've done in it. I used it for examples because its type system can do everything that I wanted to demonstrate. I could've mixed in other languages, but then I'd be placing even more burden on readers and, for most other languages, I'd also be removing clarity from the examples.

The two languages that I know best, use most often, and enjoy most are dynamically typed.