It's Independent Learning Week here in St Andrews, so I'm Independently Learning what Idris 2 can do. You'd think this is the sort of thing I'd know, but it continues to surprise me in pleasing ways.
-
Show this thread
-
Today, for example, I can't decide whether to be pleased or horrified that this type checks... https://gist.github.com/edwinb/90f6cd29dd59e22384ee0dfb1762f6a4 … (Note the pattern matching on types in >>= to work out whether to bind the result as linear or not)
1 reply 1 retweet 9 likesShow this thread -
Replying to @edwinbrady
Does there exist a minimal change to the code that ensures horror?
1 reply 0 retweets 0 likes
Replying to @kristleifur
I took the gratuitous LiftIO out, but otherwise not that I can tell. I was mostly pleased to see there was a way of expressing linearity in the return type. I had been doing that via an index, which was ugly.
10:14 AM - 23 Oct 2019
0 replies
0 retweets
1 like
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.