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).
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 :).
Will we see a longer form post/paper or something that isn’y merely Twitter teasers about Blodwen anytime soon? :)
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…
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
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 :))
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
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! :)
I’ve got to admit it’s very weird reading a reply by someone with your identical name/spelling, thanks!
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!
Nice! What’s your language? Btw your second link is broken
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!
Nice logo. Looks harmless and fun.
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…)
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!
Looks like it was meant to be https://bentnib.org/quantitative-type-theory.html
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.
Looks like 2004 (based on https://scholar.google.com/scholar?cluster=12699060675691339774&hl=en&as_sdt=0,5 )
I can’t remember who posted the interesting type safety idea of making sure that inches and meters were never combined.
You can get this in haskell, along with a huge variety of other units, and conversions
I’m not sure if that one was me. I did push for it for miles and kilometers given we already lost a spacecraft to a conversion error. The technique is types that make things unique by default. Type Miles as Int and Kilometers as Int are treated as two, different types that have to be casted to ensure developer knows something could happen. Ada has this.
There’s also the possibility that they say distance in two modules from two teams with one being miles and one kilometers. That could’ve been how that spacecraft error played out. The types wouldn’t help. So, I further wanted a collection of various units such as miles or kilometers in the standard library where developers explicitly used them to catch more of these errors. That led me to Frink. I bookmarked it in case anyone wanted to work on something like this. It would probably be a nice, head start. Most of it is just formulas but some stuff like currencies are dynamic. Not sure best route for handling that.
I think Tedu may have described how to get something like that in C with structs
I saw the same idea for handling user input. Functions that take user input would be typed as DirtyString or something to that effect and would need to be sanitized before being used elsewhere. For me, it was an enlightening use of types.
I actually did that! It was like having safe vs unsafe in modules. Good for highlighting problems.
The other thing I used it for was Red/Black separation to stop leaks. You make sure stuff with secrets is Red, stuff that’s potentially-hostile is Black, watch CPU/cache/memory interactions, and type system helps with that as they get mixed at various points. I literally added it to variable names, though, which let me do it manually instead of writing a type checker.
F# has that https://fsharpforfunandprofit.com/posts/units-of-measure/
I’ve never used F# though