8 ms·

Recently I talked with my cousin, who is also a software engineer, about dependent types, contract programming, invariants, and all that. Among other things I'v

• alexashka 8y ago
  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 been having. Typescript is a good example - it came with VS Code integration out of the box, and some decent tutorials. It solves the problem of catching dumb type mismatch bugs at compile time, gives jump-to-definition, auto-complete and doesn't cost anything, it's opt-in. Those are killer usability features! Dependent types give type theorists a place to try interesting things. That's about it so far. Regarding invariant annotations - people call those tests :)
  • 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.
  • 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.
• mindB 8y ago
  I'm not super familiar with it, but ATS[1] might fit the bill in having dependent types and linear types but supporting both functional and imperative paradigms. It's pretty darn obscure, though. [1] http://www.ats-lang.org/ http://www.ats-lang.org/
  • PeCaN 8y ago
    ATS is an amazing language, but suffers from being mainly a one-person effort. doublec's ATS articles are probably the most accessible introduction: https://bluishcoder.co.nz/tags/ats/index.html https://bluishcoder.co.nz/tags/ats/index.html Other than that the documentation is very decent for a one-man research project. (I say "research project", and it is, but it has huge practical value as well.) Still, I have very high hopes for ATS.
• star-castle 8y ago
  OCaml has a type-safe printf and isn't purely functional. ATS is essentially 'C with dependent types'. And optionally some other languages with dependent types. You can think of its dependent type checking and theorem-proving as 'pre-compilation', since there's no runtime overhead to it (and since you can separate it out into its own compilation step, including swapping out alternative solvers). ATS's relationship with C is good enough that you can take an arbitrary C program and start tightening its screws by injecting a bit of ATS into it.
  • lomnakkus 8y ago
    > OCaml has a type-safe printf and isn't purely functional. Isn't that a non-extensible built-in that's handled "magically" by the compiler? (Apologies if that's wrong, it's been a few years since I've used O'Caml.) In Idris it's possible to write a type-safe printf entirely in library code -- no magic.
    • wk_end 8y ago
      IIRC the only magic is in parsing the format string to a structured representation of it; but that format object is a normal ocaml value and the actual typechecking happens without any "magic".
      • mixedCase 8y ago
        >the only magic is in parsing the format string to a structured representation of it That's the "magic" being discussed, where the value determines the type of something, hence, dependent typing :)
        • wk_end 8y ago
          (sorry for the late reply, I didn't see this) The magic that's happening in the ocaml compiler isn't dependent typing - it's a purely syntactic transformation, something like GHC turning "hello" into ['h', 'e', 'l', 'l', 'o'] into 'h':'e':'l':'l':'o':[]. ocaml notices that you have a string literal in a place where a format string is expected and swaps it out - that's all. It's magic, but it's unrelated to the type system - the type system comes in later. What does it replace it with? A value of type ('a, 'b, 'c, 'd, 'e', f) fmt. fmt is a GADT [1], fully defined within ocaml [2] - and I promise, ocaml does not have full dependent types. [1] https://en.wikipedia.org/wiki/Generalized_algebraic_data_type https://en.wikipedia.org/wiki/Generalized_algebraic_data_typ... [2] https://caml.inria.fr/pub/docs/manual-ocaml/libref/CamlinternalFormatBasics.html#TYPEfmt https://caml.inria.fr/pub/docs/manual-ocaml/libref/Camlinter...
• tel 8y ago
  My understanding is that the research background for a lot of dependently typed designs is based on proof theories where the program/proof represents the theory/constraint one-to-one. Other systems (PRL, Hoare logic) also exist but either have difficulties or haven’t had the same level of research and exploration to reach designs like modern dependently types languages. So you can easily add imperative steps to such a language, but since you not rely on side-effects for “interesting” behavior, it becomes more difficult to match the underlying proof theories to the kind of verification you’re attempting. I’m confident people will flood this comment with sources showing how proof theories exist which don’t have these properties, but I think the prevalence of DT langs nowadays does suggest that this particular synthesis is somewhat more productive so far.
• insulanus 8y ago
  It's not necessary to be a functional language to have this feature, but in the past it has been the case that mostly functional languages are the ones that do. The reason I think this happened, is that the language designers of languages like C had things like machine code generation at the top of their mind when writing the language, not abstractions. Once decisions were made in that mindset, you start making things very difficult to add this without having edge cases. Anyway, C++ finally has enough features to support this, and the committee will accept it into the standard soon-ish. (Mind you, of course you will still be able to do foolishness like: std::cout << static_cast<TrustMeImPrintable>(0); P.S. The feature you need to support this is to be able to pick the types our of the "format sting" (whatever type you use to represent that object), and run a check against the types of the arguments, at compile time.
• bakhy 8y ago
  For C#, and all .NET languages, there are Code Contracts. I've never used them, but they seem to be maintained and relatively easy to use. The docs, with a good example at the end, are here: https://docs.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts https://docs.microsoft.com/en-us/dotnet/framework/debug-trac... Edit: Actually it seems abandoned, with no support for .NET Core right now. Shame.
• repolfx 8y ago
  Imperative and functional programming languages have gone in different directions with respect to proving program correctness. I'm not sure one path is clearly better than another, they're just different. The imperative world has languages like Dafny or Whiley, where functions are annotated with expressions denoting things that must be true, and the compiler does theorem proving to ensure that the constraints aren't violated. So rather than put things like "length of array A equals length of array B" into types, you put that rule into the code, and the compiler proves that the constraint always holds. Unfortunately all these languages aren't really mature, whether they use dependent types or contracts. The imperative versions in particular often need you to specify constraints that are obvious.
  • pron 8y ago
    > The imperative world has languages like Dafny or Whiley, where functions are annotated with expressions denoting things that must be true, and the compiler does theorem proving to ensure that the constraints aren't violated. We have that for Java, too: http://www.openjml.org/ http://www.openjml.org/ The great thing about contracts (as opposed to dependent types) is that they separate specification from verification. You could use proofs (fully- or semi-automatic), but you could also use weaker but cheaper forms of verification, such as concolic tests or randomized tests, generated from the contracts, or, weaker still, runtime assertions. Dependent types tie specification to a specific form of verification (proof). A standardized specification language like JML can (and does) have many tools offering different forms of verification.
  • mcguire 8y ago
    In addition to Dafny (https://github.com/Microsoft/dafny https://github.com/Microsoft/dafny) and Whiley (http://whiley.org/ http://whiley.org/), check out Frama-C (https://frama-c.com/ https://frama-c.com/) for C and SPARK (http://www.spark-2014.org/ http://www.spark-2014.org/) for Ada. Both are mature enough to be in use, but are limited primarily by the fact that both languages have manual memory management, which is well understood via separation logic, but poorly supported by the tools. I've written some blog posts about Frama-C: * https://maniagnosis.crsr.net/2017/06/AFL-brute-force-search.html https://maniagnosis.crsr.net/2017/06/AFL-brute-force-search.... * https://maniagnosis.crsr.net/2017/06/AFL-bug-in-quicksearch.html https://maniagnosis.crsr.net/2017/06/AFL-bug-in-quicksearch.... * https://maniagnosis.crsr.net/2017/07/AFL-correctness-of-quicksearch.html https://maniagnosis.crsr.net/2017/07/AFL-correctness-of-quic... * https://maniagnosis.crsr.net/2017/08/AFL-verifying-quicksort.html https://maniagnosis.crsr.net/2017/08/AFL-verifying-quicksort...
• FeepingCreature 8y ago
  D has something like type-safe printf. You can pass the printf string as a compiletime parameter, so ie. format!`%s is bigger than %s`(2, 3, 4) will error during compilation.
  • ben-schaaf 8y ago
    It also has similar type safety for native to `byte[]` conversion, ie. `bigEndianToNative!int` takes a `byte[4]`, which you can pass in from a `byte[]` using `data[0..4]`.
  • icebraining 8y ago
    The question is whether that's a special case of the compiler or if it can be implemented by regular D code.
    • FeepingCreature 8y ago
      It is implemented by regular D code in std.format. Logging libraries often do the same thing.
• weavie 8y ago
  I'm not sure how it would be possible to have dependent types in a non-pure language. A function such as append: Vect n elem -> Vect m elem -> Vect (n + m) elem only works because the compiler can know exactly what is going to happen to those parameters in the function. It can guarantee that there are no side effects that can randomly and non-deterministically come along and change the result. The `Vect n elem` input parameter is always going to be a parameter of n elements. If the function changed n to be (n + 1) then should the result be `Vect (n + 1 + m) elem` or still `Vect (n + m)`? Things get a lot harder to lock down!
  • ihm 8y ago
    +1. If the language is not pure it's unclear how type checking would work. To make things even clearer, consider the following example (in a hypothetical dependently typed language with mutable references): f : () -> Type f = let r = ref 0 in fun () -> let t = if !r = 0 then Int else String in r := r + 1; r x : f () x = 17 y : f () y = "foo" Should this program type check? I think there is a consistent way to talk about type checking here (if there is a canonical ordering of all definitions across all files) but it seems unlikely you'll get a system that's easy to understand.
  • saurik 8y ago
    I don't understand the issue... it is trivial and in fact extremely common-place in impure languages to fundamentally disallow modifications to something's type. C++, which is definitely not pure but yet essentially has dependent types, is easily able to express this exact thought without problem, as your ability to modify things at runtime is extremely limited. (Of course, the place where C++ is limited is its inability to template over non-concrete values, but I see nothing about its model that fundamentally limits its ability to conceptualize such a thing. It is still technically a dependently typed language even without the ability to do this, of course.) [edit: matt-noonan has told me that I am wrong on that last comment :(... so not "of course".] #include <stdlib.h> template <size_t S, typename E> class Vect { private: E data[S]; public: const size_t size() const { return S; } E &operator [](size_t i) { return data[i]; } const E &operator [](size_t i) const { return data[i]; } }; template <size_t N, size_t M, typename E> Vect<N + M, E> append(const Vect<N, E> &l, const Vect<M, E> &r) { Vect<N + M, E> v; for (size_t i(0); i != N; ++i) v[i] = l[i]; for (size_t i(0); i != M; ++i) v[N+i] = r[i]; return v; } int main() { Vect<4, int> a; Vect<2, int> b; Vect<6, int> c = append(a, b); Vect<8, int> d = append(a, b); return 0; } test.cpp:36:18: error: no viable conversion from 'Vect<4UL + 2UL aka 6, [...]>' to 'Vect<8, [...]>' Vect<8, int> d = append(a, b); ^ ~~~~~~~~~~~~ test.cpp:4:7: note: candidate constructor (the implicit copy constructor) not viable: no known conversion from 'Vect<4UL + 2UL, int>' to 'const Vect<8, int> &' for 1st argument class Vect { ^ 1 error generated.
• hota_mazi 8y ago
  In a nutshell, all dependent type systems are very impractical to use and are widely seen as going way past the point of diminishing returns for real world scenarios. It's not really a coincidence that most illustrations of dependently type programs never go beyond a simple list/stack/vector structure. I'll take a statically typed language with a decent type system and and assortment of tests any day over a dependently typed language.
• dorfsmay 8y ago
  Is ATS purely functional? Wikipedia lists it as multi-paradigm. https://en.wikipedia.org/wiki/ATS_(programming_language) https://en.wikipedia.org/wiki/ATS_(programming_language)
• KirinDave 8y ago
  Haskell is an excellent imperative language and can simulate some aspects of dependent typing. There are also refinement types which are related. Typesafe printf is actually a very old trick, typed scheme and even Common Lisp have been showing off macro-based variants for some time. As for why there aren't more languages directly LIKE Idris and Agda? Probably because the technology and theory to actually make them feasible has existed for less than a full decade. Sorta like how people don't realize sort is an O(n) operation, CRDTs exist, or that we can write lazy succinct parsers of complex tree structures, or can write universal query-insensitive indicies over relational data.
  • nickpsecurity 8y ago
    Liquid Haskell is probably the closest to Idris in its goals: https://wiki.haskell.org/Liquid_Haskell https://wiki.haskell.org/Liquid_Haskell
• saurik 8y ago
  Technically (and truly), C++ has dependent types, as types can depend on values [edit: matt-noonan has corrected me and pointed out this is wrong, but I think most of this comment is still useful]. (I can't say much about D, but I would believe it does as well; I could also see them having "simplified" away a really critical piece, though.) A prototypical concept you would expect to find in a dependently typed language is "the ability to have a function that concatenates to arrays of sizes X and Y and returns an array of size X+Y that can be safely verified against further functions that also require arrays given as arguments to have specific lengths". C++ is a bit indirect in its semantics here, but you will note that most other languages with generic types cannot express this thought (using either real integers or simulating them with types, either of which can be done in C++). One could easily imagine "filling out" C++ to allow compile time type argument manipulation of more value types without even stressing its model, and in fact that is exactly the direction the language has been going in with constexpr. Here is an article on how to build a compile-time printf using C++14. http://blogs.microsoft.co.il/sasha/2015/01/29/compile-time-runtime-safe-replacement-printf/ http://blogs.microsoft.co.il/sasha/2015/01/29/compile-time-r... The only real limitation in C++ is that these values have to be relatively "concrete": at some level there has to be a number that can be calculated, as you can only deal with values as you don't have the amazing ability to do unification of program fragments like you have access to in Idris (like, you'd like to be able to say "the length of this array is the same as the length of this runtime string", and then after a bunch of array manipulation claim that you return a string five characters longer than the input string). Again, though: this could be added to C++ without breaking its underlying model. And it definitely is not required by the concept of "dependent types" [edit: matt-noonan points out it is, in fact, required for a language to have "dependent types" :(.]
  • pjmlp 8y ago
    Which is why after so many years of playing with FP on the sidelines, I have come to realize C++ has become a good way to use those concepts, while keeping my CV relevant for the kind of work I do. Sometimes it feels like a kludge, but then I get to enjoy the nice IDEs, libraries that it has. If only C++ had proper pattern matching support. Of course, it isn't the only language I play with.
  • 8y ago