169

I have seen several sources echo the opinion that "Haskell is gradually becoming a dependently-typed language". The implication seems to be that with more and more language extensions, Haskell is drifting in that general direction, but isn't there yet.

There are basically two things I would like to know. The first is, quite simply, what does "being a dependently-typed language" actually mean? (Hopefully without being too technical about it.)

The second question is... what's the drawback? I mean, people know we're heading that way, so there must be some advantage to it. And yet, we're not there yet, so there must be some downside stopping people going all the way. I get the impression that the problem is a steep increase in complexity. But, not really understanding what dependent typing is, I don't know for sure.

What I do know is that every time I start reading about a dependently-typed programming language, the text is utterly incomprehensible... Presumably that's the problem. (?)

6
  • 10
    Put simply, you can write types that depend on terms (calculations). This is enough to specify types about every aspect of your program, and therefore means the type system is capable of full program specification. The problem is that because the types depend on calculations, type checking is vastly more difficult to do (impossible in general).
    – GManNickG
    Oct 18, 2012 at 19:06
  • 28
    @GManNickG: Type checking is entirely possible. Type inference is another matter, but then again GHC's various extensions have long since abandoned the idea that it should be possible to infer all types. Oct 18, 2012 at 19:21
  • 8
    If I understand correctly, the drawback is that doing dependent typing right (e.g., in a way which is both usable and well-founded) is hard, and we don't know how quite yet. Oct 18, 2012 at 20:06
  • 4
    I don't think anyone's pointed out the one big pragmatic drawback: writing proofs that all of your code is correct is pretty insanely tedious. Because you can't automatically do type inference (corresponds to theorem proving in a "hella powerful" logic), you have to write annotations for your program in the form of proofs. This obviously gets annoying and hard to do after a while, especially for the more elaborate monadic magic that people typically do in Haskell. The closest that we're coming these days is languages that do most of this for us or give us a good set of primitives. Oct 25, 2012 at 6:36
  • I had assumed that dependent types were a "solved problem" and that Haskell was simply shying away from going full-out because of historical reasons, or because of complexity. From the responses here, it appears that it's actually far from being solved... Jun 26, 2013 at 20:06

4 Answers 4

226

Dependently Typed Haskell, Now?

Haskell is, to a small extent, a dependently typed language. There is a notion of type-level data, now more sensibly typed thanks to DataKinds, and there is some means (GADTs) to give a run-time representation to type-level data. Hence, values of run-time stuff effectively show up in types, which is what it means for a language to be dependently typed.

Simple datatypes are promoted to the kind level, so that the values they contain can be used in types. Hence the archetypal example

data Nat = Z | S Nat

data Vec :: Nat -> * -> * where
  VNil   :: Vec Z x
  VCons  :: x -> Vec n x -> Vec (S n) x

becomes possible, and with it, definitions such as

vApply :: Vec n (s -> t) -> Vec n s -> Vec n t
vApply VNil         VNil         = VNil
vApply (VCons f fs) (VCons s ss) = VCons (f s) (vApply fs ss)

which is nice. Note that the length n is a purely static thing in that function, ensuring that the input and output vectors have the same length, even though that length plays no role in the execution of vApply. By contrast, it's much trickier (i.e., impossible) to implement the function which makes n copies of a given x (which would be pure to vApply's <*>)

vReplicate :: x -> Vec n x

because it's vital to know how many copies to make at run-time. Enter singletons.

data Natty :: Nat -> * where
  Zy :: Natty Z
  Sy :: Natty n -> Natty (S n)

For any promotable type, we can build the singleton family, indexed over the promoted type, inhabited by run-time duplicates of its values. Natty n is the type of run-time copies of the type-level n :: Nat. We can now write

vReplicate :: Natty n -> x -> Vec n x
vReplicate Zy     x = VNil
vReplicate (Sy n) x = VCons x (vReplicate n x)

So there you have a type-level value yoked to a run-time value: inspecting the run-time copy refines static knowledge of the type-level value. Even though terms and types are separated, we can work in a dependently typed way by using the singleton construction as a kind of epoxy resin, creating bonds between the phases. That's a long way from allowing arbitrary run-time expressions in types, but it ain't nothing.

What's Nasty? What's Missing?

Let's put a bit of pressure on this technology and see what starts wobbling. We might get the idea that singletons should be manageable a bit more implicitly

class Nattily (n :: Nat) where
  natty :: Natty n
instance Nattily Z where
  natty = Zy
instance Nattily n => Nattily (S n) where
  natty = Sy natty

allowing us to write, say,

instance Nattily n => Applicative (Vec n) where
  pure = vReplicate natty
  (<*>) = vApply

