13 ms·

I'm always curious what people are using the more exotic type system functionality of e.g. Haskell or Idris for in practice. It was interesting to hear that ev

I'm always curious what people are using the more exotic type system functionality of e.g. Haskell or Idris for in practice. It was interesting to hear that even Simon didn't expect such things to be used in industry quite yet. Still, I wish I could see more info on this. At what point does the additional cognitive burden of advanced type system features become a worthwhile tradeoff for program correctness? It seems to me that this depends wholly on the complexity of the program. Further to that point, the most complex programs I can think of (perhaps you may be able to offer other opinions, which I welcome) are AAA game engines. What are the reasons why the big engines out there are not using higher-kinded types, dependent types and the like? Is this just because of pragmatic issues such as the languages the developers learned in school not supporting these features, or because here-to-date functional languages supporting these features lacked the appropriate throughput of C/C++, where one can layout data for cache-efficiency?

Drup 8y ago
Well, the reason you gave are valid, but it also highly depends on the task at hand. You say AAA game engines are the most complex programs you can think of .... I raise you production-grade compilers, and those benefits enormously from complex type systems. Also, it's sometimes possible to use high-flying type trickeries in a local way that is not directly visible to the outside, but highly increase the safety inside a library. In all cases, Rust is probably the first language which both has a type system rich enough to start doing advanced type trickery and the capacity for fine-grained control over memory layout. I know they have a fairly vibrant gamedev community but I don't know the details. Do they use all the fancy things such as phantom types, complex traits, and all that?
- castle-bravo 8y ago
  What do you consider to be the minimum for advanced type trickery? I ask to see if Ada might fit that criteria and and what features it might be lacking that would make it competitive with Rust in the type-trickery domain.
  - Drup 8y ago
    As far as I'm concerned, the minimal is sum, products and, most importantly, abstract parametric datatypes. This is sufficient for phantom types, and then the fun starts. More complex parametric types (with ad-hoc polymorphism for example) then extends what you can do.
- chrisseaton 8y ago
  The most complex program I can think of surely has to be something like Facebook. It’s like a 4 GB executable isn’t it? I don’t think compilers are that large or complicated.
  - tomsmeding 8y ago
    The Facebook mobile application sure is large, but I wager lots of that is assets and repeated code. Even so, there is lots of code there anyway (someone dove into that at some point), but I think that's a "different kind" of complexity than, say, a compiler. There's lots of complex user interfaces to set up and work with, and there's some amount of user state to keep track of; but a compiler has to perform highly complicated operations on a large, intricate state that can often be described effectively with a strong type system. I'm inclined to believe a compiler is better suited for a type system like Haskell's than e.g. a mobile app or a game engine is, but maybe someone with more domain knowledge might correct me here.
  - oblio 8y ago
    I’d say Facebook is peanuts compared to the MS Office suite.
nightski 8y ago
AAA game engines could greatly benefit from the type systems. The problem is most (if not all to my knowledge) functional languages with advanced type systems require a garbage collector which is not ideal at all in that type of environment. They prefer the more deterministic latency provided by manual memory management.
- seanmcdirmid 8y ago
  Unity uses C# as its scripting language, Lua is popular as well. These all have GC.
  - deleted 8y ago
    [deleted]
  - cgh 8y ago
    My friends in game dev do not consider Unity to be a AAA game engine, not by a long stretch.
    - pjmlp 8y ago
      So given that, would they consider Unreal to be a AAA game engine?
      - nightski 8y ago
        Generally it's judged by the types of games which have been produced. Since Unreal has had AAA games released using it, then yes I'd say so.
        pjmlp 8y ago
        So then having a GC isn't an impediment to be a AAA games engine it seems.
        deleted 8y ago
        [deleted]
Kootle 8y ago
Haskell's type system works because of purity, and purity doesn't generally mesh well with performance-oriented applications like game engines. There are some type-driven approaches to gamedev, like https://github.com/jonascarpay/apecs https://github.com/jonascarpay/apecs, but it's fairly experimental. There has been some talk about linear types, which would allow Haskell to have controlled impurity similar to Rust, but they're still a ways off.
- wz1000 8y ago
  Linear types support is coming along nicely, there is a fork of GHC with a prototype implementation. https://github.com/tweag/ghc/tree/linear-types https://github.com/tweag/ghc/tree/linear-types However, to allow the compiler to optimise pure operations to impure ones, I don't think linear types are sufficient. You need something like uniqueness types.
  - btcindivist 8y ago
    I think C++ compiles down to a pure functional language that is then optimized into an efficient beast. So I'm not sure that pure code is hard to optimize.
    - seanmcdirmid 8y ago
      SSA is quite different from a pure FP; for example it doesn’t do anything about effects, it only gets rid of local imperative assignments that don’t really interfere with purity anyways.
    - tathougies 8y ago
      Most imperative languages have an intermediate language in which local variables are immutable. However, purity is about more than immutability. For example, in C++ x = doSomething(x) + 1 Can be written to not overwrite x int x2 = doSomething(x) + 1 This is equivalent in some ways to Haskell let x' = doSomething x + 1 However, I know that in Haskell, evaluating 'doSomething x' will not turn off the computer, display anything to the user, or launch missiles. I have no idea what evaluating 'doSomething(x)' does in C++. It may add things to caches, exit the program, etc.
