Idris Developers Meeting, March 2015

Edwin Brady edited this page Mar 19, 2015 · 30 revisions
Clone this wiki locally

There will be an Idris Developers Meeting in St Andrews, Scotland, from Monday 16th-Friday 20th March 2015. The meeting is open to anyone who is interested in contributing to Idris, implementing libraries or applications in Idris, or just interested in watching progress.


It will be hosted by the School of Computer Science at the University of St Andrews. (map)

  • We will begin at 9:30am on Monday, meeting in the coffee area in the Jack Cole Building
  • For those arriving on Sunday evening, we will meet at 8pm in Aikman's on Bell Street (map)


Watch this space for updates as the week progresses. There will be:

  • Talks (Most likely on Wednesday; please add to this list)
    • Idris quasiquotation (David Christiansen)
    • Guarded recursion in Idris (Sune Alkærsig and Thomas Didriksen)
    • A new tactic system (David Christiansen)
    • A library for command-line flags / options (Guillaume Allais)
    • Uniqueness types and communication protocols (Edwin Brady)
    • Progress on refactoring and dependent types (Andreas Reulaeux)
    • ...
  • Discussion (Please add to this list)
    • Future funding sources
    • Website
      • Does the content of the website need updating/adjusting?
      • Is there content from the GitHub Wiki pages that should be on the Website, and vice-versa?
      • Does anyone want to volunteer to help maintain the website?
    • Documentation
    • Libraries
      • Does libs need sorting/pruning/adding?
        • Yes --- David will do it. A new "contrib" package will contain things that are less canonical.
    • Externally hosted Idris Backends.
      • Can we find maintainers?
    • Branding: We now have a logo and a re branded website.
      • Should we consider the creation on a lambda/pi Idris mark, for use alongside the logo? or is the 'dragon ear' the mark as well as the logo?
        • The participants are not sure what "mark" means in contrast to logo. But we're keeping the thing we have.
      • Should similar considerations be given to an Idris mascot, and also a colour scheme?
        • We won't have a mascot and a colour scheme will not be worked on this week
      • Should we outsource the above if required?
        • It's not really required, but if we want it, we only really have pocket change
      • Should we consider authorised merch for Idris?
        • Yes, Edwin will open up the Spreadshirt instance that he has.
    • Record syntax
    • ...
  • Focussed hacking sessions (Please add to this list)

Things we decided not to do:

  • Generation of a language specification to describe:
    • Language constructs and their use.
    • Underlying implementation details such as elaborater operation, and FFI.
    • Design rationale and guidance.
  • The 'Idris Package Manager'.


Space will be fairly limited, so if you plan to attend, please send an email to Edwin Brady stating:

  • Which days you will be attending
  • Whether you'd like to give a talk (please also add this to the list above)

Optionally, you can also add your name to the list below.


  • Edwin Brady
  • David Christiansen
  • Andreas Reuleaux
  • Thomas Didriksen (Monday-Thursday)
  • Sune Alkærsig (Monday-Thursday)


There is a hostel

Progress Log

Monday 16th

  • Edwin
    • Added provenance information to unification errors
    • Fixed a bug or two
  • David
    • Wrote a pretty-printer for TT
    • Added :core to REPL and its equivalent to IDE mode
  • Matus

Tuesday 17th

  • Jan
    • Proposed, and provided a PR, for Sphinx-Based documentation for Idris.
  • Edwin
    • Resolved some issues
    • Tidying up type class resolution, in particular avoiding resolving too early
    • Implemented 'determining parameters' for typeclasses - a way of annotating which parameters are used for resolving instances.
  • David
    • Made it so the new tactic language can declare types
    • Fixed some issues
    • Discussed library reorg
  • Matus
    • Implemented an alpha of byte buffers + ported Data.Text to it

Wednesday 18th


Thursday 19th

  • Edwin
    • Various type class resolution improvements and fixes