That works, but it now means that our original Nat type has spawned three copies: a kind, a singleton family and a singleton class. We have a rather clunky process for exchanging explicit Natty n values and Nattily n dictionaries. Moreover, Natty is not Nat: we have some sort of dependency on run-time values, but not at the type we first thought of. No fully dependently typed language makes dependent types this complicated!

Meanwhile, although Nat can be promoted, Vec cannot. You can't index by an indexed type. Full on dependently typed languages impose no such restriction, and in my career as a dependently typed show-off, I've learned to include examples of two-layer indexing in my talks, just to teach folks who've made one-layer indexing difficult-but-possible not to expect me to fold up like a house of cards. What's the problem? Equality. GADTs work by translating the constraints you achieve implicitly when you give a constructor a specific return type into explicit equational demands. Like this.

data Vec (n :: Nat) (x :: *)
  = n ~ Z => VNil
  | forall m. n ~ S m => VCons x (Vec m x)

In each of our two equations, both sides have kind Nat.

Now try the same translation for something indexed over vectors.

data InVec :: x -> Vec n x -> * where
  Here :: InVec z (VCons z zs)
  After :: InVec z ys -> InVec z (VCons y ys)

becomes

data InVec (a :: x) (as :: Vec n x)
  = forall m z (zs :: Vec x m). (n ~ S m, as ~ VCons z zs) => Here
  | forall m y z (ys :: Vec x m). (n ~ S m, as ~ VCons y ys) => After (InVec z ys)

and now we form equational constraints between as :: Vec n x and VCons z zs :: Vec (S m) x where the two sides have syntactically distinct (but provably equal) kinds. GHC core is not currently equipped for such a concept!

What else is missing? Well, most of Haskell is missing from the type level. The language of terms which you can promote has just variables and non-GADT constructors, really. Once you have those, the type family machinery allows you to write type-level programs: some of those might be quite like functions you would consider writing at the term level (e.g., equipping Nat with addition, so you can give a good type to append for Vec), but that's just a coincidence!

Another thing missing, in practice, is a library which makes use of our new abilities to index types by values. What do Functor and Monad become in this brave new world? I'm thinking about it, but there's a lot still to do.

Running Type-Level Programs

Haskell, like most dependently typed programming languages, has two operational semanticses. There's the way the run-time system runs programs (closed expressions only, after type erasure, highly optimised) and then there's the way the typechecker runs programs (your type families, your "type class Prolog", with open expressions). For Haskell, you don't normally mix the two up, because the programs being executed are in different languages. Dependently typed languages have separate run-time and static execution models for the same language of programs, but don't worry, the run-time model still lets you do type erasure and, indeed, proof erasure: that's what Coq's extraction mechanism gives you; that's at least what Edwin Brady's compiler does (although Edwin erases unnecessarily duplicated values, as well as types and proofs). The phase distinction may not be a distinction of syntactic category any longer, but it's alive and well.

Dependently typed languages, being total, allow the typechecker to run programs free from the fear of anything worse than a long wait. As Haskell becomes more dependently typed, we face the question of what its static execution model should be? One approach might be to restrict static execution to total functions, which would allow us the same freedom to run, but might force us to make distinctions (at least for type-level code) between data and codata, so that we can tell whether to enforce termination or productivity. But that's not the only approach. We are free to choose a much weaker execution model which is reluctant to run programs, at the cost of making fewer equations come out just by computation. And in effect, that's what GHC actually does. The typing rules for GHC core make no mention of running programs, but only for checking evidence for equations. When translating to the core, GHC's constraint solver tries to run your type-level programs, generating a little silvery trail of evidence that a given expression equals its normal form. This evidence-generation method is a little unpredictable and inevitably incomplete: it fights shy of scary-looking recursion, for example, and that's probably wise. One thing we don't need to worry about is the execution of IO computations in the typechecker: remember that the typechecker doesn't have to give launchMissiles the same meaning that the run-time system does!

Hindley-Milner Culture

The Hindley-Milner type system achieves the truly awesome coincidence of four distinct distinctions, with the unfortunate cultural side-effect that many people cannot see the distinction between the distinctions and assume the coincidence is inevitable! What am I talking about?

  • terms vs types
  • explicitly written things vs implicitly written things
  • presence at run-time vs erasure before run-time
  • non-dependent abstraction vs dependent quantification

We're used to writing terms and leaving types to be inferred...and then erased. We're used to quantifying over type variables with the corresponding type abstraction and application happening silently and statically.

