In case you missed it: We're hiring CS Lecturers/Senior Lectures/Readers in St Andrews. Closing date August 17th.
Hiring in all areas of CS and I'd love to have more Programming Languages colleagues!
This is important because type checking interesting dependently typed programs fundamentally relies on this evaluator. As it stands now, if Idris is slow to type check something, it's almost always the evaluator.
So I hope I can fill in those remaining holes! Place Your Bets...
There are now 9 holes. so it's still like a golf course, albeit a smaller one.
Turns out this does adapt to Idris, yay! Although this fork of Idris is currently like a golf course, in that it has 18 holes and involves someone shouting FOUR a lot.
I suppose if your runtime just happens to include a compiler for the lambda calculus, you might as well see what you can do with it...
This is a toy language that compiles to Scheme so it can use the Scheme evaluator on open terms, then read back from Scheme to its syntax.
That last example runs instantly. In contrast, the Idris evaluator takes 15 seconds on the equivalent. I might have some fun with this...
The main goal of my research is to find the most contrived way of calculating 2+2. Latest effort: https://gist.github.com/edwinb/00319dfe5aebcedc3849fffd428e4123#file-eval-idr-L143-L225
I put my ECOOP talk on this here new fangled youtube thingy: https://www.youtube.com/watch?v=msTsTKRT9xs
That's the edited highlights of this paper: https://drops.dagstuhl.de/opus/volltexte/2021/14052/
In case anyone's interested, the answer turns out to be one thread making a blocking FFI call, and the other waiting for the blocking FFI call to finish so that it can run the garbage collector before sending a message to the other blocking thread.
Are there any Chez Scheme experts who can tell me what a "tc-mutex" is, and whether it behaves differently with "--program" and "--script"?
Still exploring yesterday's concurrency problem... I don't have any of my own mutexes! #lazyweb
I should perhaps have been explicit that I'm not asking for advice here... you'd think I'd know how twitter works by now ;).
I have several guesses as to why this might be happening, and it's clearly a real problem that only one version happens to trip over.
I've ended up with 8 seconds to spare. I'll have to think of a short joke or I've wasted an opportunity...
I think if I edit out every time I say the word "so" that's a good two minutes saved.
Aikman's has been painted and polished up. I might have to complain.
CS Lecturer at University of St Andrews. Idris hacker, programming language researcher and developer. He/him.
Server run by the main developers of the project It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!