4 ms·

> [Dependent types] can by used to guarantee things like "applying 'concat' to a list of length X and list of length Y returns a list of X+Y". As a curious bys

• Warwolt 4y ago
  Dependent types allow for more nuanced statements made by types. You can for instance have a lists that are sorted in ascending order as a type, or implement messaging protocols at the type level where you can only construct a reply in the message exchange if you've received the correct preceding message. It's very cool, but it's very expensive to compile, which is why it's still research stuff, I believe.
  • kaba0 4y ago
    Not only “compile expensiveness”, but you quite literally have to prove your types in the program, which is seldom easy. E.g. if you were to write a merge sort, and have it in the type that it will output a sorted array, you will have a very hard time actually proving it correct, akin to algorithm analysis. Though to be fair most dependent typed languages allows for types without proofs, and having it in the type that an array is sorted for example can be valuable even without formal verification.
• gdprrrr 4y ago
  One example I like is a binary search Funktion which only allows to pass a sorted list
  • kaba0 4y ago
    Well, you can do that in traditional languages as well, just wrap your list in a SortedArray type. Chances are your “sorted” function won’t actually prove the algorithm used formally either in a dependently typed language.
• Atiscant 4y ago
  One way to think about it is that you can extend your testing to prove the correctness of your program up to some notion of what “correct” means. You can reason about your program in your program and that allows you to capture another class of errors than regular static typing does. In principle, a strong enough dependent type systems allows you to encode mathematics, and you can then prove thing about your program in the same language as your are writing it. As for practical examples, you should look at Idris and some of the talks given about it. They do very fancy things while still being somewhat performant. Besides errors and testing, having dependent types also allows your IDE to reason about your program and can give much stronger hints and code completion. But I agree that it is often a hard sell for normal developers. Given the choice, I would happily write large code bases in a dependent language, but I am also very biased having worked a lot in them.
  • Warwolt 4y ago
    One really nice "everyday" example that comes from Idris that I really like is the ability to typecheck a printf function. You provide the format string, and then the typechecker will know what to expect from the rest of the arguments! Usually that is implemented in C compilers, so that "printf("%d", 2.3f)" becomes an error, but with dependent types you can do it on the user level in library code.
    • ZitchDog 4y ago
      This is also possible in typescript which is a little more mainstream than Idris.
      • naasking 4y ago
        TypeScript's type system is not consistent though.
    • dwenzek 4y ago
      And here is a gist that demonstrates how simple it is to implement such a type-safe printf function: https://github.com/mukeshtiwari/Idris/blob/master/Printf.idr https://github.com/mukeshtiwari/Idris/blob/master/Printf.idr
