8 ms·

“Make illegal states unrepresentable” Types pay off the most on large systems. Architectural requirements captured formally. This more than ANYTHING else is w

“Make illegal states unrepresentable” Types pay off the most on large systems. Architectural requirements captured formally. This more than ANYTHING else is why I want to move enterprisey app code to Haskell. Having worked on numerous ginormous enterprisey systems -- which are usually doing pretty straightforward things, just at scale, and needing to be maintained by non-brilliant developers -- I can say pretty securely that north of 95% of the invariants could be lifted into the type system, making run-time errors a thing of the past. Also, in most frameworky big systems, you WANT to stop devs from "just doing IO" or pretty much doing anything without a strong contract around it. Monad stacks do wonders for circumscribing your computational context in an app. I wonder why they rewrote Aeson though ... perhaps before it was mature? Aeson's pretty awesome.

carterschonwald 12y ago
It might have to do with the way the default generics for aesons fromjson and tojson instances for record types are defined? Or maybe the lack of incremental streaming read write support in the aeson data model? Or maybe they wanted better date or integer support? It'd be pretty easy to ask don or Lennart I'd imagine. I have to say that I definitely enjoy using haskell when faced with dirty complicated data, which I'm told happens a lot in larger organizations.
eru 12y ago
> Monad stacks do wonders for circumscribing your computational context in an app. Wait until you discover the power of Applicative Functors. They are more restricted in their operations than Monads, so they compose better and allow for analysis.
- davdar 12y ago
  I'm curious, what do you mean they compose better and allow for analysis [better than monads]?
  - gergoerdi 12y ago
    You can determine a lot more about a computation described only in terms of an applicative functor as you can from a monadic one, without running any of its effects (i.e. "statically"). It's easy to see why when you consider the opaqueness of the function in the right-hand side of a bind. Check out http://gergo.erdi.hu/blog/2012-12-01-static_analysis_with_applicatives/ http://gergo.erdi.hu/blog/2012-12-01-static_analysis_with_ap... for an example.
  - tel 12y ago
    gergoerdi covered analysis, but composition is simple. For any two Applicatives F and G and value type A the following 4 values are all Applicative values F A G A F (G A) G (F A) But for monads only the first two are monads for general monads F and G. So, Applicatives compose better!
    - eru 12y ago
      And to get F (G A) with Monads, F needs to be a Monad transformer. In addition to composition, products of Applicatives are also Applicatives: (F A, G A)
      - tel 12y ago
        Even for monad transformers it's not necessarily the case that direct composition leads to a monad. For instance, ContT looks like newtype ContT r m a = ContT ((a -> m r) -> m r) so ContT M A is not the same as Cont (M A). Monads also compose under products as two parallel monadic computations data (f * g) a = Pair (f a) (g a) p1 :: (f * g) a -> f a p1 (Pair fa _) = fa p2 :: (f * g) a -> g a p2 (Pair _ ga) = ga instance (Monad f, Monad g) => Monad (f * g) where return a = Pair (return a) (return a) Pair fa ga >>= k = Pair (fa >>= p1 . k) (ga >>= p2 . k) You can also talk about composition under sums data (f + g) a = Inl (f a) | Inr (g a) and you'll get compositions of applicatives here so long as you have a notion of natural transformation class Natural f g where phi :: f a -> g a instance (Applicative f, Applicative g, Natural f g) => Applicative (f + g) where pure a = Inl (pure a) Inl ff <*> Inl fa = Inl ( ff <*> fa) Inr gf <*> Inr ga = Inr ( gf <*> ga) Inl ff <*> Inr ga = Inr (phi ff <*> ga) Inr gf <*> Inl fa = Inr ( gf <*> phi fa) but there's no way to get a similar monad. It turns out that you have to "know what branch to go down before you start" in exactly the kind of way applicatives allow and monad preclude.
- dkarapetyan 12y ago
  Mathematically speaking applicatives are less restrictive since more things can be applicatives than monads. A monad is a "very special" kind of functor and that is why a composition of monads often fails to satisfy the monad laws. The least restricted thing in this hierarchy is the functor since composition and other kinds of operations always give you back another functor.
