Edwin Brady - Idris 2: Type-driven development of Idris | Code Mesh LDN 18

This video was recorded at Code Mesh LDN 18 bit.ly/2P7SPII
Get involved in Code Sync's next conference bit.ly/2Mcm4aS
---
IDRIS 2: TYPE-DRIVEN DEVELOPMENT OF IDRIS
by Edwin Brady
THIS TALK IN THREE WORDS:
Enthusiasm
About
Types :)
TALK LEVEL:
ABSTRACT
We've been having lots of fun over the last couple of years investigating the possibilities and limitations of type-driven development in Idris. As we write larger programs, though, we're finding the implementation of Idris is showing the strain - such is the nature of "research quality software" - and recently I decided the time was right to start again, and implement Idris 2 in Idris. In this talk, I'll give an introduction to type-driven development (in Idris 2) and report on progress so far, showing off the most interesting features which the new design enables (notably, linear types and better type inference).
Read the full abstract: codesync.global/speaker/edwin-...
---
THE SPEAKER - EDWIN BRADY
Creator of the Idris programming language; Lecturer
Edwin is Lecturer in Computer Science at the University of St Andrews in Scotland, interested in type-driven development, domain-specific languages and reasoning about effectful programs. When he's not doing that, he might be playing Go, watching cricket, or wandering around Scotland's hills.
More on Edwin Brady: codesync.global/speaker/edwin-...
---
CODE SYNC & CODE MESH LDN 18
Code Mesh LDN is powered by Code Sync. Code Mesh LDN 18 was sponsored by WhatsApp, Toyota Connected, Erlang Solutions, TEAMango, and aeternity.
CODE SYNC
Website: www.codesync.global
Twitter: CodeMeshIO
Facebook: / codesyncglobal
LinkedIn: / code-sync
Mail: info at codesync.global
#CodeMesh #Idris #EdwinBrady #TDD

[@derelbenkoenig]

Beautiful how Idris was able to do all this dependently-typed programming, _and_ voice Knuckles in the second Sonic movie. True Renaissance man.

[@CBaggers]

I love this speaker. His talks always hit that lovely balance between practical and academic and have a lovely learning curve (for me at least as I often struggle with this stuff). Cant wait for more blodwen!

[@declup]

Idris 2 --> "And I thought, it can't be that easy. That's just embarrassing. It can't be that easy. It was." (17:00)
Java/C/C# --> ...

[@mortenbrodersen8664]

This is BRILLIANT!

[@C4rb0neum]

So simple yet so useful. I hope this will catch on!

[@bneymanov]

Really great!

[@nilp0inter2]

This is absolutely bananas!

[@mwgkgk]

awesome

[@OptimusVlad]

For the love of all that's holy, please make this language embeddable into c/c++ programs. c/c++ can be used to do the performance critical stuff and we can use Idris for the app/business logic parts. If the runtime is designed to be embeddable then, trivially, there can (and will be) a standalong cli version that can run on its on.
If idris cannot be embedded into larger programs, then it is virtually impossible to sell this to current users of other languages, as its economically unfeasible to use Idris standalone (because of no ecosystem/userbase/tools).
I NEED this language in my life.

[@osolomons]

There's a good foriegn function interface (at least in Idris 1, I'm sure it exists in Idris 2 too) so you can call C from Idris and pass Idris functions as pointers to C. It would certainly be possible to make a system that automates some of the foriegn function setup and allow C to be embedded in Idris code.
The main problem is that there aren't enough people working on Idris to make it industry-ready.

[@saltrocklamp199]

The core language runtime is written in Chez scheme and I think it's already been ported to Racket. Maybe it can be ported to another Scheme that's specifically meant for embedding (Guile?).

[@saltrocklamp199]

@@osolomons Linear types in Idris 2 should theoretically help with memory management too. I've seriously thought about going back to academia specifically so I can work on this stuff...

[@luisaranda9015]

curious to know if this language will be suitable for systems programming once it gets linear types.

[@johannes.schaffer]

Never thought someone like him would use macOS:)

[@okuno54]

41:03 Don't worry; I laughed at it

[@bocckoka]

is it int? no, it's isInt

[@Hangtime875]

who else got lost because of star Citizen in here? :)

[@hectobit]

ded gaem

[@Copperis]

I got here from elsewhere, but am intrigued. How is star citizen related to this video?

[@hectobit]

@@Copperis I have no fucking clue. But lett me tell you, this seaso is fucking shit.Don't buy. Just abandon the series.