Re:Notes on Idris (2017)
by chriswarbo on Thursday June 07, 2018 @05:39PM
(#17260534)
> 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 ). 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/
> 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?
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 ). 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/
> 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?