My new plan for teaching FP: Start with Agda so they will be slightly sad about Idris and then after Idris they will be sad about Haskell.
-
-
Replying to @ReinH
what makes you sad in Idris? Some things make me sad too, but there are tradeoffs everywhere.
1 reply 0 retweets 0 likes -
Replying to @edwinbrady
I prefer true mixfix to syntax/dsl, I like unicode syntax and (almost) unrestricted identifier grammar, case-aware proof search...
2 replies 0 retweets 1 like -
Replying to @ReinH
Aha. I want the last of those, but I'm not keen on the others. I've gone off extensible syntax too.
1 reply 0 retweets 1 like -
Replying to @edwinbrady @ReinH
Extensible syntax a la Racket is much more fun than extensible syntax a la Idris
3 replies 1 retweet 7 likes -
Replying to @d_christiansen @edwinbrady
I'll take mixfix if it's on offer, please. ;)
1 reply 0 retweets 0 likes -
I also wish Idris didn't borrow Haskell's restrictions on operator grammar. I want letters in my operators sometimes!
2 replies 0 retweets 1 like
I think a lot of these are matters of taste, but I'm open to more flexible operator syntax at least...
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.