Idris Developers Meeting, Nov 2013

There will be an Idris Developers Meeting in St Andrews, Scotland, from Monday 18th-Friday 22nd November 2013. 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.

Location

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

• We will be in room 1.04 in the Jack Cole Building all week, except:
  • 10-11 Monday 18th, Jack Cole 1.33b
  • 11-12 Monday 18th, John Honey Building, Goldfish Bowl
  • 11-1pm Wednesday 20th, Jack Cole 0.29
  • 11-12 Friday 22nd, Jack Cole 1.33a
  • 12-1pm Friday 22nd, Jack Cole 1.33b
• 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)

Content

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

• Talks (Please add to this list)
  • An overview of Idris internals (Edwin Brady)
  • Idris type providers (David Christiansen)
  • Ideslave mode (structured input and output to idris, to be used by development environments) hannes
  • Abstraction classes (why they should be included, somewhat short presentation) - Ahmad Salim Al-Sibahi
  • Computational Mathematics and Idris/Dependent Types - Markus Pfeiffer
  • Idris and, Modern and Modern Modern Encryption - Jan de Muijnck-Hughes
  • ...
• Discussion (Please add to this list)
  • Library design (class hierarchy, effects, ...)
    • In particular, what should be in the Prelude? A dependent Prelude?
  • Module system
  • Copatterns
  • Error reflection (might turn into talk by David Christiansen)
  • Interactive editing
  • Projects for GSoC, grants, funding, papers, ...
  • Generic programming, 'deriving'
  • What is required for version 1.0?
  • Abstraction classes
  • Computational Mathematics and Idris/Dependent Types
  • Crypto Bindings
  • ...
• Focussed hacking sessions (Please add to this list)
  • Type classes as dependent records
  • Optimisation: better inlining, partial evaluation
  • Library optimisations: string processing is particularly bad
  • Bug squashing (from the issue tracker)
  • Improving laziness in executor (the thing that does :x)
  • Improving proof search
  • Making binary packages for various OSes
  • Std Library and Prelude Documentation
  • Tutorial Updates and Improvements
  • ...

Registration

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.

Attendees

• Edwin Brady
• Markus Pfeiffer
• Simon Fowler
• Franziska Schmidt
• David Christiansen
• Hannes Mehnert
• Ahmad Salim Al-Sibahi
• Jan de Muijnck-Hughes
• Matúš Tejiščák

Practicalities

There is a hostel

Progress Log

18. November 2013

Markus:

• Added floating point primitives, and finally managed to open a proper pull request, #627
• While being around tests, I patched test scripts to use #!/usr/bin/env.

Matúš:

• Figuring out collapsibility and forceable arguments of data constructors
• Constructor disjointness check fully recursive now

Edwin:

• Talked about internals
• Started work on reimplementing partial evaluation
• Answered lots of questions :)

Jan:

• Started work on a logo.
• Started working on tutorials, one result is Idris Koans.

David:

• Closed #607
• Worked with Hannes on proper support for interactive editing in ideslave and the Emacs mode

Ahmad:

• Finishing eliminators (started to work)

Hannes

• Worked with David on interactive editing and ideslave
• started cleanups to support building on FreeBSD out of the box

19. November 2013

Markus

• Fixed tests for presence of floating point primitives and fix the pull request
• setup idris bindings to libusb, the repository lives at https://github.com/idris-hackers/usb

Matúš

• extending forceability to recursive applications of a datatype

Hannes

• polished patches for FreeBSD support

Jan

• Worked more on Idris-Koans and improved tutorials using meta variables.

20. November 2013

Jan

• Gave talk: Idris, Modern and Modern Modern Cryptography.

Matúš

• forceability check rewritten from the ground up (runtime reconstructing projections pending)

Markus

• worked on libusb bindings, successfully opened usb devices

21. November 2013

Jan

• Updated Idris Hackers Blog and worked on Tutorial.

Edwin

• Improved type class implementation using dependent records
• Reorganisation of the libraries, separating the prelude from the base libraries