• mcguire 4y ago
  One interesting aspect, at least for us old systems guys where runtime is important, is that you can not only move errors into compile time, you can move validation checks into compile time. Simple example: returning the head of a list is partial; normally, you have to have a check if the list is empty and return an error. With dependent types, you can guarantee that the list is not empty, moving that test to some higher level where it's actually meaningful. If you're manipulating arrays, you can guarantee at compile time that the indices have the right values, moving the tests outside of a function that gets called often. (In fact, when I was playing with ATS, this is what I did: I picked one boring validation test in the code at a time and moved it into the type. It vastly simplified the code.)
  • chriswarbo 4y ago
    > Simple example: returning the head of a list is partial; normally, you have to have a check if the list is empty and return an error. With dependent types, you can guarantee that the list is not empty, moving that test to some higher level where it's actually meaningful. You don't need dependent types for that. In particular, non-empty lists are isomorphic to a tuple containing a value for the head and a list for the tail: type NonEmptyList<T> = Pair<T, List<T>> Note that this is just the type of cons ( https://en.wikipedia.org/wiki/Cons https://en.wikipedia.org/wiki/Cons ). We can use this to define List recursively (representing an empty list (AKA nil) as the single value of type Unit): type List<T> = Either<Unit, NonEmptyList<T>> If we inline the definition of NonEmptyList, we get the usual definition of List<T> = Either<Unit, Pair<T, List<T>>>
• deleted 4y ago
  [deleted]
• deleted 4y ago
  [deleted]
• zasdffaa 4y ago
  IIUC, you can use it to ensure you never index outside the limits of your static array at runtime, this check being done at compile time.
• agumonkey 4y ago
  I have a different pov about this. It's an intellectual need to encode logic at the type level. It's not showing lots of practical value yet.. just like most interesting and generic techniques in the mainstream today.
  • valenterry 4y ago
    It's a practical need. It allows for the compiler to enhance your productivity by stopping mistakes and errors as soon as possible. For instance, you can't even write a generic "window slide" function support dynamic window length without this typelevel logic. Except of course if you don't mind your program to blow up on a mistake or write excessive tests for every piece of your code.
    • kaba0 4y ago
      Well, can it spot race conditions? Or will it suddenly solve the halting problem? Safety is not a binary value. Dependent types can increase safety, though they do come with a significant cost, which may very well be spent on additional testing, indeed.
      • valenterry 4y ago
        > Safety is not a binary value Exactly. Encoding logic in types doesn't have to fix all problems all the time. It's sufficient if advantages outweight the costs.
  • deleted 4y ago
    [deleted]
• dunham 4y ago
  Internally, the Idris2 compiler uses deBruijn numbering for its terms, which is tricky to get right once you start trying to manipulate terms. To help with this, it keeps a list of the names corresponding to the deBruijn indices at the type level. The type checker catches mistakes as you write code to manipulate them (inserting names, removing names, or renaming things). I ran through some exercises teaching this technique[1]. My take-away as a beginner was that it was a pain to make the compiler happy and my code that the compiler didn't like was actually wrong. I remember reading someone had written a functional red-black tree (with proof of correctness leveraging dependent types) and said the delete algorithm naturally followed from the types. That has was not my experience (delete wasn't immediately obvious to me), but I need to find some time to give it another go. The Idris2 docs have an example of a lambda expression interpreter[2] whose terms have a vector of the types in the environment as a type parameter (erased at runtime), to ensure everything is type safe in the resulting interpreter. Typescript has added some bits of dependent typing. For example, asserting a function returns true if the argument has type X, that a function throws if the argument is falsy, and I think type level string manipulation. They are fairly pragmatic, it's not a research language, so I presume that specific functionality is useful to a lot of people. I've used it a little bit of it to help the type checker infer non-null after my assert function was called. All of that said, I think people are still exploring how dependent types can be used in practice. [1]: https://github.com/edwinb/SPLV20/blob/master/Code/Lecture2/Exercises.txt https://github.com/edwinb/SPLV20/blob/master/Code/Lecture2/E... [2]: https://idris2.readthedocs.io/en/latest/tutorial/interp.html https://idris2.readthedocs.io/en/latest/tutorial/interp.html There is a copy of #1 at github.com/dunhamsteve/SPLV20 that is updated to work with the latest Idris2.
  • wk_end 4y ago
    TypeScript does not have dependent types. It has type-level constants and surprisingly powerful type manipulation facilities, including string manipulation on string type constants. But there's no way to operate on types at the "dynamic" expression level - they're deliberately erased, to the point that transforming TypeScript to JavaScript is almost trivial. For example, take the very first example of a dependent type in the Idris tutorial - a function `isSingleton` that consumes a `Bool` and produces `Nat` if you give it `True` and `List Nat` if you give it `False`; it then uses `isSingleton` as part of the type of `mkSingle`, a function that consumes a `Bool` called `x` and produces an `isSingleton x` - that is, a `Nat` if `x` is `True` and a `List Nat` if `x` is `False`. There's no way to write this in TypeScript. You could have `isSingleton` return dynamic constructors instead, but you can't use that `isSingleton` as part of the type of `mkSingle` to generate a return type. Your `mkSingle` would be stuck with the signature `(x: boolean): number | number[]`; which branch of the return type you end up with depends on `x`, but there's no way to make TypeScript properly understand the connection.
• sn9 4y ago
  http://kevinmahoney.co.uk/articles/tests-vs-types/ http://kevinmahoney.co.uk/articles/tests-vs-types/
• lmm 4y ago
  > As an example of what I'm looking for, I see regular static typing as a way to move a class of runtime errors to compile time errors, increasing your confidence in aspects that otherwise would need repetitive unit tests. Dependent typing just makes it easier to do that, by making the type system more expressive. For example a map where the values are of different types, but where the type for each key is fixed, is something that people do all the time in dynamic languages, but it's very cumbersome to express that to a static typechecker without dependent types, so even in a statically typed langauge people usually make do with a Map<String, Object> and have to use unit tests to confirm the behaviour.