6 ms·

Dependent types are a solution in search of a problem. Widespread adoption comes from an easy to use, backed by big name, solution to a problem people have bee

• nine_k 8y ago
  Maybe the typical "pedestrian" problems, like lists having non-zero length, or numbers being in a given range, can be checked statically with simpler means that full-on dependent types? E.g. safe resource deallocaion problem can be seen as a dependent-type problem (only let an initialized resource into a deallocator), but is usually solved with sort-of linear types, or even simpler (though more crude) means.
  • dnomad 8y ago
    It's not clear that dependent types even are types. Does a zero-length list offer a different methods than a list that contains some elements? Does the compiler magically eliminate the 'remove()' method and then add it back when you add some elements? The entire domain is highly dubious and the people researching it are often of ill repute.
    • fiddlerwoaroof 8y ago
      Basically, the way it works is that the compiler prevents you from calling functions like head, tail and remove unless it has a proof that the list is non-empty.
    • star-castle 8y ago
      c.f. https://github.com/deech/LeftPad/blob/master/left-pad.org https://github.com/deech/LeftPad/blob/master/left-pad.org , in particular "At the type level we have:" and "At the level of sorts and refinements:" Or take this silly code: https://stackoverflow.com/questions/50658528/how-do-you-replace-static-assertions-with-prfuns https://stackoverflow.com/questions/50658528/how-do-you-repl... At the type level, nothing changes between the first program and the second. At the level of sorts and refinements, ATS2 is given more information in the second program so it's able to turn the two noted error conditions into compile time errors, when in first program they could only be runtime errors. I haven't heard anything bad about Hongwei Xi. Who are these ill-regarded researchers?
    • alexashka 8y ago
      The removeLast() function signature would be UntypedCollection (S n) -> UntypedCollection n (S n) stands for successor of n. (Think of (S n) as n+1) Given this, you can't call removeLast() on an UntypedCollection Z (empty collection) because the types wouldn't match. So it's not by magic - the compiler knows the number of elements in the collection, because that value is part of the type. That's the entire point of dependent types - you get to have any value as part of a type. The part that becomes tiresome very quickly - is convincing the type checker that what you want is valid. You have to provide proofs for the most trivial things (2+1 = 1+2) and the way it is currently achieved, is not programmer friendly.
    • chriswarbo 8y ago
      > Does the compiler magically... No. There is no magic. I had trouble understanding dependent types at first, thinking that the compiler was doing something magical, but in fact it's excrutiatingly simple (it has to be, since computers are dumb). > It's not clear that dependent types even are types. In the case of lists and non-empty lists, these can indeed be represented as different types. In particular, a non-empty list is a pair type, containing a value and a list of values, e.g. `(myInt, myListOfInts)`. This represents a non-empty list starting with `myInt` and followed by whatever's in `myListOfInts`. Notice that this must be non-empty, regardless of what's in `myListOfInts` (or if it's empty), since we have the first value right there (`myInt`)! This is a fundamentally different type than a normal, potentially empty list. Normal lists are a sum type (AKA tagged union): they can either be empty (usually represented with the symbol `nil`), or they can be a pair containing a value and another list (usually represented as a function call `cons(myValue, myList)`). Notice that the second possibility for normal lists corresponds exactly to our representation of non-empty lists. We can think of a list as being either empty or a non-empty list. Likewise we can think of a non-empty list as a pair of a value and a list. Now this all seems quite recursive, self-referential and circular (which it is!), but that's just our mental model. When we actually write this down as a program we must be very explicit about what's going on. In particular, we cannot just throw pairs of things together and expect the compiler to figure out that these are lists/non-empty lists/etc. > Does the compiler magically eliminate the 'remove()' method and then add it back when you add some elements? No. You do that, manually, when you change the representation of your data. In particular, we must explicitly choose whether we're making a normal list or a non-empty list, and we must explicitly convert between the two as necessary (there is no magic!). In Idris this might look something like: data List (t : Type) : Type where ListNil : List t ListCons : t -> List t -> List t data NEList (t : Type) : Type where NECons : t -> List t -> NEList t Now we can write functions which deal with a List or with a NEList, but not both, since that would be a type error e.g. "Expected 'List t', got 'NEList t'" (note that we can code to an interface, and there are some interfaces like `Mappable` or `HasLength` which can be implemented by both types, but that's another topic!). > Does a zero-length list offer a different methods than a list that contains some elements? Yes. If we have a non-empty list, we can get its first element (AKA the "head") and we can get a list of any following elements (AKA the "tail"): -- The head function is trivial for NEList neHead : (t : Type) -> NEList t -> t neHead t (NECons x ys) = x -- The tail function is trivial for NEList neTail : (t : Type) -> NEList t -> List t neTail t (NECons x ys) = ys These functions are easy for NEList, but they only work for NEList; we can't pass these a List since that will be a type error. We also can't write a head or tail function for List, since there's no way to handle the Nil case: -- The head function is impossible to write for List, since there's no valid -- return value when we're given Nil lHead : (t : Type) -> List t -> t lHead t (ListCons x ys) = x lHead t ListNil = {-WHAT COULD POSSIBLY GO HERE?-} lTail : (t : Type) -> List t -> List t lTail t (ListCons x ys) = ys lTail t ListNil = {-WHAT MIGHT GO HERE?-} The head function is impossible to write for List, since there's nothing which makes sense for Nil. For the `lTail` function we could actually return `Nil` and that would type check, but it's debatable whether that actually makes sense. > Does the compiler magically eliminate the 'remove()' method and then add it back when you add some elements? No. We do that when we "add elements" using either `ListCons` or `NECons`: if we use the `NECons` we get back an `NEList` which we can pass to functions like `neHead` and `neTail`. If we instead chose to use `ListCons` then we'd get back a normal List, which would give a type error if we tried to use it with `neHead` or `neTail`. Notice that if we used a `ListCons` value, we know what the return values of `lHead` and `lTail` should be. Yet the compiler doesn't know that (it's not magic!), so it doesn't allow us to write such functions. This is what we mean when we say phrases like "convincing the compiler that such-and-such", or that there are "proof obligations to fulfil": the thing we want to do might be perfectly reasonable (e.g. taking the `lHead` of a `ListCons` value) but the compiler forbids it because there appear to be unhandled cases (`ListNil`) and it's too dumb to figure out that they don't apply. The way we "convince" the compiler is to manually rearrange our data into a different form, where we can handle all of the possibilities (like `NEList` which only has the `NECons` case). Notice that we can easily convert an `NEList` into a `List`, if we need to (e.g. to use a function which only works on `List`): -- Some function we might want to use, which we've only defined for List lLength : (t : Type) -> List t -> Int lLength t ListNil = 0 lLength t (ListCons x ys) = 1 + lLength ys -- It's easy to convert an NEList to a List, since NECons contains the arguments -- we need for ListCons neToL : (t : Type) -> NEList t -> List t neToL t (NECons x ys) = ListCons x ys -- We can get the length of an NEList by converting it to a List first neLength : (t : Type) -> NEList t -> Int neLength t ne = lLength (neToL ne) What if we try to "trick" the compiler into taking the head of a List, by first converting a List into an NEList? It turns out to be impossible, precisely because there's no valid (type-correct) value we can use when we've been given ListNil: -- It's impossible to convert a List to an NEList, since there's nothing we can -- use as the first argument of NECons when we only have Nil lToNE : (t : Type) -> List t -> NEList t lToNE t (ListCons x ys) = NECons x ys lToNE t ListNil = NECons {-WHAT COULD GO HERE?-} Nil Notice that the first argument to NECons must have type `t`, but that could be anything since it's one of our arguments! The same goes for the return value of "head" above. Remember that Idris, etc. don't have a "null" value, so there's nothing we could put here (Haskell would let us use "bottom", i.e. a runtime error, but Idris prevents that unless we disable its totality checker). As for going the other way ("eliminate the 'remove()' method"), notice that the second argument of NECons is a List, not an NEList. This means that when we remove an element from a non-empty list (e.g. using `neTail`, or just pattern-matching on an `NECons` value) we get back a List, which we cannot pass to functions which require a non-empty list. Perhaps that List we get back does actually contain some elements. Yet the compiler doesn't know this (it's not magic!), and it certainly has no reason to think so. If we know that the tail of some NEList is actually non-empty, then we need to "convince the compiler" by converting it into an NEList. As we saw above, we cannot do that in general (since not all lists are non-empty!), but we might be able to do so on a case by case basis, i.e. by figuring out the correct value to pass as the first argument of NECons in each specific case.
    • drdeca 8y ago
      Well, how are you defining type? Are you defining type by the collection of methods a value or term of that type would have? That doesn't seem like the best definition to me, but ok. I would think that a good definition would probably involve something like, a type is the thing which restricts what terms or values can be in what places in what expressions/statements. As others have said, a function could very well require that its argument be a list which isn't of length 0. The way you phrased the question sounds like you are thinking of the methods as being contained in the value or something like that. Things don't need to work that way. You could just treat "calling a method" of an object like a different notation for calling a function with that object being the first argument. (Which, if the method required the list to be non-empty, would just be a compile time type error if it couldn't be determined that the list would be non-empty.)
• pron 8y ago
  Dependent types are an active area of research. They are one of several different avenues of research into program verification. The problem is that both their proponents and detractors (as well as those of other verification approaches) confuse research and practice. Think of the field as early stages of pharmaceutical research; experiments in the lab show some promise as well as obstacles, but it's too early to tell which of the approaches, if any, would be able to work at a large scale in field conditions. As long as we don't confuse research and practice we can follow, enjoy and evaluate research on its own terms, rather than judging it based on criteria that may not be relevant at this stage. This is not to say that we cannot point out risks to field adoption, but research is research. I, too, have my doubts about dependent types, but it's unfair to judge them harshly at this stage, when nobody knows how best to use them.