You don't have to veer too far from vanilla Hindley-Milner before these distinctions come out of alignment, and that's no bad thing. For a start, we can have more interesting types if we're willing to write them in a few places. Meanwhile, we don't have to write type class dictionaries when we use overloaded functions, but those dictionaries are certainly present (or inlined) at run-time. In dependently typed languages, we expect to erase more than just types at run-time, but (as with type classes) that some implicitly inferred values will not be erased. E.g., vReplicate's numeric argument is often inferable from the type of the desired vector, but we still need to know it at run-time.

Which language design choices should we review because these coincidences no longer hold? E.g., is it right that Haskell provides no way to instantiate a forall x. t quantifier explicitly? If the typechecker can't guess x by unifiying t, we have no other way to say what x must be.

More broadly, we cannot treat "type inference" as a monolithic concept that we have either all or nothing of. For a start, we need to split off the "generalisation" aspect (Milner's "let" rule), which relies heavily on restricting which types exist to ensure that a stupid machine can guess one, from the "specialisation" aspect (Milner's "var" rule) which is as effective as your constraint solver. We can expect that top-level types will become harder to infer, but that internal type information will remain fairly easy to propagate.

Next Steps For Haskell

We're seeing the type and kind levels grow very similar (and they already share an internal representation in GHC). We might as well merge them. It would be fun to take * :: * if we can: we lost logical soundness long ago, when we allowed bottom, but type soundness is usually a weaker requirement. We must check. If we must have distinct type, kind, etc levels, we can at least make sure everything at the type level and above can always be promoted. It would be great just to re-use the polymorphism we already have for types, rather than re-inventing polymorphism at the kind level.

We should simplify and generalise the current system of constraints by allowing heterogeneous equations a ~ b where the kinds of a and b are not syntactically identical (but can be proven equal). It's an old technique (in my thesis, last century) which makes dependency much easier to cope with. We'd be able to express constraints on expressions in GADTs, and thus relax restrictions on what can be promoted.

We should eliminate the need for the singleton construction by introducing a dependent function type, pi x :: s -> t. A function with such a type could be applied explicitly to any expression of type s which lives in the intersection of the type and term languages (so, variables, constructors, with more to come later). The corresponding lambda and application would not be erased at run-time, so we'd be able to write

vReplicate :: pi n :: Nat -> x -> Vec n x
vReplicate Z     x = VNil
vReplicate (S n) x = VCons x (vReplicate n x)

without replacing Nat by Natty. The domain of pi can be any promotable type, so if GADTs can be promoted, we can write dependent quantifier sequences (or "telescopes" as de Briuijn called them)

pi n :: Nat -> pi xs :: Vec n x -> ...

to whatever length we need.

The point of these steps is to eliminate complexity by working directly with more general tools, instead of making do with weak tools and clunky encodings. The current partial buy-in makes the benefits of Haskell's sort-of dependent types more expensive than they need to be.

Too Hard?

Dependent types make a lot of people nervous. They make me nervous, but I like being nervous, or at least I find it hard not to be nervous anyway. But it doesn't help that there's quite such a fog of ignorance around the topic. Some of that's due to the fact that we all still have a lot to learn. But proponents of less radical approaches have been known to stoke fear of dependent types without always making sure the facts are wholly with them. I won't name names. These "undecidable typechecking", "Turing incomplete", "no phase distinction", "no type erasure", "proofs everywhere", etc, myths persist, even though they're rubbish.

It's certainly not the case that dependently typed programs must always be proven correct. One can improve the basic hygiene of one's programs, enforcing additional invariants in types without going all the way to a full specification. Small steps in this direction quite often result in much stronger guarantees with few or no additional proof obligations. It is not true that dependently typed programs are inevitably full of proofs, indeed I usually take the presence of any proofs in my code as the cue to question my definitions.

For, as with any increase in articulacy, we become free to say foul new things as well as fair. E.g., there are plenty of crummy ways to define binary search trees, but that doesn't mean there isn't a good way. It's important not to presume that bad experiences cannot be bettered, even if it dents the ego to admit it. Design of dependent definitions is a new skill which takes learning, and being a Haskell programmer does not automatically make you an expert! And even if some programs are foul, why would you deny others the freedom to be fair?

Why Still Bother With Haskell?

I really enjoy dependent types, but most of my hacking projects are still in Haskell. Why? Haskell has type classes. Haskell has useful libraries. Haskell has a workable (although far from ideal) treatment of programming with effects. Haskell has an industrial strength compiler. The dependently typed languages are at a much earlier stage in growing community and infrastructure, but we'll get there, with a real generational shift in what's possible, e.g., by way of metaprogramming and datatype generics. But you just have to look around at what people are doing as a result of Haskell's steps towards dependent types to see that there's a lot of benefit to be gained by pushing the present generation of languages forwards, too.

