Hmm. Duo knows...
Edwin Brady
@edwinb
- 24 Followers
- 39 Following
- 430 Posts
CS Lecturer at University of St Andrews. Idris hacker, programming language researcher and developer. He/him.
Okay, there are good bits.
(it may look empty, but the usual crowd are chatting on separate tables, metres apart...)
Doing some clearing out, I've found this in a cupboard. Not sure I have the right dongle to load it on my Mac though.
We used to play some approximation of cricket here years ago. I see they've removed the slide that fielded at silly mid off.
House rule: if you hit the slide on the full, you're out caught.
It's yet more evidence that the game favours batters these days...
Okay, so I've actually got a bit further, it's just that I didn't think of that joke (if that's what it is) until now. #lightningwit
The scheme based evaluator seems to be just the teensiest bit faster...
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've had to pop into St Andrews for the first time in months. Better do my bit for the local economy while I'm here! These parts are especially important...
We have got to stop making the joke (which is far too strong a word for it) that we don't need to run dependently typed programs because we already know they work.
Although I realise I have a t-shirt which says "It type checks, ship it!" so I'm hardly blameless...
This sort of improvement always pleases me.
Although in this case, it did leave me asking myself "Why didn't you do it that way in the first place ya numpty?"
Oops. On the plus side, I just implemented a thing that GHC has been doing for about 25 years and got a small performance gain.
(From https://www.microsoft.com/en-us/research/wp-content/uploads/1998/09/comp-by-trans-scp.pdf)