danharaj 8y ago
> Still, I wish I could see more info on this. At what point does the additional cognitive burden of advanced type system features become a worthwhile tradeoff for program correctness? As a professional Haskell programmer, I find the cognitive burden to be lower in Haskell than in, say, Java, where I have to do a lot more bookkeeping about design patterns and how they're glued together than in standardish Haskell where compositional forms fall into a compact set of powerful concepts amenable to reasoning. I say standardish Haskell because the sweet spot in my experience is a few lightweight GHC extensions but mostly shunning some of the seriously experimental stuff in the language. For example, i agree with your doubt when it comes to dependent types and in particular singletons, a halfway house implementation that can be used in Haskell today. Some of my coworkers had unsuccessfully attempted to write mobile games in Haskell. That was 10 or so years ago and many of the technical hurdles that impeded them then are no longer there. The only major one I know of at the moment that prevents Haskell from being used in a AAA game engine is a guaranteed low latency garbage collector. I expect someone to implement such a thing for Haskell in the next 10 years. The space is moving fast, our understanding of how to write big Haskell apps has advanced drastically since when I first started using the language! I expect big things to come in the next couple of years. This is not to say that the space is getting rewritten all the time, it's just that more useful concepts are being discovered and matured. For example, Applicative only 11 years ago and scalable FRP like 4 years ago or so. I should say what type concepts compose my compact tool set: * higher order functions with syntax optimized for using them. * algebraic data types (sparingly generalized algebraic data types) * type classes + higher kinds (The synergy is far greater than the individual features) * monad transformers (the promise of aspect oriented programming actually realized)
- delhanty 8y ago
  Thank you - very useful summary. >I say standardish Haskell because the sweet spot in my experience is a few lightweight GHC extensions but mostly shunning some of the seriously experimental stuff in the language. Are you able to say which GHC extensions you use and why?
  - danharaj 8y ago