fsloth 12y ago
A sidenote: There is nothing in Java/C++ etc that would stop one from making only legal states representable. It's just easier and more obvious in ML family...
- lomnakkus 12y ago
  That's only true in the most trivial Turing Tarpit sense, though. Ease of use and defaults matter in practice. E.g. you can do compile-time exhaustiveness-checked pattern matching using the visitor pattern in Java/C++, but try doing that in practice and the amount of boilerplate just becomes unbearable -- and actually obscures (rather than illuminate) the essence of the data structure. There's also the lack of higher-kinded types. (Or just plain syntactic pain of using HKTs e.g. in Scala.)
  - fsloth 12y ago
    Very true. I usually avoid complex constructs in C++ - especially in production code and strive to strike a balance between KISS and YAGNI. KISS comes first unless there is some obvious boilerplate that can be avoided... Encoding only valid states in subareas of code can be done within C++ without extravagant constructs. Ie. instead of passing around a Car with a Car::isDriving member implement a DrivingCar class and use that where this state of car matters. It's not as neat as ADT:s in ML but provide the same Lego-block static composability with minimum amount of moving parts. I would not use pattern matching as such in C++.
  - tel 12y ago
    Additionally, the Turing Tarpit doesn't apply in the level of the type language. These languages actually differ significantly in power since they're not Turing complete. Thus, there are certainly non-trivial and interesting static invariants which you can encode in Haskell and cannot in Java. The most critical and strong common one is probably parametricity.
    - lomnakkus 12y ago
      Oh, certainly. I was just alluding to the futility of the comparison :). Interestingly[1], the power of the type system seems to conflict somewhat with type inference. Or, at least, that a Turing Complete type-level language like in Shen or Idris does require you to spell out increasing amounts of type information. Obviously, this has to do with undecidability of TC languages, but I kind of think it's interesting that e.g. Haskell seems to occupy a kind of "sweet spot" in terms of inference and being able to tell the programmer when it needs a type ascription. AFAICT that would be impossible in a language whose type system is a-priory undecidable, correct? (Just to spell it out: In Haskell, the compiler knows that if you want feature X, Y and Z, then constructs A, B and C become undecidable... and can tell you so.) [1] Well, I found it interesting, but I'm a layman at best.
pjmlp 12y ago
Another thing is contract programming, but it is really hard to sell to managers where shipping cheap outweights quality. I don't envision FP or contract based programming in enterprise offshore code.
- codygman 12y ago
  Imagine a super-charged version of the method where Java Architects make class hierarchies and interfaces for offshore/contract programmers. I think FP (and contract based programming) would do a much better job than Java for varying qualities of programmers on very large projects.
marmaduke 12y ago
invariants could be lifted into the type system Is there a reason this is only possible in Haskell, or does Haskell just make it super convenient / idiomatic?
- pdpi 12y ago
  The way I see it, immutability and purity are hard requirements for actually enforcing the contract, and a very robust type system is then a requirement to go from code that makes you want to shoot yourself in the head, to code that's incredibly expressive and easy to reason about. Haskell just happens to sit in that exact niche.
  - marmaduke 12y ago
    immutability and purity are hard requirements I agree this is important. I have just started to move a project to Java from Python and see that immutability and purity are attainable for certain parts of the system but appear to cost a lot (leaning hard on use of interfaces, for example) in terms of readability.
- yummyfajitas 12y ago
  Haskell/Scala/etc makes it easy to nudge other developers into avoiding mistakes. A concrete example: I had a Scala system (build on Scalaz, which is a library providing Haskell for Scala), and one of our core types was DBTransaction[_] (a monad). A developer (a skeptic of the type system) was complaining to me about all the excess work he needed to go through, how he couldn't get properly construct a LazyStream[Foo] as a result of this. He wanted to construct a DBTransaction[LazyStream[Foo]], call runTransaction on it, and get the LazyStream[Foo] out. Then he was going to call f(lazyStream). The compiler just wouldn't allow this, so his "workaround" was to instead call lazyStream.map(f). Turns out this workaround prevented a runtime error. If he did get his LazyStream[Foo] out, generating the next element in the stream would have called resultSet.next() after closing the connection. This sort of thing happened quite often. People would complain that the type system made it harder for them to do what they wanted. They'd ask the FP "guru" types how to fix it and the "guru" would point out that what they wanted to do was fundamentally unsafe.

