1. 18

    Okay, I’ll bite, despite the click-baity title (A scam? Seriously? Who’s attempting to deceive anyone? Is there money to be gained fraudulently here?)

    The value in Curry-Howard, like so many things, is not at the extremes - like the example programs here that only prove vague and uninteresting things, or the complex proofs that don’t give you much computational behaviour - but somewhere in the middle. That is, programs that express some lightweight invariant that needs to be maintained, so there is value in expressing it in the type meaning that you have a proof that it is maintained. Here’s an example from the Idris 2 implementation:

    eval : {free, vars : _} ->
           Env Term free -> LocalEnv free vars ->
           Term (vars ++ free) -> Stack free -> Core (NF free)
    

    This type says that we have an environment of free variables free, some additional bound local variables vars, and the process of evaluating an expression gives us a normal form which doesn’t refer to the bound variables any more, because they’ve been substituted in. And I know that’s true, because the type says so, and the type checker agrees. Variable scoping is easy to get wrong, so I’ve decided it’s important to prove it’s right throughout.

    Here’s another example, more contrived but I think easier to understand:

    uncompress : RLE xs -> Singleton xs
    

    That’s the type of a program which takes a compressed, run-length encoded representation of a list xs, and gives back the uncompressed representation. It’s both a program which does the uncompression, and a proof that the uncompressed list is the same as the original. Or, maybe you could read it as: “For all run-length encoded lists, there is a way to reconstruct the original list, and this is it.”

    Is Curry-Howard overrated? Probably. I’d even have read the article if that’s what the title said, and I’d probably have largely agreed with it. But even so, it’s a useful way to understand what’s going on in languages with more expressive type systems.

    The internet is already full of articles with clickbaity titles that take an extreme and infer some general negative conclusion from it. Let’s not have more of them.

    1. 2

      The value in Curry-Howard, like so many things, is not at the extremes

      Yup. It allows us to reason about our code in the same way we can reason about mathematical proofs. That’s about it. That’s both extremely powerful and useless, depending on your environment and what you’re trying to do.

      I think a lot of this gets back to what another commenter said: tooling and language choice. The program is not the proof, but the running of the program can work just like a proof if you set it up correctly. That’s an extremely cool observation. Not such a good essay.

      1. 3

        Yup. It allows us to reason about our code in the same way we can reason about mathematical proofs. That’s about it. That’s both extremely powerful and useless, depending on your environment and what you’re trying to do.

        But why do you need C-H to do this reasoning? C-H is a much more narrow result, specifically proving a duality between proof and program. Verification of invariants does not require C-H.

      2. 2

        Author here. I should have titled it “over hyped” or “overrated” indeed (in the conclusion I do acknowledge the click baitiness, but oh well ^^). I do love type driven programming, even from my lowly OCaml vantage point, and Idris is pretty cool. The eval example is impressive.

        Excerpt which hopefully isn’t too far off:

        Idris could possibly have some interesting proofs that are also real programs… if it were designed to be a proof assistant and not a beefed-up programming language.

      1. 4

        Has anyone here played with Idris 2 recently? How does it compare in terms of “readiness” with Idris 1?

        1. 25

          I’m biased here, since I’m writing the thing, but I would strongly recommend using Idris 2 over Idris 1 now.

          The tools aren’t as polished, but that’s coming, and it’s more than made up for by the fact the the tools we do have (especially interactive editing) actually scale beyond small programs - I’m actively using the interactive tools for editing Idris 2 itself. The code it generates is much faster (targetting Chez Scheme, which is well suited to the job) and erasure is predictable, so you actually know what’s going to run at run-time rather than trusting inference to do what you want.

          Also, it’s much more robust. Not that there aren’t lots of issues to deal with, of course - that is always the way - but given that the implementation takes advantage of Idris’ type system, the issues that do arise tend to be more about high language design questions and presentational things than anything fundamental.

        1. 4

          Very interesting that it’s faster than the previous version written in Haskell. I’d love to hear more about what the contributing factors were to the performance increase.

          1. 25

            This question has come up a few times, so I’ve rattled off a thing that I think covers the main factors: https://www.type-driven.org.uk/edwinb/why-is-idris-2-so-much-faster-than-idris-1.html

            tl;dr: it turns out it’s much easier to improve performance spectacularly when it starts so bad :)

            1. 2

              While you are here, is the Type Driven Development book still relevant? It’s from 2017 so I am somewhat skeptical how relevant it is now.

              I’d like to give Idris a go :)

                1. 3

                  Once Idris 2 is released, do you have any plans to update the book / produce a new edition?

              1. 1

                Thank you!

            1. 3

              I wonder if Idris 2 (https://github.com/edwinb/Idris2) will help with any of the problems with Idris that you encountered. The Readme makes a few claims which might be relevant:

              • Better inference…
              • Better type checker implementation which minimises the need for compile time evaluation.
              • New Chez Scheme based back end which both compiles and runs faster…
              • Everything works faster :).
              1. 4

                Edwin said that some of the problems will in fact be addressed: https://twitter.com/edwinbrady/status/1216825355417399301

                1. 12

                  In particular, I wouldn’t be surprised if a large part of the compilation performance problems were due to ST, which was a fun thing to try but now I think is far too complicated for what it achieves - linear types probably do the job better for the situations where it’s most useful - and the notation is pretty ugly too. Also the fact that it uses implicit conversions internally (which don’t, and won’t, exist in Idris 2) makes it very hard to get good error messages.

                  It’s great to see people trying these things anyway! I’ll be interested to find out how Idris 2 deals with it, but I have a bit of work to do before it’ll be possible to try.

              1. 0

                From the author:

                If pressed for an answer, though, yes I still do believe in the central conclusions of the article. Namely: That “static typing” and “dynamic typing” are two concepts that are fundamentally unrelated to each other, and just happen to share a word. That “static types” are, at their core a tool for writing and maintaining computer-checked proofs about code That “dynamic types” are, at their core, there to make unit testing less tedious, and are a tool for finding bugs.

                This neatly encapsulates the damage that the Hindley-Milner type system project has done to CS. Neither of these propositions correspond to practice in any way.

                1. 5

                  Damage? Do not correspond to practice? WTF? Please cite examples and sources.

                  BTW, I’m implementing a dynamically typed language right now, and I’m well aware that my dynamic “types” do not correspond to the types found in a static type system. Function values in my language just have type “function” (which lines up with many other dynamic languages, like Python and Scheme). In the simplest static type system (simply-typed lambda calculus), a function type includes an argument type and a result type.

                  1. 3

                    That “static typing” and “dynamic typing” are two concepts that are fundamentally unrelated to each other, and just happen to share a word.

                    I gave an example of this in my prior comment, where function “types” in a dynamic language don’t line up with function types in a static type system.

                    That “static types” are, at their core a tool for writing and maintaining computer-checked proofs about code.

                    The point is that a static type system reports errors in your program before you run it. With increasingly more sophisticated static type systems, you can write computer checked proofs that cover more of the semantics of your programs. Eg, with a dependent type system such as is found in Idris, you can use the type system to prove that the output of a sort function is sorted.

                    That “dynamic types” are, at their core, there to make unit testing less tedious, and are a tool for finding bugs.

                    To ensure that your dynamically typed code is correct, you can’t rely on compile time errors, you have to write unit tests to achieve the same kind of checking.

                    1. 1

                      You don’t need unit testing or any testing at all to profit from dynamic type checking. It may be an advantage to use one or some other test methodology, but that’s it. Similarly, you can call static type checking “computer checked proofs” but that simply sounds like a pompous way of saying “it compiles”.

                      The premise of the milner-hinley type system and e.g. Cardellis type theory is that you can prove correctness of code by checking types (although Cardelli knows that type checking is, at most, a partial indication of correctness and that e.g. they can’t protect against errors like divide by zero). Whether the type system is the proper locus of correctness checking is not at all self-evident. To me, it appears as the result of this effort is complexity in the type system that doesn’t correspond to either mathematical practice or computer architectures. I’m unconvinced that most or the most significant errors come from subtle type errors. Of course, I may be wrong, but your assumption that this line of research is self-evident is, at the least, unsupported.

                      1. 3

                        Cardelli may not have known how to make a type system that protects against divide by zero (it’s arguable), but today that is a solved problem. Eg, see: https://gist.github.com/edwinb/0047a2aff46a0f49c881 for Idris. Or your safe division function returns an Option or Either type, and you use monadic something something syntax to invoke it. I won’t be surprised to see more of this kind of thing in future languages.

                        Is it worth having a super complicated static type system that can catch this error? For me, personally, no. I prefer programming languages that are easy to use and understand, and I feel that some modern type systems are too complex and hard to use.

                        This is all tangential to the topic. The original author made a distinction between the properties of static and dynamic type systems, and his description is correct. Also, my experience as a software engineer (I’m not a mathematician) is that it’s useful to understand the theoretical math that underlies the problem you are trying to solve, it leads you to better solutions. One of my projects is a programming language, and understanding the mathematical theory of programming language design has been very beneficial to this project. And yes, I’m using type theory to help me solve design problems, even though my language is dynamically typed.

                        1. 1

                          That idris “solution”

                          safe_div(x, f(y))

                          wow, all we have to have is a proof of some arbitrary result. Pretty good! Sorry, your compiler spent 4 hours looking for a proof and couldn’t find one so …

                          I’d love to see an example of how type theory helps you solve a real problem . But your assumption that type-theory is the “theoretical math that underlies” any interesting problem at all is not well supported.

                          The distinction between dynamic/static in the op is untenable.

                          1. 4

                            Just to clarify for anyone reading this discussion… The purpose of this gist, as I remember it, was to demonstrate to someone who wanted to know how you could use something like safe_div if you didn’t statically know that it wasn’t dividing by zero (that is, what if the input isn’t known until run time?). So, Idris will accept a call to safe_div if either the second argument in non-zero, or there is a proof in the context that it’s already been checked to be non-zero. Implicit argument search doesn’t (and can’t) claim to be complete, but it is a handy way of guaranteeing that necessary dynamic checks have been done.

                    2. 2

                      Operations in programming modify binary strings. Type systems associate these strings with intended use and some meaning. A major function of type systems is to detect programming errors where operations are applied to binary strings that don’t make sense given the associated type. Both dynamic and static type systems work in the same way - except that static systems use programmer annotations (or possibly inference) to check types at compile time and dynamic type systems are run-time. The end. Typed lambda calculus not needed.

                      1. 3

                        Static and dynamic type systems do not work the same way. They diverge when you consider function types, as I already noted. They diverge when you consider parameterized types, any type that is not just a simple name like String or Int. Dynamic types are usually little more than simple tags that are associated with run-time values: they correspond to simple type names. Dynamic types can be organized in an inheritance hierarchy, which superficially resembles subtypes in a static type system. Static types can have structure, sometimes a lot of structure (especially when you consider rich type systems, dependent types and Curry-Howard correspondence). These rich types seem to have no analog in dynamically typed languages.

                        1. 1

                          The original claim

                          That “static typing” and “dynamic typing” are two concepts that are fundamentally unrelated to each other, and just happen to share a word.

                          And yet, when python code tries to add a string to an int, it produces an error message - same as when that same error is made in a Haskell program. You want to argue that dynamic types are usually simpler than the most complex static types. Different claim.

                  1. 8

                    I think it’s a bit incomplete to talk about how Dependent Haskell is the future of formal verification (not software development), but only compare it to Agda and not any of the actual formal verification languages used in production.

                    Incidentally, is there a big software project that’s been done in Agda? I know Isabelle has seL4 and Coq has CompCert, but I’m drawing a blank on an Agda example.

                    1. 3

                      CakeML is another example from HOL side that pairs with CompCert quite nicely. They’re both compilers.

                      Far as Agda, I dont know anything big. I find a pretty-printer and simple compiler. The publications list might have something if you dare to read all that. ;) Mostly looks like PLT and math stuff vs realistic software.

                      1. 1

                        Or, indeed, to compare it to any other dependently typed languages :)

                        1. 3

                          On one hand, he did mention another independently typed language:

                          There are experiments in this direction, for instance Idris, but Idris is a language with eager (strict) evaluation and its implementation isn’t particularly stable at the moment.

                          Then again,

                          1. Is Dependently-typed Haskell’s implementation notably more stable than Idris’s?
                          2. I recall Idris having very good reasons for not being lazy ;)
                          1. 6

                            That’s not even all of the reasons :).

                            It would be perfectly reasonable to write a lazy back end for Idris. There’s plenty of back ends already and I’ve deliberately made it easy to make more if people want to try stuff out. It would probably involve rewriting a lot of library code to take proper advantage of it, though.

                            My main worry about this sort of discussion is that, cool as it is to see it happening, for me Haskell’s approach to dependent types does a good job of making them look a lot more complicated than they really need to be. I think the concept it a fairly simple one - types are first class in the same way that functions are - but either we’re not doing as good a job of explaining this as we need to be, or it’s not really as simple as I like to think after all…

                            1. 3

                              I used to think it wasn’t simple until the logical connection with proofs started making sense but that was only after years of fighting with the ideas. My most recent foray is with “Type Theory and Formal Proof” + “Software Foundations” and it’s going a lot better.

                              Now I don’t know know why it all seemed complicated. I think the main blocker was getting caught up in the categorical stuff and not realizing that’s just one angle of attack and maybe not even a very good angle at that.

                      1. 8

                        Always a joy to read Conor’s writing :)

                        Note that Epigram has been dead for a while, Idris is its spiritual successor (I believe it actually evolved from an attempt to build an Epigram compiler). Idris is explicitly aiming to be a “real” programming language; Agda is very similar, but is more often used from a mathematical/logical side of Curry-Howard, rather than the programming side.

                        Neither Idris or Agda have the 2D syntax of Epigram, but they both have powerful Emacs modes which can fill in pieces of code (Haskell’s “typed holes” is the same idea, but (as this paper demonstrates) Haskell’s types are less informative).

                        1. 10

                          Indeed, I suppose it’s that Idris evolved from what was intended to be the back end of Epigram. It certainly owes a lot to Conor McBride and James McKinna’s work on Epigram. I don’t know if “real programming language” is exactly the right way to put it, though, so much as being the language I wanted to have to explore the software development potential of dependent types. Maybe “real” will come one day :).

                          1. 1

                            Will we see a longer form post/paper or something that isn’y merely Twitter teasers about Blodwen anytime soon? :)

                            1. 6

                              Hopefully! I know I need to get on with writing things so that more people can join in properly. I have plenty of time to work on it for a change in the next few months, so that’s nice…

                              1. 1

                                Do you have a writeup about it? I’m wondering why you’re replacing Idris which is somewhat established already, I mean that probably is the reason you’re replacing it, but still I wonder what concretely necessitated a whole new language instead of a 2.0

                                1. 6

                                  It isn’t a whole new language, it’s a reimplementation in Idris with some changes that experience suggests will be a good idea. So it’s an evolution of Idris 1. I’ll call it Idris 2 at some point, if it’s successful. It’s promising so far - code type checks significantly faster than in Idris 1, and compiled code runs a bit faster too.

                                  Also, I’ve tried to keep the core language (which is internally called ‘TTImp’ for ‘type theory with implicits’) and the surface language cleanly separated. This is because I occasionally have ideas for alternative surface languages (e.g. taking effects seriously, or typestate, or maybe even an imperative language using linear types internally) and it’ll be much easier to try this if I don’t have to reimplement a dependent type checker every time. I don’t know if I’ll ever get around to trying this sort of thing, but maybe someone else will…

                                  I started this because the Idris implementation has a number of annoying problems (I’ll go into this some other time…) that can only be fixed with some pretty serious reengineering of the core. So I thought, rather than reengineer the core, it would be more fun to see (a) if it was good enough to implement itself, and (b) if dependent types would help in any way.

                                  The answer to (a) turned out to be “not really, but at least we can make it good enough” and to (b) very much so, especially when it comes to name manipulation in the core language, which is tricky to get right but much much easier if you have a type system telling you what to do.

                                  I don’t have any writeup on any of this yet. It’ll happen eventually. (It has to, really - firstly because nobody ever made anything worthwhile on their own so a writeup is important for getting people involved, and secondly because it’s kind of what my job is :))

                                  1. 1

                                    I’m so excited by all of this, can’t wait to see what comes out of it, and it can’t come soon enough:D Idris totally reinvigorated my love for programming tbh

                              2. 2

                                I just follow along with the commits. Edwinb is usually pretty good with his commit messages, so you can kind of get a story of the development from that! :)

                                1. 1

                                  I’ve got to admit it’s very weird reading a reply by someone with your identical name/spelling, thanks!

                                2. 1

                                  What’s Blodwen?

                                  1. 2

                                    An implementation of Idris in Idris: https://github.com/edwinb/Blodwen/

                                    Has a neat implementation of Quantitative Type Theory that I’m hoping to integrate in my own programming language!

                                    1. 1

                                      Nice! What’s your language? Btw your second link is broken

                                      1. 3

                                        Fixed! This is mine: https://github.com/pikelet-lang/pikelet - scratching my itch of Rust not being enough like Idris, and Idris being not designed with low level systems programming in mind. Probably won’t amount to much (it’s rather ambitious), but it’s been fun playing around, learning how dependent type checkers work! I still need to learn more about what Epigram and Idris do, but it takes passes of deepening to really get a handle on all the stuff they learned. I’m probably making a bunch of mistakes that I don’t know about yet!

                                        1. 1

                                          Nice logo. Looks harmless and fun.

                                          1. 1

                                            Nice. I’m starting to realize how I wasn’t the only one to have thought “wouldn’t it be nice to have a purely functional systems language with cool types”:D

                                            What I wanted to make was very similar to Idris, but I would’ve put way more focus on lower-level stuff. Honestly, my way of combining it was likely misguided as I was a total rookie back then (still am, but comparatively, I at least know how much I didn’t know…)

                                            1. 1

                                              Oh cool! I’m sure there are others with a similar itch to scratch - it’s just coming into the realm of the adjacent possibility. Pikelet is just my attempt at pushing that process forwards.

                                              We’ve been growing a nice community over at https://gitter.im/pikelet-lang/Lobby - you are most welcome to drop by if you like!

                                          2. 2
                                  2. 1

                                    Thanks for putting this in context, that’s really useful.

                                    Also: sounds like I’m missing a (200x) in the title, if you know the correct year.

                                  1. 2

                                    How usable is Idris today?

                                    1. 12

                                      I’ve been using Idris to solve some of the advent of code problems this year. I’ve picked it up and put it down about 5 times now, for previous projects too.

                                      My breakdown:

                                      Pros
                                      • The repl is very powerful. It has a bunch of nice features and is generally very fleshed out
                                      • The codegen for other platforms is very easy to get started with. I’ve been compiling Idris to JS, and using from inside Elm - Elm for the UI, Idris for the logic. It’s been working out pretty nicely on the whole
                                      • Proving and preventing things is very powerful, e.g just by limiting vectors to a size, you gain a bunch of reasoning around your code
                                      • Named arguments in the type signature is amazing and I wish more languages had that, especially since point-free style can be so pretty
                                      • Implied arguments can make a lot of sense sometime, e.g cast {from=String} {to=Int}
                                      • A lot of really nice extensions from Haskell are included by default. Records are generally better too
                                      Cons
                                      • The docs are pretty well hidden.
                                        • Generally you are recommended to use the repl to figure things out, but a repl does not replace a good reference
                                        • Links to the library docs are nowhere to be found. I’ve had to bookmark the page because otherwise I end up losing it all the time
                                        • The tutorial is not written for inexperienced people.
                                      • Compiler error messages are definitely not friendly
                                      • Compile times for anything involving complicated proofs are very long
                                      • There’s a big lack of libraries. Part of this might be down to the lack of a package manager
                                      • Some things like take don’t seem to be correctly resolvable by the compiler - it will frequently complain about being unable to figure out which one you want unless you use List.take

                                      Overall, I’m having a blast. I’m even considering using it to generate Native Elm code in a safer manner. We’ll see about that though.

                                      1. 5

                                        I think the documentation being the REPL is a great thing:

                                        Idris> :doc Nat
                                        Data type Prelude.Nat.Nat : Type
                                            Natural numbers: unbounded, unsigned integers which can be pattern
                                            matched.
                                        
                                        Constructors:
                                            Z : Nat
                                                Zero
                                        
                                            S : Nat -> Nat
                                                Successor     
                                        
                                        Idris> :apropos zip
                                        
                                        Prelude.List.unzip : List (a, b) -> (List a, List b)
                                        Split a list of pairs into two lists
                                        
                                        Prelude.Stream.unzip : Stream (a, b) -> (Stream a, Stream b)
                                        Create a pair of streams from a stream of pairs
                                        
                                        Prelude.List.unzip3 : List (a, b, c) -> (List a, List b, List c)
                                        Split a list of triples into three lists
                                        

                                        No need to click around a browser and find the right section. Just search your code and get documentation for whatever you like.

                                        1. 6

                                          It’s not discoverable. You need to know the commands in order to get the docs - e.g :doc, :search, :apropos, :t and so on. It’s not the natural point of entry for many people. It’s also quite hard to know what Idris has named some things, making searching via name or type not so easy. That’s when the reference docs come in handy. Having a browser and being able to link people directly to the function they need is kinda vital to encouraging more people to pick something up, I feel. repls for docs are great when you know what you’re even meant to be typing - not so much if you don’t :)

                                          1. 3

                                            I think it’s a natural entry point for people to type in :help. Yes, people have to learn how to use the commands but it’s definitely nicer than a website.

                                            You also often don’t have to know what Idris names things:

                                            Idris> :search S n + m = n + S m
                                            = Prelude.Nat.plusSuccRightSucc : (left : Nat) ->
                                                                              (right : Nat) -> S (left + right) = left + S right
                                            
                                            1. 1

                                              Until you’ve done something with Nat, you don’t even know what S or Z means. I think the repl is nice, but I also don’t think it can replace a website.

                                              1. 2

                                                My original example of :doc Nat shows what S and Z are - but I don’t think a REPL or a website are the appropriate tools for learning concepts such as Nat.

                                        2. 5

                                          Thanks for the constructive comments!

                                          We definitely need to improve documentation, or at least make it easier to find. There are links on http://www.idris-lang.org/documentation/ but it could still use some better organisation. When I wrote the tutorial it was pretty much entirely as a kind of bootstrap process to get some experienced people up to speed. I think it still serves a useful purpose in doing that, but some more introductory materials would be good. I keep hoping that someone will write an alternative tutorial with a different target audience, but alas “hoping” is not a very good strategy for getting things done…

                                          All of the other things you mention are things we’d like to improve. We don’t have many resources to throw at the problems though, so it’ll take time, but I hope we’ll get there eventually!

                                          1. 1

                                            No problem! Not sure if you remember me, but I was one of the people who interviewed to do a PhD with you (FRP in Idris). So it’s been on my “let’s really play with this” list since then - which was about two years ago! This is my first real attempt of using Idris from production perspective - other things I’ve made with it have mainly been experiments, whereas right now I’m seriously investigating using it with Elm, at least for some things.

                                            Is the main site on Github/open to pull requests? I’d love to help out a bit.

                                            1. 3

                                              Ah yes, I think I know who you are now :). We’re certainly open to pull requests. In particular, it’s good to see that you’re having some success with the JS back end, especially since we haven’t really put much effort into it for ages, so if you have useful contributions there, that’d be great!

                                            2. 1

                                              Do you have a link to a recent write-up on doing a systems application or component in IDRIS showing the triumphs or difficulties? And that is not by one of its developers? I mean, your write-ups are great but I like seeing what average newcomer from functional and/or systems background can do too. These can be different. ;)

                                          2. 2

                                            Main limitations for practical use for most people (assuming they get over the learning hurdle which is all most folks talk about) will be runtime performance and lack of a concurrency story.

                                            1. 2

                                              https://github.com/idris-lang/Idris-dev/blob/master/libs/base/System/Concurrency/Channels.idr is at least erlangish style concurrency via multiple processes if you do message passing.

                                              Everything else you said is spot on, Idris has lots of rough edges but its still a research compiler so to be expected.