tathougies 8y ago
At my workplace, we use my database library [beam](https://github.com/tathougies/beam https://github.com/tathougies/beam) to make sure that our queries (written in a Haskell-like DSL) are runnable on the backends we choose. Also, I've found the cognitive burden to be significantly less using my beam library than writing SQL. The library handles everything. We freely join against queries (which may themselves be the results of joins, aggregates, window functions, etc). The SQL produced is what you'd expect. If you try to do something that is not straightforward on the backend, the library complains at compile time, and can even offer suggestions. We don't even need to worry about NULL, because the library makes heavy use of type families and such to guarantee you won't see a SQL NULL unless the type says so. If you use standard beam operators, we handle NULL sensibly. You can also drop to SQL NULL, if you want to have tighter control, but this causes the types to change, which means you can't do anything silly (like inadvertently throw out rows because your join condition now evaluates to NULL when you didn't want it to). Ultimately, using the type system is wonderful. Best of all, the types are mostly inferred. I rarely write out explicit type signatures. Despite the types carrying significant computation, all of that is given to us basically for free. Once we have linear types in GHC, the migrations system will be able to check that a migration script is valid from beginning to end before the migration is even run! There's no way you could do that with any current tool I know of. My guess for why big game engines aren't using higher-kinded types is that they are not available in any common systems level language. The only systems language I can think of with HKTs is ATS, which is a bit obtuse. W.r.t cache efficiency, I've been working on a library to exploit the Haskell recursion-schemes package to transparently store and read data in a cache-intelligent way. It's certainly possible to do, it's just not necessary for most of the kinds of programs Haskellers write. At my last workplace we used Haskell for protocol parsing, and we were able to parse gigabits per second using just the standard Haskell containers and such. Haskell is quite a fast language, if you use it correctly. You rarely need heavy optimizations. Although obviously for game engines, you probably would.
- icc97 8y ago
  > Also, I've found the cognitive burden to be significantly less using my beam library than writing SQL. I find this confusing. You still have all the cognitive burden to figure out what SQL you want to write, but then you have to translate that SQL into Haskell (or any other ORM).
evincarofautumn 8y ago
I think this quote from the article alludes to an answer: “Somehow, the level of abstraction offered by a sophisticated type system lets you get much more ambitious in terms of the intellectual complexity of what you can deal with.” When you have a notation well suited for using these advanced features, all of a sudden they become tractable to reason about. The languages in which AAA game engines are written have notations and semantics that are not well suited to these abstractions; and people continue to use them because they have reputations for efficiency and control that functional languages historically do not. But that’s changing with the advent of languages like Rust and ATS that bring more of the power of functional programming and advanced type system features to bear on low-level efficient code without the need for a GC. (I’m also working on such a language.) What I’m getting at is that there are some things I do all the time in Haskell because it’s easy, which I don’t do in other languages becuase it’s hard. I know in principle how to get the same guarantees in other languages, but the expressiveness isn’t there: the encoding in the syntax & semantics of those languages is so unwieldy that I rarely bother. Take for example something simple like algebraic data types and pattern matching. You can encode sum types with only product types (tuples/records) and functions using Boehm-Berarducci encoding, which in OOP languages is called the visitor pattern. But it takes so much more code that I often design things entirely differently to avoid it. In Haskell I use higher-kinded polymorphism all the time—abstracting over type constructors. That’s possible to encode in C++ with template template parameters, but it’s incredibly unwieldy, produces awful error messages when you do it wrong, and can be invasive depending on what features you need to support. I use GADTs, existential types, and higher-rank polymorphism all the time, for example, passing generic functions as arguments to other functions. That’s possible to encode in OOP languages using interfaces with generic methods, but it can’t be done inline, requiring a couple of helper types and moving the “meat” of an implementation away from the actual method being defined; in Haskell I just add a “forall” with the scope I want. So I don’t think it depends on the complexity of the program so much as the complexity of the encoding in your language of choice. It’s eminently possible to take advantage of these features in C++, Java, C#, &c. to enforce better program correctness and even gain better performance, but the “wizardry” required is not accessible to the majority of users. Whereas in Haskell, sooner or later just about everyone gains some experience with type-level programming that would be possible but prohibitively difficult to do in other languages, because Haskell was designed to support those abstractions—whether through built-in concepts, extensions, or clever combinations of orthogonal and expressive language features.
erikpukinskis 8y ago
There’s an interesting relationship too: The more advanced your programming tools are, the more complex your code can get before you hit your limit and need to refactor. It’s great up til that point, but once you cross the line you are in mind melting territory. I code in a tiny subset of JavaScript, wrap at 40 character width, without allowing any build tools, and only single-file repos. This probably seems insane to most, but it has a powerful effect: Complexity becomes painful very fast, and so I am forced to refactor aggressively, which causes me to put more effort into good separation of concerns earlier in my implementation process. It’s not for everyone, but if you enjoy the discovery of medium-sized single purpose modules, I would encourage you to try this, in your language of choice. Just pick a small set of native primitives and stick to them, and libraries written in (close to) the same subset. As a side note: Some people might be thinking, “huh? Rich type systems and control structures HELP you write single purpose code with clear boundaries.” To which I agree. But I said “medium sized”. Rich toolsets will push you towards a combination of very small and very large API surfaces: small modules that do one arcane abstract thing that has no immmediate value, and then a huge surface which is the entire set of all of those small modules. Modular subset programming makes both small and large modules awkward... small modules are awkward because you need to include them over and over. Large modules are awkward. It squeezes you from both sides into finding concerns that are good brain-sized nuggets.
- kqr 8y ago
  > I code in a tiny subset of JavaScript, wrap at 40 character width, without allowing any build tools, and only single-file repos. This probably seems insane to most, but it has a powerful effect: Complexity becomes painful very fast, and so I am forced to refactor aggressively, which causes me to put more effort into good separation of concerns earlier in my implementation process. I like this idea! I've sort of gravitated toward it myself -- inspired by the exceedingly clear pieces of code that can be found in older books on programming -- but I have yet to make it an expölicit purpose of mine. I may want to try that!
- flukus 8y ago
  It actually sounds incredibly sane to me right now, I just finished a task to extend some existing code to read an extra field from a CSV. I had to touch 9 files to do this. Strict typing (c#) helped, but it's only necessary because things were so over complicated in the first place. On this project in particular there are tens of thousands of LOC, about 50 csproj files, unit tests, our own regex implementation a plugin framework and dll dependencies from half a dozen other projects. But when you step back from all that and look at what the project really does it's just taking various files and stuffing them into a database. It really could have been done with about 30 isolated 20 line bash scripts. The biggest enemy in our line of work is the complexity we create for ourselves.
deleted 8y ago
[deleted]
cstrahan 8y ago
> At what point does the additional cognitive burden of advanced type system features become a worthwhile tradeoff for program correctness? It seems to me that this depends wholly on the complexity of the program. I have similar thoughts as those expressed by the sibling post by danharaj (ohai Dan!), but I'd like to stress a particular point: the type system lowers the cognitive burden, rather than increase it. By way of analogy, think of it this way: spoken languages are quite complex; you have all sorts of stuff to get right: * conjugation * noun genders * tenses * participles * prepositions * etc, etc, etc... And there are all sorts of fun, intricate grammatical rules that govern which words are supposed to go where. That's a ton of work! Now, one could argue: wouldn't it be much easier if we just, you know, made the language simpler? The problem is that each of these things serves some purpose (well, mostly, anyway -- dunno how I feel about, say, gendered nouns); for example, if we stripped away the ability to convey tense, the language would become simpler, but it would lose out on some important expressive power. While we're at it, we could also shorten the vocabulary. Picking an arbitrary number, let's say we keep only the top 100 words. That'll probably capture most of the essentials, if what is "essential" is "that which ensures you get your basic needs for survival". But let's say "love" wasn't in that top 100: how would you tell someone that you love them? That's no problem: whenever we want to tell someone we love them, we can unpack the definition: love: a gentle feeling of fondness or liking Uh-oh -- "gentle" and "fondness" didn't make the cut... I suppose we'll unpack those definitions as well. So now we have: love: a (mild in temperament or behavior; kind or tender) feeling of (affection or liking for someone or something) or liking Oh hell, temperament certainly isn't in the top 100, so here we go again: love: a (mild in (a person's or animal's nature, especially as it permanently affects their behavior) or behavior; kind or tender) feeling of (affection or liking for someone or something) or liking So ... ... yeah, that got out of hand pretty quickly, and we still have a ways to go. The next time you tell someone you love them, think about how incredible it is that you have a word at your disposal that immediately conveys something so nuanced. Think of all the meaning that's cram-packed into that one word. And it's only one syllable! So how does this exercise relate back to more advanced type systems? A sophisticated type system (like Haskell's) allows me think (and express) thoughts that I otherwise wouldn't be able to. I mean, with inordinate amounts of effort (kind of like the effort I would need to keep the whole, fully unpacked definition of "love" in my head all at once), I might be able to do everything I was able to do before -- it would just make things more difficult, and it wouldn't be practical. Programming in weaker languages (e.g. Java, Go) often feels like trying to tell someone something as seemingly simple as "I love you", but all I have at my disposal is the ability to grunt and flail my arms around -- that's a simpler system, but man is it a lot of work.
nnq 8y ago
> AAA game engines I think most game programmers have a typical "incremental" mentality, where they need to see progress all the way, even at the learning the language stage. And then studios want easily replaceable programmers. So by this point you'd probably be left with few ideal languages: Java or C#. Add the constraint of low level optimizations for performance combined with "zero cost abstractions" so that in theory you can keeps a decent amount of productivity while working with heavily optimized code. So you're left at... C++ Nothing else gets even close to fitting the requirements. I imagine that if Rust gets popular enough to satisfy the "easily replaceable programmers" imaginary requirement (because I imagine it never works), you'll start seeing game engins written in Rust. To be honest, I think Rust will never get very popular because it will tend to have a huuuge gap between "library creators" (that will use the full feature set of the language, understand all the lifetimes tricks, never use garbage collection etc.) and the "library consumers", so people will keep being afraid of popping off the hood. I'd have more hopes with someone creating some kind of "superset of Go" as a next systems language, that would add something like generics, local type inference, and a way to turn off GC. The lowest common denominator always wins, "worse is better" and all that...
imh 8y ago
The cheeky answer is what I most miss during my day job (python). The more I can assert at compile time, the easier refactoring is. That's what I miss most. In Haskell, you have a great range of how much you want to do at the type level, and I miss that flexibility greatly at work.
quickthrower2 8y ago
A big shout here for Elm. Compared to Haskell it has fewer features and is much simpler. Think of it as kind of a subset, but with nicer record syntax and error messages, and tightly coupled to the web. The upside is you can learn it quick and understand other people's code easily. This makes it more fun to use and feel more productive. There is also a different culture - in Haskell things like template Haskell and Lenses are fairly widely used, but although you can in theory do some Lens stuff in Elm, no one actually does. To give you an idea, as a beginner your introduction to Lenses is this beast http://i.imgur.com/ALlbPRa.png http://i.imgur.com/ALlbPRa.png. So that's probably an entire weekend to get your head around. (Big respect to Edward Knett though for creating this and dozens of other libraries) You can get your head around all of Elm in that time. The downside is that you end up with more boilerplate than Haskell. For example there is no monad typeclass, so you have multiple definitions of "andThen" whereas Haskell you can always reach for the generic >>= I'm working on a side project and having a lot of fun in Elm
thesz 8y ago
I used pretty advanced type system features to support better hardware description language. for example, I had to provide length of bit vectors in the type system and account for compatibility of concatenation of two bit vectors and bit vector with the length of the sum of their lengths. That required implementing arithmetic in the type system. I also strictly required that arithmetic and most other operations require length equality. E.g., you should not be able to compare for equality single bit and bit vector of length 10, as it is possible in C and Verilog. This thing alone proved very effective in reducing errors in the code. The operations that cross clock domains are also prohibited, etc. The problem with hardware is that it is really hard to change once you "compiled" it. So you have to plan to get rid of errors early, without too much testing. The problem with AAA games is their budget - you can throw many people at finding bugs by testing (playing and replaying). So you do not need a tool that allows you to get rid of as many bugs as possible as early as possible. The process employed in AAA games development ensures that there will be not many bugs in the end. It is just that process is different than, say, one in hardware development.
lmm 8y ago
> Still, I wish I could see more info on this. At what point does the additional cognitive burden of advanced type system features become a worthwhile tradeoff for program correctness? It seems to me that this depends wholly on the complexity of the program. I think that's a false equivalence, because there's only a burden if you're doing something complex. Indeed short scripts can see a lot of benefit from using an advanced type system, since they tend to have interacting effects that can easily lead to misbehaviour if uncontrolled. > Further to that point, the most complex programs I can think of (perhaps you may be able to offer other opinions, which I welcome) are AAA game engines. What are the reasons why the big engines out there are not using higher-kinded types, dependent types and the like? My experience of the games industry is that it's full of young developers with a macho performance culture (I appreciate that this doesn't match everyone's experiences). "We're adopting a tool that will help us make fewer mistakes" is a tough sell in any segment of the software industry - it requires a mature culture to get beyond the "just write better code" response - but particularly so in games.
CMCDragonkai 8y ago
Having the type system match the domain model of your code immensely reduces the cognitive burden compared to untyped languages. You can just trust the types and trust purity and carry on. On the other end of the spectrum is where someone goes and creates complex type wizardry which can be overkill, or if they modeled thr problem incorrectly then it can become a ball and chain.
georgewsinger 8y ago
An example of real-world Haskell use: https://github.com/SimulaVR/Simula https://github.com/SimulaVR/Simula SimulaVR is a 3D window manager (under active development) for VR Linux Desktop.

Drup 8y ago

Well, the reason you gave are valid, but it also highly depends on the task at hand. You say AAA game engines are the most complex programs you can think of .... I raise you production-grade compilers, and those benefits enormously from complex type systems. Also, it's sometimes possible to use high-flying type trickeries in a local way that is not directly visible to the outside, but highly increase the safety inside a library. In all cases, Rust is probably the first language which both has a type system rich enough to start doing advanced type trickery and the capacity for fine-grained control over memory layout. I know they have a fairly vibrant gamedev community but I don't know the details. Do they use all the fancy things such as phantom types, complex traits, and all that?

castle-bravo 8y ago
What do you consider to be the minimum for advanced type trickery? I ask to see if Ada might fit that criteria and and what features it might be lacking that would make it competitive with Rust in the type-trickery domain.
- Drup 8y ago
  As far as I'm concerned, the minimal is sum, products and, most importantly, abstract parametric datatypes. This is sufficient for phantom types, and then the fun starts. More complex parametric types (with ad-hoc polymorphism for example) then extends what you can do.
chrisseaton 8y ago
The most complex program I can think of surely has to be something like Facebook. It’s like a 4 GB executable isn’t it? I don’t think compilers are that large or complicated.
- tomsmeding 8y ago
  The Facebook mobile application sure is large, but I wager lots of that is assets and repeated code. Even so, there is lots of code there anyway (someone dove into that at some point), but I think that's a "different kind" of complexity than, say, a compiler. There's lots of complex user interfaces to set up and work with, and there's some amount of user state to keep track of; but a compiler has to perform highly complicated operations on a large, intricate state that can often be described effectively with a strong type system. I'm inclined to believe a compiler is better suited for a type system like Haskell's than e.g. a mobile app or a game engine is, but maybe someone with more domain knowledge might correct me here.
- oblio 8y ago
  I’d say Facebook is peanuts compared to the MS Office suite.

nightski 8y ago

AAA game engines could greatly benefit from the type systems. The problem is most (if not all to my knowledge) functional languages with advanced type systems require a garbage collector which is not ideal at all in that type of environment. They prefer the more deterministic latency provided by manual memory management.

seanmcdirmid 8y ago
Unity uses C# as its scripting language, Lua is popular as well. These all have GC.
- deleted 8y ago
  [deleted]
- cgh 8y ago
  My friends in game dev do not consider Unity to be a AAA game engine, not by a long stretch.
  - pjmlp 8y ago
    So given that, would they consider Unreal to be a AAA game engine?
    - nightski 8y ago
      Generally it's judged by the types of games which have been produced. Since Unreal has had AAA games released using it, then yes I'd say so.
      - pjmlp 8y ago
        So then having a GC isn't an impediment to be a AAA games engine it seems.
        deleted 8y ago
        [deleted]

Kootle 8y ago

Haskell's type system works because of purity, and purity doesn't generally mesh well with performance-oriented applications like game engines. There are some type-driven approaches to gamedev, like https://github.com/jonascarpay/apecs https://github.com/jonascarpay/apecs, but it's fairly experimental. There has been some talk about linear types, which would allow Haskell to have controlled impurity similar to Rust, but they're still a ways off.

wz1000 8y ago
Linear types support is coming along nicely, there is a fork of GHC with a prototype implementation. https://github.com/tweag/ghc/tree/linear-types https://github.com/tweag/ghc/tree/linear-types However, to allow the compiler to optimise pure operations to impure ones, I don't think linear types are sufficient. You need something like uniqueness types.
- btcindivist 8y ago
  I think C++ compiles down to a pure functional language that is then optimized into an efficient beast. So I'm not sure that pure code is hard to optimize.
  - seanmcdirmid 8y ago
    SSA is quite different from a pure FP; for example it doesn’t do anything about effects, it only gets rid of local imperative assignments that don’t really interfere with purity anyways.
  - tathougies 8y ago
    Most imperative languages have an intermediate language in which local variables are immutable. However, purity is about more than immutability. For example, in C++ x = doSomething(x) + 1 Can be written to not overwrite x int x2 = doSomething(x) + 1 This is equivalent in some ways to Haskell let x' = doSomething x + 1 However, I know that in Haskell, evaluating 'doSomething x' will not turn off the computer, display anything to the user, or launch missiles. I have no idea what evaluating 'doSomething(x)' does in C++. It may add things to caches, exit the program, etc.

danharaj 8y ago

> Still, I wish I could see more info on this. At what point does the additional cognitive burden of advanced type system features become a worthwhile tradeoff for program correctness? As a professional Haskell programmer, I find the cognitive burden to be lower in Haskell than in, say, Java, where I have to do a lot more bookkeeping about design patterns and how they're glued together than in standardish Haskell where compositional forms fall into a compact set of powerful concepts amenable to reasoning. I say standardish Haskell because the sweet spot in my experience is a few lightweight GHC extensions but mostly shunning some of the seriously experimental stuff in the language. For example, i agree with your doubt when it comes to dependent types and in particular singletons, a halfway house implementation that can be used in Haskell today. Some of my coworkers had unsuccessfully attempted to write mobile games in Haskell. That was 10 or so years ago and many of the technical hurdles that impeded them then are no longer there. The only major one I know of at the moment that prevents Haskell from being used in a AAA game engine is a guaranteed low latency garbage collector. I expect someone to implement such a thing for Haskell in the next 10 years. The space is moving fast, our understanding of how to write big Haskell apps has advanced drastically since when I first started using the language! I expect big things to come in the next couple of years. This is not to say that the space is getting rewritten all the time, it's just that more useful concepts are being discovered and matured. For example, Applicative only 11 years ago and scalable FRP like 4 years ago or so. I should say what type concepts compose my compact tool set: * higher order functions with syntax optimized for using them. * algebraic data types (sparingly generalized algebraic data types) * type classes + higher kinds (The synergy is far greater than the individual features) * monad transformers (the promise of aspect oriented programming actually realized)

delhanty 8y ago
Thank you - very useful summary. >I say standardish Haskell because the sweet spot in my experience is a few lightweight GHC extensions but mostly shunning some of the seriously experimental stuff in the language. Are you able to say which GHC extensions you use and why?
- danharaj 8y ago

tathougies 8y ago

At my workplace, we use my database library [beam](https://github.com/tathougies/beam https://github.com/tathougies/beam) to make sure that our queries (written in a Haskell-like DSL) are runnable on the backends we choose. Also, I've found the cognitive burden to be significantly less using my beam library than writing SQL. The library handles everything. We freely join against queries (which may themselves be the results of joins, aggregates, window functions, etc). The SQL produced is what you'd expect. If you try to do something that is not straightforward on the backend, the library complains at compile time, and can even offer suggestions. We don't even need to worry about NULL, because the library makes heavy use of type families and such to guarantee you won't see a SQL NULL unless the type says so. If you use standard beam operators, we handle NULL sensibly. You can also drop to SQL NULL, if you want to have tighter control, but this causes the types to change, which means you can't do anything silly (like inadvertently throw out rows because your join condition now evaluates to NULL when you didn't want it to). Ultimately, using the type system is wonderful. Best of all, the types are mostly inferred. I rarely write out explicit type signatures. Despite the types carrying significant computation, all of that is given to us basically for free. Once we have linear types in GHC, the migrations system will be able to check that a migration script is valid from beginning to end before the migration is even run! There's no way you could do that with any current tool I know of. My guess for why big game engines aren't using higher-kinded types is that they are not available in any common systems level language. The only systems language I can think of with HKTs is ATS, which is a bit obtuse. W.r.t cache efficiency, I've been working on a library to exploit the Haskell recursion-schemes package to transparently store and read data in a cache-intelligent way. It's certainly possible to do, it's just not necessary for most of the kinds of programs Haskellers write. At my last workplace we used Haskell for protocol parsing, and we were able to parse gigabits per second using just the standard Haskell containers and such. Haskell is quite a fast language, if you use it correctly. You rarely need heavy optimizations. Although obviously for game engines, you probably would.

icc97 8y ago
> Also, I've found the cognitive burden to be significantly less using my beam library than writing SQL. I find this confusing. You still have all the cognitive burden to figure out what SQL you want to write, but then you have to translate that SQL into Haskell (or any other ORM).

evincarofautumn 8y ago

I think this quote from the article alludes to an answer: “Somehow, the level of abstraction offered by a sophisticated type system lets you get much more ambitious in terms of the intellectual complexity of what you can deal with.” When you have a notation well suited for using these advanced features, all of a sudden they become tractable to reason about. The languages in which AAA game engines are written have notations and semantics that are not well suited to these abstractions; and people continue to use them because they have reputations for efficiency and control that functional languages historically do not. But that’s changing with the advent of languages like Rust and ATS that bring more of the power of functional programming and advanced type system features to bear on low-level efficient code without the need for a GC. (I’m also working on such a language.) What I’m getting at is that there are some things I do all the time in Haskell because it’s easy, which I don’t do in other languages becuase it’s hard. I know in principle how to get the same guarantees in other languages, but the expressiveness isn’t there: the encoding in the syntax & semantics of those languages is so unwieldy that I rarely bother. Take for example something simple like algebraic data types and pattern matching. You can encode sum types with only product types (tuples/records) and functions using Boehm-Berarducci encoding, which in OOP languages is called the visitor pattern. But it takes so much more code that I often design things entirely differently to avoid it. In Haskell I use higher-kinded polymorphism all the time—abstracting over type constructors. That’s possible to encode in C++ with template template parameters, but it’s incredibly unwieldy, produces awful error messages when you do it wrong, and can be invasive depending on what features you need to support. I use GADTs, existential types, and higher-rank polymorphism all the time, for example, passing generic functions as arguments to other functions. That’s possible to encode in OOP languages using interfaces with generic methods, but it can’t be done inline, requiring a couple of helper types and moving the “meat” of an implementation away from the actual method being defined; in Haskell I just add a “forall” with the scope I want. So I don’t think it depends on the complexity of the program so much as the complexity of the encoding in your language of choice. It’s eminently possible to take advantage of these features in C++, Java, C#, &c. to enforce better program correctness and even gain better performance, but the “wizardry” required is not accessible to the majority of users. Whereas in Haskell, sooner or later just about everyone gains some experience with type-level programming that would be possible but prohibitively difficult to do in other languages, because Haskell was designed to support those abstractions—whether through built-in concepts, extensions, or clever combinations of orthogonal and expressive language features.

erikpukinskis 8y ago

There’s an interesting relationship too: The more advanced your programming tools are, the more complex your code can get before you hit your limit and need to refactor. It’s great up til that point, but once you cross the line you are in mind melting territory. I code in a tiny subset of JavaScript, wrap at 40 character width, without allowing any build tools, and only single-file repos. This probably seems insane to most, but it has a powerful effect: Complexity becomes painful very fast, and so I am forced to refactor aggressively, which causes me to put more effort into good separation of concerns earlier in my implementation process. It’s not for everyone, but if you enjoy the discovery of medium-sized single purpose modules, I would encourage you to try this, in your language of choice. Just pick a small set of native primitives and stick to them, and libraries written in (close to) the same subset. As a side note: Some people might be thinking, “huh? Rich type systems and control structures HELP you write single purpose code with clear boundaries.” To which I agree. But I said “medium sized”. Rich toolsets will push you towards a combination of very small and very large API surfaces: small modules that do one arcane abstract thing that has no immmediate value, and then a huge surface which is the entire set of all of those small modules. Modular subset programming makes both small and large modules awkward... small modules are awkward because you need to include them over and over. Large modules are awkward. It squeezes you from both sides into finding concerns that are good brain-sized nuggets.

kqr 8y ago
> I code in a tiny subset of JavaScript, wrap at 40 character width, without allowing any build tools, and only single-file repos. This probably seems insane to most, but it has a powerful effect: Complexity becomes painful very fast, and so I am forced to refactor aggressively, which causes me to put more effort into good separation of concerns earlier in my implementation process. I like this idea! I've sort of gravitated toward it myself -- inspired by the exceedingly clear pieces of code that can be found in older books on programming -- but I have yet to make it an expölicit purpose of mine. I may want to try that!
flukus 8y ago
It actually sounds incredibly sane to me right now, I just finished a task to extend some existing code to read an extra field from a CSV. I had to touch 9 files to do this. Strict typing (c#) helped, but it's only necessary because things were so over complicated in the first place. On this project in particular there are tens of thousands of LOC, about 50 csproj files, unit tests, our own regex implementation a plugin framework and dll dependencies from half a dozen other projects. But when you step back from all that and look at what the project really does it's just taking various files and stuffing them into a database. It really could have been done with about 30 isolated 20 line bash scripts. The biggest enemy in our line of work is the complexity we create for ourselves.

deleted 8y ago

[deleted]

cstrahan 8y ago

> At what point does the additional cognitive burden of advanced type system features become a worthwhile tradeoff for program correctness? It seems to me that this depends wholly on the complexity of the program. I have similar thoughts as those expressed by the sibling post by danharaj (ohai Dan!), but I'd like to stress a particular point: the type system lowers the cognitive burden, rather than increase it. By way of analogy, think of it this way: spoken languages are quite complex; you have all sorts of stuff to get right: * conjugation * noun genders * tenses * participles * prepositions * etc, etc, etc... And there are all sorts of fun, intricate grammatical rules that govern which words are supposed to go where. That's a ton of work! Now, one could argue: wouldn't it be much easier if we just, you know, made the language simpler? The problem is that each of these things serves some purpose (well, mostly, anyway -- dunno how I feel about, say, gendered nouns); for example, if we stripped away the ability to convey tense, the language would become simpler, but it would lose out on some important expressive power. While we're at it, we could also shorten the vocabulary. Picking an arbitrary number, let's say we keep only the top 100 words. That'll probably capture most of the essentials, if what is "essential" is "that which ensures you get your basic needs for survival". But let's say "love" wasn't in that top 100: how would you tell someone that you love them? That's no problem: whenever we want to tell someone we love them, we can unpack the definition: love: a gentle feeling of fondness or liking Uh-oh -- "gentle" and "fondness" didn't make the cut... I suppose we'll unpack those definitions as well. So now we have: love: a (mild in temperament or behavior; kind or tender) feeling of (affection or liking for someone or something) or liking Oh hell, temperament certainly isn't in the top 100, so here we go again: love: a (mild in (a person's or animal's nature, especially as it permanently affects their behavior) or behavior; kind or tender) feeling of (affection or liking for someone or something) or liking So ... ... yeah, that got out of hand pretty quickly, and we still have a ways to go. The next time you tell someone you love them, think about how incredible it is that you have a word at your disposal that immediately conveys something so nuanced. Think of all the meaning that's cram-packed into that one word. And it's only one syllable! So how does this exercise relate back to more advanced type systems? A sophisticated type system (like Haskell's) allows me think (and express) thoughts that I otherwise wouldn't be able to. I mean, with inordinate amounts of effort (kind of like the effort I would need to keep the whole, fully unpacked definition of "love" in my head all at once), I might be able to do everything I was able to do before -- it would just make things more difficult, and it wouldn't be practical. Programming in weaker languages (e.g. Java, Go) often feels like trying to tell someone something as seemingly simple as "I love you", but all I have at my disposal is the ability to grunt and flail my arms around -- that's a simpler system, but man is it a lot of work.

nnq 8y ago

> AAA game engines I think most game programmers have a typical "incremental" mentality, where they need to see progress all the way, even at the learning the language stage. And then studios want easily replaceable programmers. So by this point you'd probably be left with few ideal languages: Java or C#. Add the constraint of low level optimizations for performance combined with "zero cost abstractions" so that in theory you can keeps a decent amount of productivity while working with heavily optimized code. So you're left at... C++ Nothing else gets even close to fitting the requirements. I imagine that if Rust gets popular enough to satisfy the "easily replaceable programmers" imaginary requirement (because I imagine it never works), you'll start seeing game engins written in Rust. To be honest, I think Rust will never get very popular because it will tend to have a huuuge gap between "library creators" (that will use the full feature set of the language, understand all the lifetimes tricks, never use garbage collection etc.) and the "library consumers", so people will keep being afraid of popping off the hood. I'd have more hopes with someone creating some kind of "superset of Go" as a next systems language, that would add something like generics, local type inference, and a way to turn off GC. The lowest common denominator always wins, "worse is better" and all that...

imh 8y ago

The cheeky answer is what I most miss during my day job (python). The more I can assert at compile time, the easier refactoring is. That's what I miss most. In Haskell, you have a great range of how much you want to do at the type level, and I miss that flexibility greatly at work.

quickthrower2 8y ago

A big shout here for Elm. Compared to Haskell it has fewer features and is much simpler. Think of it as kind of a subset, but with nicer record syntax and error messages, and tightly coupled to the web. The upside is you can learn it quick and understand other people's code easily. This makes it more fun to use and feel more productive. There is also a different culture - in Haskell things like template Haskell and Lenses are fairly widely used, but although you can in theory do some Lens stuff in Elm, no one actually does. To give you an idea, as a beginner your introduction to Lenses is this beast http://i.imgur.com/ALlbPRa.png http://i.imgur.com/ALlbPRa.png. So that's probably an entire weekend to get your head around. (Big respect to Edward Knett though for creating this and dozens of other libraries) You can get your head around all of Elm in that time. The downside is that you end up with more boilerplate than Haskell. For example there is no monad typeclass, so you have multiple definitions of "andThen" whereas Haskell you can always reach for the generic >>= I'm working on a side project and having a lot of fun in Elm

thesz 8y ago

I used pretty advanced type system features to support better hardware description language. for example, I had to provide length of bit vectors in the type system and account for compatibility of concatenation of two bit vectors and bit vector with the length of the sum of their lengths. That required implementing arithmetic in the type system. I also strictly required that arithmetic and most other operations require length equality. E.g., you should not be able to compare for equality single bit and bit vector of length 10, as it is possible in C and Verilog. This thing alone proved very effective in reducing errors in the code. The operations that cross clock domains are also prohibited, etc. The problem with hardware is that it is really hard to change once you "compiled" it. So you have to plan to get rid of errors early, without too much testing. The problem with AAA games is their budget - you can throw many people at finding bugs by testing (playing and replaying). So you do not need a tool that allows you to get rid of as many bugs as possible as early as possible. The process employed in AAA games development ensures that there will be not many bugs in the end. It is just that process is different than, say, one in hardware development.

lmm 8y ago

> Still, I wish I could see more info on this. At what point does the additional cognitive burden of advanced type system features become a worthwhile tradeoff for program correctness? It seems to me that this depends wholly on the complexity of the program. I think that's a false equivalence, because there's only a burden if you're doing something complex. Indeed short scripts can see a lot of benefit from using an advanced type system, since they tend to have interacting effects that can easily lead to misbehaviour if uncontrolled. > Further to that point, the most complex programs I can think of (perhaps you may be able to offer other opinions, which I welcome) are AAA game engines. What are the reasons why the big engines out there are not using higher-kinded types, dependent types and the like? My experience of the games industry is that it's full of young developers with a macho performance culture (I appreciate that this doesn't match everyone's experiences). "We're adopting a tool that will help us make fewer mistakes" is a tough sell in any segment of the software industry - it requires a mature culture to get beyond the "just write better code" response - but particularly so in games.

CMCDragonkai 8y ago

Having the type system match the domain model of your code immensely reduces the cognitive burden compared to untyped languages. You can just trust the types and trust purity and carry on. On the other end of the spectrum is where someone goes and creates complex type wizardry which can be overkill, or if they modeled thr problem incorrectly then it can become a ball and chain.

georgewsinger 8y ago

An example of real-world Haskell use: https://github.com/SimulaVR/Simula https://github.com/SimulaVR/Simula SimulaVR is a 3D window manager (under active development) for VR Linux Desktop.