11
  • 6
    I really don't care about the DataKinds stuff yet. Mostly because I want to do something like this: fmap read getLine >>= \n -> vReplicate n 0. As you note, Natty is a ways away from this. Furthermore, vReplicate should be translatable to an actual memory array, something like newtype SVector n x = SVector (Data.Vector.Vector x), where n has kind Nat (or similar). Perhaps another demonstration point for a "dependently-typed show-off?"
    – John L
    Nov 6, 2012 at 2:06
  • 7
    Could you say what you have in mind for an ideal treatment of programming with effects? Nov 8, 2012 at 5:36
  • 6
    Thanks for the great write-up. I'd love to see some examples of dependently typed code where some data originates outside the program (e.g. read from a file), to get a feel for how promoting values to types would look like in such a setting. I have this feeling that all examples involve vectors (implemented as lists) with statically known sizes.
    – tibbe
    Nov 8, 2012 at 5:48
  • 5
    @pigworker You take "no phase distinction" as a myth (the others I agree are myths). But you haven't dismantled this one in papers and talks I've seen, and meanwhile another person I respect tells me "dependent type theory is different from a typical compiler because we cannot meaningfully separate the type checking, compilation, and execution phases." (see Andrej' latest post of nov 8 2012) In my experience "faking it" we sometimes at least blur the phase distinction although need not erase it. Could you expand, if not here then elsewhere, on this issue?
    – sclv
    Nov 9, 2012 at 4:30
  • 4
    @sclv My work hasn't especially targeted the "no phase distinction" myth, but others' has. I recommend the rejectum "Phase Distinctions in the Compilation of Epigram", by James McKinna and Edwin Brady, as a good place to start. But see also much older work on Program Extraction in Coq. The open-terms evaluation done by the typechecker is completely separate from execution via extraction to ML, and it is clear that extraction strips out types and proofs.
    – pigworker
    Nov 9, 2012 at 8:56
22

Dependent typing is really just the unification of the value and type levels, so you can parametrize values on types (already possible with type classes and parametric polymorphism in Haskell) and you can parametrize types on values (not, strictly speaking, possible yet in Haskell, although DataKinds gets very close).

Edit: Apparently, from this point forward, I was wrong (see @pigworker's comment). I'll preserve the rest of this as a record of the myths I've been fed. :P


The issue with moving to full dependent typing, from what I've heard, is that it would break the phase restriction between the type and value levels that allows Haskell to be compiled to efficient machine code with erased types. With our current level of technology, a dependently typed language must go through an interpreter at some point (either immediately, or after being compiled to dependently-typed bytecode or similar).

This is not necessarily a fundamental restriction, but I'm not personally aware of any current research that looks promising in this regard but that has not already made it into GHC. If anyone else knows more, I would be happy to be corrected.

7
  • 51
    What you say is almost entirely false. I'm not entirely blaming you: it repeats standard myths as fact. Edwin Brady's language, Idris, performs type erasure (because no run-time behaviour depends on types) and generates a fairly standard lambda-lifted supercombinator encoding from which code is generated using stock G-machine techniques.
    – pigworker
    Oct 18, 2012 at 19:06
  • 3
    As a side note, someone recently pointed me to this paper. From what I can tell, it would make Haskell dependently-kinded (i.e., the type level language would be dependently-typed), which is as close as I can see us getting anytime soon. Oct 18, 2012 at 19:09
  • 8
    Yes, that paper does go most of the way to showing how to make types dependent on type-level stuff (and to eliminate the type/kind distinction). A plausible follow-up, already under discussion, is to permit actual dependent function types, but restrict their arguments to the fragment of the language that can exist in both value and type layers (now nontrivial thanks to datatype promotion). That would eliminate the need for the singleton construction which currently makes "faking it" more complex than desirable. We're getting steadily closer to the real thing.
    – pigworker
    Oct 18, 2012 at 19:14
  • 13
    There are lots of pragmatic questions, retrofitting dependent types to Haskell. Once we've got this restricted form of dependent function space, we still face the question of how to enlarge the fragment of the value language that's allowed at the type level, and what its equational theory should be (like we want 2+2 to be 4, and such). There are lots of fiddly issues (eg, bottom) that from-scratch dependently typed languages design away from the get go.
    – pigworker
    Oct 18, 2012 at 19:21
  • 2
    @pigworker Is there a clean subset of Haskell that's total? If so, couldn't we just use that for the "fragment of the language that can exist in both value and type layers"? If not, what would it take to produce one? Oct 18, 2012 at 19:25
21

John that's another common misconception about dependent types: that they don't work when data is only available at run-time. Here's how you can do the getLine example:

data Some :: (k -> *) -> * where
  Like :: p x -> Some p

fromInt :: Int -> Some Natty
fromInt 0 = Like Zy
fromInt n = case fromInt (n - 1) of
  Like n -> Like (Sy n)

withZeroes :: (forall n. Vec n Int -> IO a) -> IO a
withZeroes k = do
  Like n <- fmap (fromInt . read) getLine
  k (vReplicate n 0)

*Main> withZeroes print
5
VCons 0 (VCons 0 (VCons 0 (VCons 0 (VCons 0 VNil))))

Edit: Hm, that was supposed to be a comment to pigworker's answer. I clearly fail at SO.

6
  • Your first sentence seems a bit odd; I would say the point of dependent types is that they do work when data is only available at run-time. However, this CPS-style technique is not the same. Suppose you have a function Vec Zy -> IO String. You can't use it with withZeroes, because the type Zy can't be unified with forall n. Maybe you can work around that for one or two special cases, but it quickly gets out of hand.
    – John L
    Nov 6, 2012 at 17:16
  • The key when taking a simply typed value (like the String from getLine) and turning it into something with a stronger type (like a Natty n above) is that you have to convince the type checker that you are doing the necessary dynamic checks. In your example you're reading an arbitrary number so the forall n makes sense. More precise restrictions can be implemented in the same way. Do you have a better example than Vec Zy (the program would still need to handle the user inputing 5 rather than 0)?
    – ulfnorell
    Nov 6, 2012 at 20:10
  • 1
    What I meant to say with the first sentence is that I occasionally run into people that believe that you can't use dependent types if you get your data by interacting with the outside world. My point is that the only thing you have to do is write a dependently typed parser, which is usually straight-forward.
    – ulfnorell
    Nov 6, 2012 at 20:23
  • 1
    ulfnorell: Sorry, I wasn't clear. Suppose you have one function that will work with Vec Zy -> IO String and another for Vec n -> IO String, and you want to use the first only if the type matches. Yes it's possible, but the mechanisms for enabling it are clunky. And this is very simple logic; if you have more complex logic it's worse. Also, you may need to re-write a lot of code in CPS. And you still don't have a type-level expression that's dependent on a term at the value level
    – John L
    Nov 6, 2012 at 23:38
  • Ah, I see what you're saying. This is what Natty is for, like in vReplicate where we do different things depending on n. Indeed this can get a little clunky. An alternative to the CPS style is to work with packed up existentials: zeroes :: IO (Some (Flip Vec Int)).
    – ulfnorell
    Nov 7, 2012 at 7:22
21

pigworker gives an excellent discussion of why we should be headed towards dependent types: (a) they're awesome; (b) they would actually simplify a lot of what Haskell already does.

As for the "why not?" question, there are a couple points I think. The first point is that while the basic notion behind dependent types is easy (allow types to depend on values), the ramifications of that basic notion are both subtle and profound. For example, the distinction between values and types is still alive and well; but discussing the difference between them becomes far more nuanced than in yer Hindley--Milner or System F. To some extent this is due to the fact that dependent types are fundamentally hard (e.g., first-order logic is undecidable). But I think the bigger problem is really that we lack a good vocabulary for capturing and explaining what's going on. As more and more people learn about dependent types, we'll develop a better vocabulary and so things will become easier to understand, even if the underlying problems are still hard.

The second point has to do with the fact that Haskell is growing towards dependent types. Because we're making incremental progress towards that goal, but without actually making it there, we're stuck with a language that has incremental patches on top of incremental patches. The same sort of thing has happened in other languages as new ideas became popular. Java didn't use to have (parametric) polymorphism; and when they finally added it, it was obviously an incremental improvement with some abstraction leaks and crippled power. Turns out, mixing subtyping and polymorphism is inherently hard; but that's not the reason why Java Generics work the way they do. They work the way they do because of the constraint to be an incremental improvement to older versions of Java. Ditto, for further back in the day when OOP was invented and people started writing "objective" C (not to be confused with Objective-C), etc. Remember, C++ started out under the guise of being a strict superset of C. Adding new paradigms always requires defining the language anew, or else ending up with some complicated mess. My point in all of this is that, adding true dependent types to Haskell is going to require a certain amount of gutting and restructuring the language--- if we're going to do it right. But it's really hard to commit to that kind of an overhaul, whereas the incremental progress we've been making seems cheaper in the short term. Really, there aren't that many people who hack on GHC, but there's a goodly amount of legacy code to keep alive. This is part of the reason why there are so many spinoff languages like DDC, Cayenne, Idris, etc.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.