5 ms·

I was mostly joking... I understand how dependent types work and don't think those researching it are of "ill repute." It's worth pointing out though what is t

by dnomad 8y ago

I was mostly joking... I understand how dependent types work and don't think those researching it are of "ill repute." It's worth pointing out though what is the real flaw with union types and dependent types: syntax might obscure it but the actual program is riddled with conditional logic and it is very hard to reason about such types in practice. People like to call this "pattern matching" but in reality such code, where each function is generally doing if (x instanceof Y) over a set, is exactly the sort of code that we try to avoid in modern systems.

chriswarbo 8y ago
> exactly the sort of code that we try to avoid in modern systems What has "modern" got to do with any sort of value judgement? "Modern systems" could just as well be describing a tangle of Node.js spaghetti plugged into an unstructured pile of nosql data. > each function is generally doing if (x instanceof Y) over a set Your description sounds like some poor approximation of algebraic datatypes encoded in classes or something. I could imagine that being horrible. That doesn't mean that algebraic datatypes are horrible. Personally, I found OOP to be very difficult to get my head around for the first few years; after that, I found it to mostly be used as an excuse for bloat, boilerplate and architecture astronautics (true story: I was once called "too academic" for using PHP's `array_map` function, by someone who thought it was perfectly reasonable to have a class called `ServiceControllerServiceProvider`...). I find algebraic datatypes (sums/unions and products) to be much easier to reason about. In particular the data model is closed: these are the only possible cases we'll run into, handle them and we're done. OOP takes the other side of the "expression problem": its set of methods is closed, but we never know if some unexpected subclass might be passed in. Also note that `instanceof` isn't particularly applicable in languages like Idris, Agda, Haskell, etc. since they're based on type theory, where typing is a judgement not a proposition (see e.g. https://ncatlab.org/nlab/show/judgment#in_type_theory https://ncatlab.org/nlab/show/judgment#in_type_theory ). Whilst in e.g. set theory we might query whether or not an element is in a set, e.g. using `x ∈ ℤ`, in these languages everything has a (principal) type, and saying something like `x : Int` is just asserting/defining/constraining that the value has that type. In particular it doesn't give us any information to branch on (it's either correct, and couldn't be otherwise; or it's incorrect, and the program won't compile). Also there are no subtypes, so if the type signature says we have a `Foo` then it's definitely a `Foo`. Personally, after using and encountering many type systems, I've never seen a version of subtyping that seemed 'worth it', i.e. where the extra expressiveness or guarantees outweighed all of the edge-cases, co-variant/contra-variant gotchas, etc. By the way there's a great explanation of why OOP and classes are a poor implementation of subtyping at http://okmij.org/ftp/Computation/Subtyping/ http://okmij.org/ftp/Computation/Subtyping/ > syntax might obscure it but the actual program is riddled with conditional logic and it is very hard to reason about such types in practice If you're actually in favour of class-based OOP, then surely you realise that exactly the same thing applies to dynamic dispatch of method calls?
deleted 8y ago
[deleted]
taliaringer 8y ago
All nontrivial programs are riddled with conditional logic. The difference is whether or not this conditional logic is exposed at the type level. Every single time you branch over anything in your code (say, to check if a list is empty before calling a function that will fail on an empty list), you could bubble that branch up to the type level in a full dependently-typed language, and have the compiler do that check for you. (Of course, this doesn't necessarily mean you'd always want to!) Dependent types can be hard to work with because you have to hold the compiler's hand and tell it that yes, actually, the list you're working with at the point you want to call this function is definitely non-empty, and you can prove it by providing an instance of that type. So if you want to make a function that takes two non-empty lists l1 and l2 and spits back out a non-empty list l3 which is l1 ++ l2, in addition to the standard list append functionality, you need to show that l1 ++ l2 actually is non-empty. But the fact that you have to do so much of this manually is, in my (professional) opinion, more a limitation of what we can currently automate than an inherent limitation of dependent types. Sometimes you want the same guarantees, but it's easier to keep this separate from the list type. So you just write plain old vanilla list append, and then later on your inhabit the type that proves that for any two lists l1 and l2, l1 ++ l2 is non-empty. There are tradeoffs here: later on when you need a proof that (l1 ++ l2) is empty, you'll have to explicitly reference the type you found a term for earlier to show it to the compiler. If you put it into the list type itself, then you only need to do that once, when you write the append function. On the other hand, you also have to construct a whole bunch of other functions this way, and you might not actually care about the result being non-empty in those cases. Also in my professional opinion, switching back and forth between these representations will be easier very soon. There are probably dozens of fantastic researchers all over the world working on making this easier, and we've made a lot of progress these past few years! Regardless, deciding what you actually want to expose at the type level and how you want to expose it is an important design problem, and it depends a lot on what you want to be able to prove about your system without ever running your code.

by dnomad 8y ago

chriswarbo 8y ago

> exactly the sort of code that we try to avoid in modern systems What has "modern" got to do with any sort of value judgement? "Modern systems" could just as well be describing a tangle of Node.js spaghetti plugged into an unstructured pile of nosql data. > each function is generally doing if (x instanceof Y) over a set Your description sounds like some poor approximation of algebraic datatypes encoded in classes or something. I could imagine that being horrible. That doesn't mean that algebraic datatypes are horrible. Personally, I found OOP to be very difficult to get my head around for the first few years; after that, I found it to mostly be used as an excuse for bloat, boilerplate and architecture astronautics (true story: I was once called "too academic" for using PHP's `array_map` function, by someone who thought it was perfectly reasonable to have a class called `ServiceControllerServiceProvider`...). I find algebraic datatypes (sums/unions and products) to be much easier to reason about. In particular the data model is closed: these are the only possible cases we'll run into, handle them and we're done. OOP takes the other side of the "expression problem": its set of methods is closed, but we never know if some unexpected subclass might be passed in. Also note that `instanceof` isn't particularly applicable in languages like Idris, Agda, Haskell, etc. since they're based on type theory, where typing is a judgement not a proposition (see e.g. https://ncatlab.org/nlab/show/judgment#in_type_theory https://ncatlab.org/nlab/show/judgment#in_type_theory ). Whilst in e.g. set theory we might query whether or not an element is in a set, e.g. using `x ∈ ℤ`, in these languages everything has a (principal) type, and saying something like `x : Int` is just asserting/defining/constraining that the value has that type. In particular it doesn't give us any information to branch on (it's either correct, and couldn't be otherwise; or it's incorrect, and the program won't compile). Also there are no subtypes, so if the type signature says we have a `Foo` then it's definitely a `Foo`. Personally, after using and encountering many type systems, I've never seen a version of subtyping that seemed 'worth it', i.e. where the extra expressiveness or guarantees outweighed all of the edge-cases, co-variant/contra-variant gotchas, etc. By the way there's a great explanation of why OOP and classes are a poor implementation of subtyping at http://okmij.org/ftp/Computation/Subtyping/ http://okmij.org/ftp/Computation/Subtyping/ > syntax might obscure it but the actual program is riddled with conditional logic and it is very hard to reason about such types in practice If you're actually in favour of class-based OOP, then surely you realise that exactly the same thing applies to dynamic dispatch of method calls?

deleted 8y ago

[deleted]

taliaringer 8y ago

All nontrivial programs are riddled with conditional logic. The difference is whether or not this conditional logic is exposed at the type level. Every single time you branch over anything in your code (say, to check if a list is empty before calling a function that will fail on an empty list), you could bubble that branch up to the type level in a full dependently-typed language, and have the compiler do that check for you. (Of course, this doesn't necessarily mean you'd always want to!) Dependent types can be hard to work with because you have to hold the compiler's hand and tell it that yes, actually, the list you're working with at the point you want to call this function is definitely non-empty, and you can prove it by providing an instance of that type. So if you want to make a function that takes two non-empty lists l1 and l2 and spits back out a non-empty list l3 which is l1 ++ l2, in addition to the standard list append functionality, you need to show that l1 ++ l2 actually is non-empty. But the fact that you have to do so much of this manually is, in my (professional) opinion, more a limitation of what we can currently automate than an inherent limitation of dependent types. Sometimes you want the same guarantees, but it's easier to keep this separate from the list type. So you just write plain old vanilla list append, and then later on your inhabit the type that proves that for any two lists l1 and l2, l1 ++ l2 is non-empty. There are tradeoffs here: later on when you need a proof that (l1 ++ l2) is empty, you'll have to explicitly reference the type you found a term for earlier to show it to the compiler. If you put it into the list type itself, then you only need to do that once, when you write the append function. On the other hand, you also have to construct a whole bunch of other functions this way, and you might not actually care about the result being non-empty in those cases. Also in my professional opinion, switching back and forth between these representations will be easier very soon. There are probably dozens of fantastic researchers all over the world working on making this easier, and we've made a lot of progress these past few years! Regardless, deciding what you actually want to expose at the type level and how you want to expose it is an important design problem, and it depends a lot on what you want to be able to prove about your system without ever running your code.