[HN Gopher] Idris: A language for type-driven development
___________________________________________________________________
Idris: A language for type-driven development
Author : peter_d_sherman
Score : 189 points
Date : 2023-01-20 15:13 UTC (7 hours ago)
(HTM) web link (www.idris-lang.org)
(TXT) w3m dump (www.idris-lang.org)
| peter_d_sherman wrote:
| There also seems to be some intersection here between type-driven
| development and Proof Assistants:
|
| https://en.wikipedia.org/wiki/Proof_assistant
| jshaqaw wrote:
| A huge overlap. Idris is aimed at being a general purpose
| language with proof assistant characteristics while some of its
| peers are more theorem provers built with general purpose
| language characteristics.
| chills wrote:
| See also:
| https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
| peter_d_sherman wrote:
| Wowzer!
|
| That is quite the page...
|
| There is definitely something there!
|
| That page is decidedly worth reading and re-reading many
| times in the future...
|
| I think it boils down to the following:
|
| >"Curry-Howard correspondence [...] is the direct
| relationship between computer programs and mathematical
| proofs."
|
| And:
|
| >"If one abstracts on the peculiarities of either formalism,
| the following generalization arises: a _proof_ is a _program_
| , and _the formula it proves_ is the _type_ for the program.
| "
|
| In fact, I'm going to go for "full crackpot" here...
|
| If all computer programs are algorithms, and all mathematical
| proofs are algorithms, and all types are algorithms -- then a
| "grand unifying theory" between Computer Programs and
| Mathematics -- looks like this:
|
| It's all _Algorithms_.
|
| Algorithms on top of algorithms.
|
| You know, like turtles on top of turtles...
|
| This makes sense too, if we think about it...
|
| Algorithms are just _series of steps_ , with given inputs and
| given outputs.
|
| That is no different than Computer Programs.
|
| And that is no different than Math...
|
| You can call this _series of steps_ an Algorithm, you can
| call it a Function, you can call it y=f(x), you can call it a
| Type, you can call it a Computer Program, you can call it a
| Math Equation, you can call it a logical proposition, and you
| can use whatever notation and nomenclature you like -- but in
| the end, in the end, it all boils down to an Algorithm...
|
| A series of steps...
|
| Now, perhaps that series of steps -- uses other series of
| steps -- perhaps that Algorithm uses other Algorithms,
| perhaps that function uses other functions, perhaps that
| Computer Program uses other computer programs, perhaps that
| Math Equation uses other math equations, etc., etc. --
|
| But in the end, in the end...
|
| It's all a series of rigorously defined steps...
|
| It's all an Algorithm...
|
| Or Algorithm consisting of other Algorithms...
| (recursively...)
|
| Patterns of steps -- inside of patterns of other steps
| (again, recursively...)
|
| Anyway, great page, definitely worth reading and re-reading!
| schoen wrote:
| If you're excited about that, you might enjoy
|
| https://softwarefoundations.cis.upenn.edu/
|
| Officially you're supposed to download the book and then
| edit the exercise solutions into it with Emacs (or VSCode,
| I think), as you can then run the exercises to see if they
| type-check (i.e., if they're correct!). However, there's
| also a not-necessarily-up-to-date interactive in-browser
| version:
|
| https://jscoq.github.io/ext/sf/
|
| I haven't used Idris, so I'd say it's quite possible that
| working through the Idris book is also just as fun and
| relevant for understanding the implications of the Curry-
| Howard correspondence.
| ykonstant wrote:
| I am dabbling in the cousin language Lean right now, and it is
| very fun to use!
| peter_d_sherman wrote:
| Some quick info for Lean:
|
| Homepage: https://leanprover.github.io/
|
| Source: https://github.com/leanprover/lean4
|
| Wikipedia: https://en.wikipedia.org/wiki/Lean_(proof_assistant)
| agentultra wrote:
| I also wrote a guide:
| https://agentultra.github.io/lean-4-hackers/
| daxfohl wrote:
| One difference I see is Lean uses type classes while Idris uses
| implicits. Can anyone comment on the pros and cons of that
| decision? (Or pros and cons between the two languages in
| general?)
|
| It also seems that Idris was created as a general-purpose
| language first, whereas Lean started as a proof assistant and
| only recently added general-purpose language. Is that evident
| when using the languages? A quick look at Lean's general-
| purpose language seems reasonably similar to the Indris
| experience AFAICT.
| ImprobableTruth wrote:
| Imo the biggest difference is the "heritage", Lean is Coq
| inspired, Idris Agda inspired. This manifests in how people
| prove things. Idris has dependent pattern matching, so proofs
| are written as normal terms. Lean has tactics and proofs are
| small tactics scripts (which then generate the proof term
| behind the scene).
|
| Other than that, the difference is mainly in
| infrastructure/libraries and community.
| lapinot wrote:
| Well, idris (v2) is very special since it has modalities
| for compile-time erasure and linearity. This sets it apart
| from all the other dependently-typed languages. This makes
| it possible in theory (and currently being experimented
| with) to implement efficient-by-construction code.
|
| https://arxiv.org/abs/2104.00480
| ImprobableTruth wrote:
| Linearity is exclusive to Idris 2, compile time only
| values/run-time erasure are supported by all major proof
| assistants. Coq and Lean have the Prop type (compile time
| only) while Agda allows annotation of variables as run-
| time irrelevant.
| [deleted]
| nightowl_games wrote:
| Anyone else finding this documentation is pretty hard to
| navigate? Makes me think this isn't a serious language, but
| rather an academic toy or resume builder.
| andrewmcwatters wrote:
| The main repository is in the top 1% of stargazed repositories
| on GitHub, and the project has a mailing list, Discord server,
| IRC, AND Slack.
|
| It has been forked over 300 times, and has over 100
| contributors.
|
| What in the world counts as "serious" to some of you people?
|
| Sometimes I read HN and ask myself if people here know at all
| how hard it is make something people want, and how many people
| know what the real-world thresholds are for understanding when
| you have made something that people want.
|
| I guess if everyone hasn't heard of it, people here don't think
| it's serious.
| Kranar wrote:
| >What in the world counts as "serious" to some of you people?
|
| For a programming language? Would be good to know what
| projects have used it. Most languages people develop are done
| as either a hobby or to serve some kind of research/academic
| purpose. Is Idris used for any production grade software?
| mejutoco wrote:
| I find Idris incredibly interesting. Specially combined with
| the output it can generate in other languages. The book of it
| is also a masterpiece, even if you never program in it.
| Already lots of "serious" hacked together programming
| languages.
|
| The only downside I see if the lack of a package manager.
| bobleeswagger wrote:
| [flagged]
| andrewmcwatters wrote:
| I mean you tell me, which would be bullying to you? You
| work for years on something and someone tells you it's not
| "serious" because they haven't learned to browse a source
| tree, or the guy telling him to read a little more?
|
| Either way, I apologize for how it came off.
| bobleeswagger wrote:
| > someone tells you it's not "serious" because they
| haven't learned to browse a source tree
|
| "Fuck this stranger for not learning something I know how
| to do!"
| CoastalCoder wrote:
| > Anyone else finding this documentation is pretty hard to
| navigate?
|
| I can't speak to these docs in particular, but I think
| documentation regarding type-system in general can be hard to
| digest. And it probably varies by reader.
|
| E.g., some people find "The Little Typer" [0] to be a wonderful
| intro to its topic. Personally, I find the writing style
| impenetrable.
|
| > Makes me think this isn't a serious language, but rather an
| academic toy or resume builder.
|
| If the documentation turns out to be useless to the majority of
| readers, then you might be right that it's a sign of under-
| investment. I'm not sure if that's happening here.
|
| There was a good interview on Corecursive [1] about Idris, so
| IMHO that's some evidence that some people are serious about
| the language.
|
| [0] https://mitpress.mit.edu/9780262536431/the-little-typer/
|
| [1] https://corecursive.com/006-type-driven-development-and-
| idri...
| wk_end wrote:
| TBH I actually think the documentation for Idris is quite good,
| but your overall point is correct: it's definitely somewhere
| between "academic toy" and "serious language". It's not really
| usable for anything real world at the moment, and - like I
| comment every time it pops up here - just as it was building up
| momentum the author scrapped the whole thing and started over
| (Idris 2), and even though I've been making that comment for
| years it still hasn't recovered. The book everyone recommends
| to read on it is based around a dead version of the language;
| the tooling it has you use (which is a huge part of working
| with a dependently-typed language) depends on Atom, which is
| now dead, and Idris 2 still doesn't have comparable IDE
| support.
|
| I find it really frustrating because I like the language a lot,
| and I want to be using dependent types in my real life ASAP.
| Right now I'd be looking more towards Lean, though, which seems
| to be more modern and developing rapidly.
| hjadal wrote:
| The Atom implementation has been replicated in VSCode and
| works alright. It was good enough for me to learn how Idris
| worked and go through the book's exercises.
| revskill wrote:
| I think it's the chicken-egg issue. Firstly it's not the
| tools'fault. But overall, the culture of using that tool made
| it worse.
|
| For example, most of readthedocs documentation i've seen is
| nothing better a wiki page, where you have a bunch of links to
| click on in a messy way somehow.
|
| So i guess your issue with this one, is you're missing some
| structured knowledge with this page.
| mcdonje wrote:
| I know I'm missing something, but this seems like the functional
| version of object classes.
|
| I've mostly favored procedural programming and only use objects
| when I have to because the abstraction can make the program
| harder to reason about, especially when there's a lot of
| inheritance.
|
| But I've heard some hype about types in Rust, and now this. The
| free chapter in the manning book even introduces types in terms
| of real world objects.
|
| So, for someone who doesn't love objects, why should I love
| types?
| allochthon wrote:
| I recently watched this intro to the topic, which I found
| really interesting: https://www.youtube.com/watch?v=bnnacleqg6k
| ok_dad wrote:
| Where objects can hide state or I/O in a program, types and
| functional type driven development make each function very
| clear as to what it has for input and outputs and part of that
| is not hiding state anywhere that doesn't make sense. You might
| still have a global logger because that makes sense, but
| generally you know the things you have access to because
| they're in the function signature.
|
| It can break down if you aren't careful, and there's some
| nuance where you might still store a configuration data as an
| object property, but it's a clearly typed property that's
| assigned at initialization rather than hidden state that
| magically appears due to some hidden program flow.
| satvikpendem wrote:
| The book itself _Type Driven Development with Idris_ is great
| too, it is the principal way I write code these days, by writing
| my types upfront then filling out the logic, and in some
| languages, the logic itself can be produced automatically via the
| filling of type holes. In other words, simply based on the types
| you provide, the compiler can guess the implementation of the
| function, somewhat like Copilot but guaranteed to be correct on a
| type level, even if not necessarily on a business logic level.
|
| https://www.manning.com/books/type-driven-development-with-i...
| janjones wrote:
| > the compiler can guess the implementation of the function
| [...] guaranteed to be correct on a type level
|
| I'm curious about this. Can you provide some examples, please?
| Which languages can do this?
| [deleted]
| adamgordonbell wrote:
| The guessing the implementation part is pretty cool. You can
| find videos of Edwin Brady showing it off on youtube:
|
| https://www.youtube.com/watch?v=DRq2NgeFcO0
|
| The book also walks you through lots of examples. The key
| part is the type needs to constrain the possible
| implementations down quite a bit.
| jfoutz wrote:
| off the top of my head, coq agda idris.
|
| you can sort of do this with ghci and :hoogle.
|
| the simplest example is
|
| foo : A -> A
|
| since we know absolutely NOTHING about A, all we can really
| do is give it back to you, so foo turns out to be identity,
| or id.
|
| another might be bar: [A] -> Nat we still don't know anything
| about A, but we know a little about lists, so a good
| suggestion might be length.
|
| All of the environments are pretty interactive, and you pick
| and choose. but from time to time there is exactly one
| possible implementation that meets all the constraints, so
| the compiler can fill that in.
| dunham wrote:
| Also "Wingman" for Haskell does some type-driven code
| generation. (It might be part of the haskell language
| server now, I get it when I use the vscode plugin.)
|
| When the solution is ambiguous, Idris (and I believe
| wingman) will supply suggestions that you can pick from.
|
| In your `bar` case, `bar xs = 42` is also a solution. Idris
| suggests 0 1 2 3 ... I think, it's going off of the
| constructors for the return type. I expect this technology
| to improve over time (try to use arguments, etc.)
|
| Idris and Agda will also do stuff short of "fill in the
| answer" like "case split an argument for me" or "insert the
| appropriate constructor or lambda and leave a hole inside".
| This is quite helpful in cases where it's not gonna find
| the answer, but can type out the next step or two for you.
| (Wingman might have this, I haven't used it much. I don't
| know Coq at all.)
|
| On the Agda side, the first couple of sections of
| "Programming Language Foundations in Agda" will walk you
| through using that functionality. Idris has a couple of
| videos that others have pointed out. It's fun stuff.
| jfoutz wrote:
| in agda, I think ctrl-c ctrl-a is the "I feel lucky"
| button. Plfa is definitely good, Connor Mcbride is pretty
| good too https://www.youtube.com/playlist?list=PLqggUNm8Q
| SqmeTg5n37ox...
|
| and yes programming with holes is almost magical. I
| really like "run as much as you can" then complain when
| you get stuck. kind of a mind blowing change for me.
| acchow wrote:
| I had never heard of this book before, now I definitely want to
| give it a try.
|
| As an aside, isn't type driven development how everyone codes
| naturally in statically typed languages? Whether it's Ocaml or
| Java, I feel like I try to get the types defined, then put on
| music and turn my brain off and just line the types up (much
| moreso in Ocaml than in Java).
| satvikpendem wrote:
| Indeed, and this is precisely why I hate writing in
| dynamically typed languages like Ruby or Python; they hinder
| me from thinking about the shape of the program clearly.
| iddan wrote:
| Well now you can write full types in both of them
| shpongled wrote:
| You can write them, but without most of the benefits of
| static types
| mejutoco wrote:
| You can typecheck them with mypy or pyright or at runtime
| with typeguard.
|
| It is not ideal, but pretty good in terms of benefits.
| ok_dad wrote:
| That's great, but sometimes those tools fail to spot an
| error silently, where a compiler plus runtime checks
| usually won't.
| miohtama wrote:
| As an extensive user and a fan of these Python type
| checking tools, I do not remember this happening for some
| years now. Do you have a particular example where it
| should be improved?
| ok_dad wrote:
| Yea, at work mypy fails quite often on the old code
| there.
| shpongled wrote:
| I still use python type hints (and TypeScript) - and
| while they have benefits, I find that they fall short of
| something like Rust, Haskell, etc (because they are just
| that - hints). I don't have the surety that the types as
| annotated are the same as the types at runtime.
| mcphage wrote:
| > the logic itself can be produced automatically via the
| filling of type holes
|
| Does that work in anything but boilerplate code? Like, hole
| filling won't be able to decide between then and else clauses
| in a conditional, for instance, because both clauses return the
| same type. And conditionals are one of the most basic data flow
| structures.
| grumpyprole wrote:
| Don't forget that "type derived code" also happens with any
| language that has implicit arguments, e.g. type classes in
| Haskell and implicits in Scala. For example, in Haskell, if I
| compare two lists-of-maps-of-tuples for equality, there are
| many nested equality functions involved, but the type class
| machinery generates this code, at compile time for me. In a
| language without this, e.g. OCaml, many generic operations like
| equality, to_string, serialisation, etc become very painful.
| jshaqaw wrote:
| I'm a big fan of this book for anyone interested in the topic:
| https://www.amazon.com/Gentle-Introduction-Dependent-Types-I...
| theusus wrote:
| How is it better than tdd in Idris book?
| gre wrote:
| Better link... https://leanpub.com/gidti
| CoastalCoder wrote:
| Anyone know if there's a decent way to get a printed copy?
|
| Or barring that, can anyone suggest a good device on which to
| read it and jot notes, for someone who normally prefers
| printed books?
| [deleted]
| kadoban wrote:
| If you can find a used Remarkable 2 or something, that's a
| real nice experience. Great for textbooks and comics.
|
| You can buy them new, but I think they've moved to some
| fairly insane forced subscription model.
|
| Edit: looks like the forced subscription is no longer as
| bad as it once was
| nerdponx wrote:
| I bought a basic b&w two-sided laser printer in 2011 for
| this purpose, and it's served me extremely well over the
| years. You can then take the stack of pages to a store like
| Staples and they will bind it for you for a few dollars.
|
| I got the Brother HL-2270DW and I think they still make it.
| They even publish official Linux drivers for CUPS! Just
| make sure to get the extended toner cartridges (TN450), the
| regular ones are a ripoff.
| Jtsummers wrote:
| Staples and others will also print and bind PDFs you
| bring in. I've done this with purchased books, sometimes
| they get a bit picky but usually they'll just do it.
| peter_d_sherman wrote:
| Looks highly interesting... Thanks for the suggestion!
| timmg wrote:
| FWIW, I tried to read that book. It really didn't connect with
| me. Probably because I don't understand where it's going.
|
| Does anyone have a good pointer to a different tutorial that
| tries to teach type-driven development?
| theresistor wrote:
| What's the state of Idris2 at this point? I really enjoyed _Type
| Driven Development with Idris_ a few years ago.
| peter_d_sherman wrote:
| >"In Idris, types are first-class constructs in the langauge.
|
| _This means types can be passed as arguments to functions, and
| returned from functions just like any other value, such as
| numbers, strings, or lists._
|
| This is a small but powerful idea, enabling:
|
| o Relationships to be expressed between values; for example, that
| two lists have the same length.
|
| o Assumptions to be made explicit and checked by the compiler.
| For example, if you assume that a list is non-empty, Idris can
| ensure this assumption always holds before the program is run.
|
| o If desired, properties of program behaviour to be formally
| stated and proven."
|
| PDS: I'd be curious to know about any/all languages where types
| can be passed to functions, returned from functions -- and even
| generated at runtime by functions... that is, where the language
| regards types as first-class constructs...
| skybrian wrote:
| Zig does some of this.
|
| Functions can be written that can be called at compile time or
| runtime, depending on which language features they use.
|
| Types can be computed and returned by functions in compile-time
| expressions.
|
| I don't know how expressive the types can get, though?
| Avshalom wrote:
| I'm going to guess not very expressive. Zig refuses to have
| operator overloading because it might be used to call a
| function that's more expensive than you'd guess so the idea
| that they'd let types enforce all that much seems unlikely.
| kitd wrote:
| This is presumably not what you're thinking of but ofc
| Javascript uses objects as prototype "types". As is, they wont
| provide what you want, but if there was some kind of "compile-
| time" processing of prototypes such that types assemblies,
| dependencies, constraints and other relationships could be
| manipulated or asserted before they were applied in runtime
| code, that may provide some of the "first-class type"
| functionality mentioned.
|
| Ed: actually, Typescript might be a better host for this.
| eckza wrote:
| FP Or Die Gang is downvoting you, but this is actually
| correct.
|
| No referential transparency (among other things, no doubt)
| makes this a harder problem to solve than just using a
| language that supports it.
|
| $0.02
| teddyh wrote:
| > _PDS: I 'd be curious to know about any/all languages where
| types can be passed to functions, returned from functions --
| and even generated at runtime by functions... that is, where
| the language regards types as first-class constructs..._
|
| Python does this.
| ihm wrote:
| These types are statically checked (i.e., can be checked
| before runtime).
| teddyh wrote:
| I was not replying to the article, I was replying to the
| question from "peter_d_sherman" asking if any other
| programming language has types as first-class constructs.
| And Python does that.
| typedfalse wrote:
| Eh, in this context those aren't types; instead Python is
| unityped. Agreed they are still fun though.
| peter_d_sherman wrote:
| Sure! I'll accept Python into the list of languages that
| have types as first-class constructs! And thanks, the
| suggestion is much appreciated!
| csande17 wrote:
| Zig is probably the closest you'll get to this in an imperative
| language. You can write functions that take types as arguments
| and return types, and that's how e.g. generic data structures
| are implemented.
| astrange wrote:
| You can do that in Smalltalk descendants, if by types you
| mean metaclasses.
| brabel wrote:
| Terra is a language that can also do that, and uses Lua as
| the metaprogramming language. Types are just Lua values.
|
| But unfortunately, there's a lot of work left kind of half-
| baked so using the language is a pain... if someone invested
| a lot of time to make Terra work properly and added some
| tooling around it, wrote proper docs and so on, it would be a
| really interesting language.
|
| https://terralang.org/
| avgcorrection wrote:
| > Terra is a language that can also do that, and uses Lua
| as the metaprogramming language. Types are just Lua values.
|
| But then Terra doesn't do that. Lua does. But not to
| itself, so it's not really about passing around types as
| first-class values any more than metaprogramming Java in
| Python would elevate Java types to being first-class
| values.
| ihm wrote:
| The most famous ones off the top of my head: Coq, Agda, Lean,
| Idris, ATS. Here's a list:
| https://en.wikipedia.org/wiki/Category:Dependently_typed_lan...
| peter_d_sherman wrote:
| That (and pages like that) are what I was looking for!
|
| Thanks, much appreciated!
| [deleted]
| spelunker wrote:
| Here's an intro to dependent types from David Christiansen, I
| think it came up during another dependent types discussion:
| https://youtu.be/VxINoKFm-S4
___________________________________________________________________
(page generated 2023-01-20 23:00 UTC)