carterschonwald 12y ago

It might have to do with the way the default generics for aesons fromjson and tojson instances for record types are defined? Or maybe the lack of incremental streaming read write support in the aeson data model? Or maybe they wanted better date or integer support? It'd be pretty easy to ask don or Lennart I'd imagine. I have to say that I definitely enjoy using haskell when faced with dirty complicated data, which I'm told happens a lot in larger organizations.

eru 12y ago

> Monad stacks do wonders for circumscribing your computational context in an app. Wait until you discover the power of Applicative Functors. They are more restricted in their operations than Monads, so they compose better and allow for analysis.

davdar 12y ago
I'm curious, what do you mean they compose better and allow for analysis [better than monads]?
- gergoerdi 12y ago
  You can determine a lot more about a computation described only in terms of an applicative functor as you can from a monadic one, without running any of its effects (i.e. "statically"). It's easy to see why when you consider the opaqueness of the function in the right-hand side of a bind. Check out http://gergo.erdi.hu/blog/2012-12-01-static_analysis_with_applicatives/ http://gergo.erdi.hu/blog/2012-12-01-static_analysis_with_ap... for an example.
- tel 12y ago
  gergoerdi covered analysis, but composition is simple. For any two Applicatives F and G and value type A the following 4 values are all Applicative values F A G A F (G A) G (F A) But for monads only the first two are monads for general monads F and G. So, Applicatives compose better!
  - eru 12y ago
    And to get F (G A) with Monads, F needs to be a Monad transformer. In addition to composition, products of Applicatives are also Applicatives: (F A, G A)
    - tel 12y ago
      Even for monad transformers it's not necessarily the case that direct composition leads to a monad. For instance, ContT looks like newtype ContT r m a = ContT ((a -> m r) -> m r) so ContT M A is not the same as Cont (M A). Monads also compose under products as two parallel monadic computations data (f * g) a = Pair (f a) (g a) p1 :: (f * g) a -> f a p1 (Pair fa _) = fa p2 :: (f * g) a -> g a p2 (Pair _ ga) = ga instance (Monad f, Monad g) => Monad (f * g) where return a = Pair (return a) (return a) Pair fa ga >>= k = Pair (fa >>= p1 . k) (ga >>= p2 . k) You can also talk about composition under sums data (f + g) a = Inl (f a) | Inr (g a) and you'll get compositions of applicatives here so long as you have a notion of natural transformation class Natural f g where phi :: f a -> g a instance (Applicative f, Applicative g, Natural f g) => Applicative (f + g) where pure a = Inl (pure a) Inl ff <*> Inl fa = Inl ( ff <*> fa) Inr gf <*> Inr ga = Inr ( gf <*> ga) Inl ff <*> Inr ga = Inr (phi ff <*> ga) Inr gf <*> Inl fa = Inr ( gf <*> phi fa) but there's no way to get a similar monad. It turns out that you have to "know what branch to go down before you start" in exactly the kind of way applicatives allow and monad preclude.
dkarapetyan 12y ago
Mathematically speaking applicatives are less restrictive since more things can be applicatives than monads. A monad is a "very special" kind of functor and that is why a composition of monads often fails to satisfy the monad laws. The least restricted thing in this hierarchy is the functor since composition and other kinds of operations always give you back another functor.

fsloth 12y ago

A sidenote: There is nothing in Java/C++ etc that would stop one from making only legal states representable. It's just easier and more obvious in ML family...

