Dependent Haskell

Actual article title: "Why Dependent Haskell is the Future of Software Development" - which the author spends a few handwavey paragraphs unconvincingly trying to show. After that, though, the article moves on to why to get there, and how to do so, both of which are more interesting than the attempt to justify the claim in the title.

I was almost 100% certain it was a joke until I read the paragraph that quote is from.

I want to reassure you that most Haskell evangelists (myself included) that say stuff like that usually mean it as a joke. Most people who seek to evangelize haskell do not lose sight of the fact that it's pretty daunting at first and has a relatively steep learning curve.

That said, Haskell is simple, but it's simple in an unintuitive way (as most other languages obscure the ideas). For example I'd argue that when people when people first hear "enum", what they really want is a sum type (i.e. `data Something = OneThing {...} | TheOther {...}`) and not what you get in most languages which is enums-that-are-just-named-numbers or enums-that-are-just-named-strings.

Most languages are coming around to the way haskell/other ML languages view the world however:

- non-nullable + option types - function composition (a bunch of languages get stuck in the filter/map phase but never get to the) - typeclasses + data types over classes + interfaces/abstract classes - pattern matching - Monads - The Free(R) Monad and attempts to make programs more like state machines and encode it at the type level

I'm probably preaching to the choir in this thread but Haskell's type system is like the mercedes of production-ready languages these days -- eventually the features trickle down to other languages. There are more advanced options out there like Idris (which already has good dependent type support) but it's going to take a while for any of them to get the support and ecosystem haskell fought hard for over all these years.

One highlight of Haskell's malleability and flexibility is the work around linear types in Haskell[0] -- they basically give you rust-like semantics (reference tracking for compile-time "automatic" memory management/etc) without having to rewrite haskell from scratch. Turns out you can classify rust's main feature under the super generic problem of "ascrib[ing] more precise types". Turns out with a good enough type system, and lots of patience/determination, you can solve a lot of common software issues at the type level.

As the famous saying goes, the future is here, it's just not evenly distributed.

[0]: https://ghc.haskell.org/trac/ghc/wiki/LinearTypes

Does anybody care to explain dependent types? I’ve heard the term used in FP conversations but not sure I get it.

> I think the large amount of effort the Rust community puts into explaining what they're doing with their type system, making it a first-class feature that's included in standard tutorials and having a lot of ergonomic effort put into error messages, is actually essential to making it work for ordinary users. (And even then, just barely; fighting the borrow checker is a thing.)

100% agree -- they've learned a lot from other languages and have padded their steep learning curve (due to the ownership/borrowing scheme and advanced type system), and it's done wonders for them. I spend a lot of my time these days trying to decide between Haskell and Rust for new projects, there are seemingly a lot of people in both camps that are freely moving between these two languages because of their similarities.

> A language that allows someone to build this as a library is much more scary. What other incomprehensible type hackery could someone do? Haskell can be fun but it's always going to look like a somewhat more practical research language to me.

I think it's a bit more than a library (many of the things in the original post and in linear types require deeper changes), and a ton of these features require extensions to GHC (via language extension pragmas in the source file), but I do agree, the type trickery involved is intense.

In my opinion type-level hackery in haskell is not the same as when you do crazy class hierarchies/patterns in other languages (let's say Java) -- for a few reasons:

- Haskell is pretty darn legible, for example, servant[0] is a library that lets you express an API as a type. It does a lot at the type level with advanced techniques, but here's an example of an API:

    type TodoAPI =
        "todos" :> Get '[JSON] [WithUUID Task]
        : "todos" :> Capture "uuid" UUID :> Get '[JSON] (WithUUID Task)
        : "todos" :> Capture "uuid" UUID :> ReqBody '[JSON] (Partial TaskF) :> Patch '[JSON] (WithUUID Task)
        : "todos" :> Capture "uuid" UUID :> Delete '[JSON] (WithUUID Task)
        : "todos" :> ReqBody '[JSON] Task :> Post '[JSON] (WithUUID Task)

Despite the fancy type level trickery that servant is doing under the covers this is impressively readable. In many instances the advanced type stuff (like `Partial t`, `WithUUID t`, `Capture "uuid" UUID`) actually helps the code be easier to understand, but doesn't detract from readability.

- You can step up the levels of expressiveness on your own terms -- the simpler way to write things is always right next to the more complicated way, and you can choose to push more into the type level when you choose. Example:

    data Task = Task { tName  :: TaskName
                     , tDesc  :: TaskDesc
                     , tState :: TaskStateValue
                     } deriving (Eq, Show, Read, Generic)

    -- the "f" below can be swapped for a polymoprhic type like "Maybe" or "Identity" (which is equal to itself)
    -- You can think about this by literally replacing the f with the word "Maybe" everywhere you see it in the below definition, it even makes sense in the semantic english sense.
    data TaskF f = TaskF { tfName  :: f TaskName
                         , tfDesc  :: f TaskDesc
                         , tfState :: f TaskStateValue
                         }

    data TaskFInState (state :: TaskState) f where
        FinishedT :: f TaskName -> f TaskDesc -> TaskFInState 'Finished f
        InProgressT :: f TaskName -> f TaskDesc -> TaskFInState 'InProgress f
        NotStartedT :: f TaskName -> f TaskDesc -> TaskFInState 'NotStarted f

        -- | The case where we don't know what the state actually is
        --   Ex. when we pull a value from the DB, we can't be polymorphic over state with the other constructors
        --   but the database *has* to know what was stored forthe state.
        -- Once we have an UnknownStateT we can write functions that try to translate to what we expect/require and fail otherwise.
        UnknownStateT :: f TaskName -> f TaskDesc -> f TaskStateValue -> TaskFInState state f

        -- | Similar case, but for when we need to fix the state type variable to *something*
        SomeStateT :: f TaskName -> f TaskDesc -> f TaskStateValue -> TaskFInState 'Some f

This code isn't the greatest but it's what I've been working with in a recent blog series with an in-depth guide to writing a simple rest-ish API. You can go from `Task` to `TaskF` to `TaskFInState` as you graduate, and even let these types go between each other and use the level that is required.

Want to write a function that only works on fully-specified Tasks that are in a very specific state? specialize the types! fore example: `cancelTask :: TaskFInState 'InProgress Identity -> TaskFInState 'NotStarted Identity`. Just reading this signature tells you important information about the function.

More on-topic, the "hello world" program for a dependently typed language is usually length-typed vectors (i.e. `Vector Int 5` to represent a list of ints with 5 elements) -- from my experience people start trying to get more sophisticated with types when they see cool advanced type trickery that they think would be useful, and start doing the reading/trudging uphill to figure it out. This probably is a bit difficult for new developers thrust into a codebase with tricks they don't understand, but again the legibility of haskell code and the clarity provided by type signatures and the syntax helps.

In a very abstract way, it is a way to encode relationships between types on the type system.

You can express things like how are you allowed to consume elements from a data structure, how many elements a specific data structure is allowed/expected to have, how their form looks like and so forth, all at compile time.

Thus working as kind of profs that certain functions can only be called if the conditions are met.

https://en.wikipedia.org/wiki/Type_system