A common question at the minute (meaning about 3 people have asked) is: will you update the book for Idris 2?
Short answer: It'll still be entirely relevant. Idris 2 won't be gratuitously different from Idris 1, it'll just work better. /cc @ManningBooks
-
-
At the very least, I'll make sure updated code is online! And I suppose this is as good a point as any for another gratuitous plug. https://www.manning.com/books/type-driven-development-with-idris … with 50% off the eBook today (20181217) via https://www.manning.com/dotd !
Show this threadThanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
One thing I’ve been mulling for my own experiments is : can 0 weighted values be used impredicatively in types? Would be a neat way to get traditional parametricity ! I’m fuzzy on soundness though. I have some notes on how to rep these function spaces you may like.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
Also the right tweak to function spaces lets you encode some really cool forms of reasoning.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
Is there a story of pi/rho calculus and Idris 2? Blockchain peeps could prove termination for smart contracts and use concurrency approach they care about. There are some papers about linear types, session types and pi calc. Blockchain would be the killer app for Idris :)
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.