lomnakkus 12y ago
That's only true in the most trivial Turing Tarpit sense, though. Ease of use and defaults matter in practice. E.g. you can do compile-time exhaustiveness-checked pattern matching using the visitor pattern in Java/C++, but try doing that in practice and the amount of boilerplate just becomes unbearable -- and actually obscures (rather than illuminate) the essence of the data structure. There's also the lack of higher-kinded types. (Or just plain syntactic pain of using HKTs e.g. in Scala.)
- fsloth 12y ago
  Very true. I usually avoid complex constructs in C++ - especially in production code and strive to strike a balance between KISS and YAGNI. KISS comes first unless there is some obvious boilerplate that can be avoided... Encoding only valid states in subareas of code can be done within C++ without extravagant constructs. Ie. instead of passing around a Car with a Car::isDriving member implement a DrivingCar class and use that where this state of car matters. It's not as neat as ADT:s in ML but provide the same Lego-block static composability with minimum amount of moving parts. I would not use pattern matching as such in C++.
- tel 12y ago
  Additionally, the Turing Tarpit doesn't apply in the level of the type language. These languages actually differ significantly in power since they're not Turing complete. Thus, there are certainly non-trivial and interesting static invariants which you can encode in Haskell and cannot in Java. The most critical and strong common one is probably parametricity.
  - lomnakkus 12y ago
    Oh, certainly. I was just alluding to the futility of the comparison :). Interestingly[1], the power of the type system seems to conflict somewhat with type inference. Or, at least, that a Turing Complete type-level language like in Shen or Idris does require you to spell out increasing amounts of type information. Obviously, this has to do with undecidability of TC languages, but I kind of think it's interesting that e.g. Haskell seems to occupy a kind of "sweet spot" in terms of inference and being able to tell the programmer when it needs a type ascription. AFAICT that would be impossible in a language whose type system is a-priory undecidable, correct? (Just to spell it out: In Haskell, the compiler knows that if you want feature X, Y and Z, then constructs A, B and C become undecidable... and can tell you so.) [1] Well, I found it interesting, but I'm a layman at best.

pjmlp 12y ago

Another thing is contract programming, but it is really hard to sell to managers where shipping cheap outweights quality. I don't envision FP or contract based programming in enterprise offshore code.

codygman 12y ago
Imagine a super-charged version of the method where Java Architects make class hierarchies and interfaces for offshore/contract programmers. I think FP (and contract based programming) would do a much better job than Java for varying qualities of programmers on very large projects.

marmaduke 12y ago

invariants could be lifted into the type system Is there a reason this is only possible in Haskell, or does Haskell just make it super convenient / idiomatic?

pdpi 12y ago
The way I see it, immutability and purity are hard requirements for actually enforcing the contract, and a very robust type system is then a requirement to go from code that makes you want to shoot yourself in the head, to code that's incredibly expressive and easy to reason about. Haskell just happens to sit in that exact niche.
- marmaduke 12y ago
  immutability and purity are hard requirements I agree this is important. I have just started to move a project to Java from Python and see that immutability and purity are attainable for certain parts of the system but appear to cost a lot (leaning hard on use of interfaces, for example) in terms of readability.
yummyfajitas 12y ago
Haskell/Scala/etc makes it easy to nudge other developers into avoiding mistakes. A concrete example: I had a Scala system (build on Scalaz, which is a library providing Haskell for Scala), and one of our core types was DBTransaction[_] (a monad). A developer (a skeptic of the type system) was complaining to me about all the excess work he needed to go through, how he couldn't get properly construct a LazyStream[Foo] as a result of this. He wanted to construct a DBTransaction[LazyStream[Foo]], call runTransaction on it, and get the LazyStream[Foo] out. Then he was going to call f(lazyStream). The compiler just wouldn't allow this, so his "workaround" was to instead call lazyStream.map(f). Turns out this workaround prevented a runtime error. If he did get his LazyStream[Foo] out, generating the next element in the stream would have called resultSet.next() after closing the connection. This sort of thing happened quite often. People would complain that the type system made it harder for them to do what they wanted. They'd ask the FP "guru" types how to fix it and the "guru" would point out that what they wanted to do was fundamentally unsafe.