Provide practical example of Dependent Types

[lancejpollard]

Hello, not sure if this entirely fits the guidelines for contributing, but wanted to ask about what dependent types are here, in case it could help clarify for others how dependent types work (which from my understanding so far in reading mostly through chapter 1, seems to be core to understanding HoTT).

I have spent the past few weeks slowly digesting the first chapter of HoTT. I have been introduced to Haskell, and recently installed Agda and Coq. I am imaging that by installing them, and trying to run the code in the HoTT/HoTT and HoTT/HoTT-agda projects, I will get a more intuitive, experiential grasp of dependent types (and eventually of homotopy type theory).

But even after these few weeks, I still don't quite understand what dependent types are, or the implication of them. Maybe it is outside the scope of the book, but it would be particularly helpful to see a practical use-case of dependent types coming from a programmers perspective. That would help really nail down the intuition of dependent types, which would greatly help in understanding the things that build upon it.

The description I have found most useful so far in developing an intuition for dependent types is here:

http://stackoverflow.com/questions/9338709/what-is-dependent-typing/9374698#9374698

With the example:

type BoundedInt(n) = {i:Int | i<=n}

With that I can sort of imagine (in source code) how you might use this in a language like Ruby, or JavaScript. To me, seeing that, I can imagine a use case like the following.. Maybe you have a web application (like GitHub itself) that has users and organizations. Maybe you want to say an organization can only have 100 members. So you might create a "type" of Organization which has a property "memberCount", which is of type BoundedInt(100). In pseudocode, maybe like:

data Organization where
  memberCount : BoundedInt(100)

From my understanding so far, that BoundedInt(100) is an example of a "dependent type". Not totally sure that is correct, so if not would love to know a more intuitive example (been searching the web for weeks for more practical examples but haven't found any other than that SO question).

Seeing an example like that, the dependent types and dependent product types start to make a lot of sense, where ∏(x:A) B(x) : U you could imagine as:

// javascript
function boundedIntDependentTypes() {
  var i = 0;
  var n = 100;
  var result = [];
  while (i++ < n) {
    var DependentType = BoundedInt(i);
    result.push(DependentType);
  }
  return result;
}

boundedIntDependentTypes();

# ruby
def bounded_int_dependent_types
  (0..100).map do |i|
    BoundedInt(i)
  end
end

Even though languages like Ruby and JavaScript don't support anything like this, an example like this allows you to compare the idea of "dependent types" with how you would typically implement that functionality in another language. So for that example above, one way to do that in JavaScript would be to create a subclass, something along the lines of:

class MemberCount extends Number
  constructor(x) ->
    assert(x <= 100);
    this.x = x;

Which that is super hacky, so then you can see the value of dependent types, and how they would really simplify stuff.

On a related note, in searching for more intuitive explanations of dependent types, it seems like many people have asked this same sort of question in different ways, so an intuitive description would be helpful all around. For example:

• http://stackoverflow.com/questions/12961651/why-not-be-dependently-typed
• http://programmers.stackexchange.com/questions/262377/what-are-the-practical-implications-of-homotopy-type-theory-in-programming

The idea of dependent types "bringing values and types on the same level" sort of makes sense too (seen this a lot in the Agda tutorials), but again, not totally sure what that means yet without having a more practical example.

Does that sort of make sense? Basically just wondering if this is a way to more intuitively introduce dependent types. The boolean and natural numbers examples in the book I think will eventually click, but they are too abstract for me to grasp after the first several readings (coming from a programming background).

[mikeshulman]

My first reaction is that I don't think this sort of thing would really be appropriate to include in the book, since it is focused on mathematics rather than programming, and especially on informal mathematics rather than mathematics formalized in a computer. We could consider adding some references to external introductions written for programmers, if there are some good stable ones (probably not stackexchange questions though).

However, if other people think this would be appropriate, I could be convinced.

[pthariensflame]

I agree with Michael in that I don't think this is appropriate for the HoTT book, but we definitely need a good programmer-oriented introduction to dependent typing suitable for leading into the book. I might try to write one, once my current projects are resolved.

[andrejbauer]

Let me just say that dependent types will make more sense from the point of view of a functional language such as Haskell or ML than they might from an object-oriented perspective.

Dependent types are everywhere in mathematics. Even just saying something like "consider a differentiable map f : [a,b] → ℝ", a common premise in real analysis, introduces a dependent type, namely an interval [a,b] which depends on its endpoints a and b. The type of the function f is then more properly written as f : ∏(a b : ℝ) [a,b] → ℝ, a dependent product.

In computer science the dependent types are everywhere, but they are not typically captured by code and programming languages. Programmers think informally in terms of dependent types all the time, they are just not aware of it. For example, something like strncpy is really a dependent function, because the length of the input string depends on the size parameter. This is not visible in the function declaration, but is part of the documentation.

My point is that you are not learning a new concept that you have never seen before. It's a familiar concept that is being made formally explicit.

[lancejpollard]

Cool, thanks guys for the thoughtful responses. I can see how this is outside the scope of the book and would be better in a separate book or something. Definitely looking forward to that @pthariensflame if you end up having time! Will close this issue for now.

@andrejbauer hmm will have to think about that one for a bit, still a little over my head. I have been a programmer for about 7 years so far (JavaScript and Ruby, and learning Haskell), but don't have a computer science degree. I have been picking up the more formal side of things in the past few months, but still haven't broken the barrier of being able to intuitively imagine super abstract stuff like the example you provided.

I can get to the point of imagining abstractions that are app-related, such as how you might mathematically model SQL queries or model data of some sort. Not exactly sure why, but for me app-level abstractions (just pulling that name out of the air) are easier for me to imagine because they are closer reality. Like I can see a table of data in a spreadsheet in my mind, and then SQL is an abstraction to manipulate that table of data, which is an abstraction on top of relational algebra, etc... So then I can read relational algebra with some intuition. But if the abstraction just starts with "imagine a type A x B : R, then you can see that this is really just a dependent product where f : ∏(a b : ℝ) [a,b] → ℝ", it's more difficult for me to make that leap in imagination.

From your years of experience, I imagine you guys probably have several canonical examples (like the Peano's natural number thing) that you spent a long time to internalize, and now when you see A x B : R your mind quickly imagines some tangible thing (like an equivalent to the spreadsheet in the SQL example). But maybe not, maybe at some point in mastering math you can just imagine the equations directly :) you would know better than me! I am working toward that, but not quite there yet haha.

One of the really cool things about you guys having these open source repos is it's an amazing way to learn how you guys approach highly abstract concepts. I'm super excited to learn how you guys think about and approach all of these math / proof / type theory problems :D

[andrejbauer]

The issue is closed, but let me just give you some SQL examples. In particular, an example which is naturally a dependent type and so it's a bit painful to do it in SQL.

Suppose we want to have a table person which contains medical info about people, so each row is a person (name, gender, etc.) Now some data makes sense only for women (number of births given), and some data only makes sense for men (has had a prostate examination). There is no optimal way to represent such data in SQL. A common solution is to have all attributes available for every person, and then you just set the non-sensical ones to NULL. But that's wasteful, the database is not told what is really going on, and it is error-prone. If we could have real dependent types in SQL, we would simply say that the types of some attributes depend on the value of the gender attribute.

In real-world programming dependent types get simulated by non-dependent types. A good sign that this is happening is when it's possible to create non-sensical values of some datatype (or a non-sensical row in SQL). With dependent types you can exactly describe what the conditions on the data are, no matter how complicated.